Переписать с последствиями в Изабель - PullRequest
Новая
       8

Переписать с последствиями в Изабель

1 голос
/ 13 января 2020

Я ищу метод для переписывания, но с последствиями вместо равенств.

Например, я знаю, что x = 3 ∧ y = 4 подразумевает Q x y, и теперь я хочу заменить положительное вхождение Q x y в моей текущей подцели с x = 3 ∧ y = 4. Есть ли в Изабель существующий метод для этого?

Например, я хотел бы сделать что-то вроде этого (где implication_subst - название метода, который я ищу): 

lemma 
  assumes a1: "⋀x y. x = 3 ∧ y = 4 ⟹ Q x y"
shows "(∃x y. A x ∧ Q x y ∧ B y)"
proof (implication_subst a1)
  show "∃x y. A x ∧ (x = 3 ∧ y = 4) ∧ B y"
    sorry
qed

Ниже приведена моя (неполная) попытка реализовать такой метод с использованием Eisbach, возможно, это дает лучшее представление о том, что я ищу: 


named_theorems pos_cong

lemma implication_subst_exists[pos_cong]: 
  assumes "⋀x. P x ⟹ Q x"
    and "∃x. P x"
  shows "∃x. Q x"
  using assms  by blast

lemma implication_subst_conjl[pos_cong]:
  assumes "P ⟹ Q"
 and "P ∧ A"
shows "Q ∧ A"
  using assms  by blast

lemma implication_subst_conjr[pos_cong]:
  assumes "P ⟹ Q"
 and "A ∧ P"
shows "A ∧ Q"
  using assms  by blast

lemma implication_subst_neg[pos_cong]:
  assumes "P ⟹ Q"
    and "P"
  shows "¬¬Q"
  using assms by auto

lemma implication_subst_impl[pos_cong]:
  assumes "P ⟹ ¬Q"
    and "¬P ⟶ A"
  shows "Q ⟶ A"
  using assms by auto

lemma implication_subst_impr[pos_cong]:
  assumes "P ⟹ Q"
    and "A ⟶ P"
  shows "A ⟶ Q"
  using assms by auto

lemma implication_subst_neg_disj_l[pos_cong]:
  assumes "P ⟹ ¬Q"
    and "¬(¬P ∨ A)"
  shows "¬(Q ∨ A)"
  using assms by auto

lemma implication_subst_neg_disj_r[pos_cong]:
  assumes "P ⟹ ¬Q"
    and "¬(A ∨ ¬P)"
  shows "¬(A ∨ Q)"
  using assms by auto



method implication_subst_h uses r declares pos_cong = (
      rule r 
      | (rule pos_cong, implication_subst_h r: r, assumption))

method implication_subst uses r declares pos_cong =
  (implication_subst_h r: r pos_cong: pos_cong, (unfold not_not)?)


lemma example1: 
  assumes a1: "⋀x y. x = 3 ∧ y = 4 ⟹ Q x y"
  shows "∃x y. A x ∧ Q x y ∧ B y"
proof (implication_subst r: a1)
  show "∃x y. A x ∧ (x = 3 ∧ y = 4) ∧ B y"
    sorry
qed


lemma example2: 
  assumes a1: "⋀x y. x = 3 ∧ y = 4 ⟹ Q x y"
  shows "(∃x y. ¬(¬A x ∨ ¬Q x y ∨ ¬B y))"
proof (implication_subst r: a1)
  show "∃x y. ¬ (¬ A x ∨ ¬ (x = 3 ∧ y = 4) ∨ ¬ B y)"
    sorry
qed
...