diff --git a/thys/Goedel_HFSet_Semanticless/Coding.thy b/thys/Goedel_HFSet_Semanticless/Coding.thy --- a/thys/Goedel_HFSet_Semanticless/Coding.thy +++ b/thys/Goedel_HFSet_Semanticless/Coding.thy @@ -1,681 +1,682 @@ chapter\De Bruijn Syntax, Quotations, Codes, V-Codes\ theory Coding imports SyntaxN begin declare fresh_Nil [iff] section \de Bruijn Indices (locally-nameless version)\ nominal_datatype dbtm = DBZero | DBVar name | DBInd nat | DBEats dbtm dbtm nominal_datatype dbfm = DBMem dbtm dbtm | DBEq dbtm dbtm | DBDisj dbfm dbfm | DBNeg dbfm | DBEx dbfm declare dbtm.supp [simp] declare dbfm.supp [simp] fun lookup :: "name list \ nat \ name \ dbtm" where "lookup [] n x = DBVar x" | "lookup (y # ys) n x = (if x = y then DBInd n else (lookup ys (Suc n) x))" lemma fresh_imp_notin_env: "atom name \ e \ name \ set e" by (metis List.finite_set fresh_finite_set_at_base fresh_set) lemma lookup_notin: "x \ set e \ lookup e n x = DBVar x" by (induct e arbitrary: n) auto lemma lookup_in: "x \ set e \ \k. lookup e n x = DBInd k \ n \ k \ k < n + length e" apply (induct e arbitrary: n) apply (auto intro: Suc_leD) apply (metis Suc_leD add_Suc_right add_Suc_shift) done lemma lookup_fresh: "x \ lookup e n y \ y \ set e \ x \ atom y" by (induct arbitrary: n rule: lookup.induct) (auto simp: pure_fresh fresh_at_base) lemma lookup_eqvt[eqvt]: "(p \ lookup xs n x) = lookup (p \ xs) (p \ n) (p \ x)" by (induct xs arbitrary: n) (simp_all add: permute_pure) lemma lookup_inject [iff]: "(lookup e n x = lookup e n y) \ x = y" apply (induct e n x arbitrary: y rule: lookup.induct, force, simp) by (metis Suc_n_not_le_n dbtm.distinct(7) dbtm.eq_iff(3) lookup_in lookup_notin) nominal_function trans_tm :: "name list \ tm \ dbtm" where "trans_tm e Zero = DBZero" | "trans_tm e (Var k) = lookup e 0 k" | "trans_tm e (Eats t u) = DBEats (trans_tm e t) (trans_tm e u)" by (auto simp: eqvt_def trans_tm_graph_aux_def) (metis tm.strong_exhaust) nominal_termination (eqvt) by lexicographic_order lemma fresh_trans_tm_iff [simp]: "i \ trans_tm e t \ i \ t \ i \ atom ` set e" by (induct t rule: tm.induct, auto simp: lookup_fresh fresh_at_base) lemma trans_tm_forget: "atom i \ t \ trans_tm [i] t = trans_tm [] t" by (induct t rule: tm.induct, auto simp: fresh_Pair) nominal_function (invariant "\(xs, _) y. atom ` set xs \* y") trans_fm :: "name list \ fm \ dbfm" where "trans_fm e (Mem t u) = DBMem (trans_tm e t) (trans_tm e u)" | "trans_fm e (Eq t u) = DBEq (trans_tm e t) (trans_tm e u)" | "trans_fm e (Disj A B) = DBDisj (trans_fm e A) (trans_fm e B)" | "trans_fm e (Neg A) = DBNeg (trans_fm e A)" | "atom k \ e \ trans_fm e (Ex k A) = DBEx (trans_fm (k#e) A)" +supply [[simproc del: defined_all]] apply(simp add: eqvt_def trans_fm_graph_aux_def) apply(erule trans_fm_graph.induct) using [[simproc del: alpha_lst]] apply(auto simp: fresh_star_def) apply(rule_tac y=b and c=a in fm.strong_exhaust) apply(auto simp: fresh_star_def) apply(erule_tac c=ea in Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: fresh_star_Pair perm_supp_eq) apply (simp add: fresh_star_def) done nominal_termination (eqvt) by lexicographic_order lemma fresh_trans_fm [simp]: "i \ trans_fm e A \ i \ A \ i \ atom ` set e" by (nominal_induct A avoiding: e rule: fm.strong_induct, auto simp: fresh_at_base) abbreviation DBConj :: "dbfm \ dbfm \ dbfm" where "DBConj t u \ DBNeg (DBDisj (DBNeg t) (DBNeg u))" lemma trans_fm_Conj [simp]: "trans_fm e (Conj A B) = DBConj (trans_fm e A) (trans_fm e B)" by (simp add: Conj_def) lemma trans_tm_inject [iff]: "(trans_tm e t = trans_tm e u) \ t = u" proof (induct t arbitrary: e u rule: tm.induct) case Zero show ?case apply (cases u rule: tm.exhaust, auto) apply (metis dbtm.distinct(1) dbtm.distinct(3) lookup_in lookup_notin) done next case (Var i) show ?case apply (cases u rule: tm.exhaust, auto) apply (metis dbtm.distinct(1) dbtm.distinct(3) lookup_in lookup_notin) apply (metis dbtm.distinct(10) dbtm.distinct(11) lookup_in lookup_notin) done next case (Eats tm1 tm2) thus ?case apply (cases u rule: tm.exhaust, auto) apply (metis dbtm.distinct(12) dbtm.distinct(9) lookup_in lookup_notin) done qed lemma trans_fm_inject [iff]: "(trans_fm e A = trans_fm e B) \ A = B" proof (nominal_induct A avoiding: e B rule: fm.strong_induct) case (Mem tm1 tm2) thus ?case by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: fresh_star_def) next case (Eq tm1 tm2) thus ?case by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: fresh_star_def) next case (Disj fm1 fm2) show ?case by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: Disj fresh_star_def) next case (Neg fm) show ?case by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: Neg fresh_star_def) next case (Ex name fm) thus ?case using [[simproc del: alpha_lst]] proof (cases rule: fm.strong_exhaust [where y=B and c="(e, name)"], simp_all add: fresh_star_def) fix name'::name and fm'::fm assume name': "atom name' \ (e, name)" assume "atom name \ fm' \ name = name'" thus "(trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')" (is "?lhs = ?rhs") proof (rule disjE) assume "name = name'" thus "?lhs = ?rhs" by (metis fresh_Pair fresh_at_base(2) name') next assume name: "atom name \ fm'" have eq1: "(name \ name') \ trans_fm (name' # e) fm' = trans_fm (name' # e) fm'" by (simp add: flip_fresh_fresh name) have eq2: "(name \ name') \ ([[atom name']]lst. fm') = [[atom name']]lst. fm'" by (rule flip_fresh_fresh) (auto simp: Abs_fresh_iff name) show "?lhs = ?rhs" using name' eq1 eq2 Ex(1) Ex(3) [of "name#e" "(name \ name') \ fm'"] by (simp add: flip_fresh_fresh) (metis Abs1_eq(3)) qed qed qed lemma trans_fm_perm: assumes c: "atom c \ (i,j,A,B)" and t: "trans_fm [i] A = trans_fm [j] B" shows "(i \ c) \ A = (j \ c) \ B" proof - have c_fresh1: "atom c \ trans_fm [i] A" using c by (auto simp: supp_Pair) moreover have i_fresh: "atom i \ trans_fm [i] A" by auto moreover have c_fresh2: "atom c \ trans_fm [j] B" using c by (auto simp: supp_Pair) moreover have j_fresh: "atom j \ trans_fm [j] B" by auto ultimately have "((i \ c) \ (trans_fm [i] A)) = ((j \ c) \ trans_fm [j] B)" by (simp only: flip_fresh_fresh t) then have "trans_fm [c] ((i \ c) \ A) = trans_fm [c] ((j \ c) \ B)" by simp then show "(i \ c) \ A = (j \ c) \ B" by simp qed section\Characterising the Well-Formed de Bruijn Formulas\ subsection\Well-Formed Terms\ inductive wf_dbtm :: "dbtm \ bool" where Zero: "wf_dbtm DBZero" | Var: "wf_dbtm (DBVar name)" | Eats: "wf_dbtm t1 \ wf_dbtm t2 \ wf_dbtm (DBEats t1 t2)" equivariance wf_dbtm inductive_cases Zero_wf_dbtm [elim!]: "wf_dbtm DBZero" inductive_cases Var_wf_dbtm [elim!]: "wf_dbtm (DBVar name)" inductive_cases Ind_wf_dbtm [elim!]: "wf_dbtm (DBInd i)" inductive_cases Eats_wf_dbtm [elim!]: "wf_dbtm (DBEats t1 t2)" declare wf_dbtm.intros [intro] lemma wf_dbtm_imp_is_tm: assumes "wf_dbtm x" shows "\t::tm. x = trans_tm [] t" using assms proof (induct rule: wf_dbtm.induct) case Zero thus ?case by (metis trans_tm.simps(1)) next case (Var i) thus ?case by (metis lookup.simps(1) trans_tm.simps(2)) next case (Eats dt1 dt2) thus ?case by (metis trans_tm.simps(3)) qed lemma wf_dbtm_trans_tm: "wf_dbtm (trans_tm [] t)" by (induct t rule: tm.induct) auto theorem wf_dbtm_iff_is_tm: "wf_dbtm x \ (\t::tm. x = trans_tm [] t)" by (metis wf_dbtm_imp_is_tm wf_dbtm_trans_tm) nominal_function abst_dbtm :: "name \ nat \ dbtm \ dbtm" where "abst_dbtm name i DBZero = DBZero" | "abst_dbtm name i (DBVar name') = (if name = name' then DBInd i else DBVar name')" | "abst_dbtm name i (DBInd j) = DBInd j" | "abst_dbtm name i (DBEats t1 t2) = DBEats (abst_dbtm name i t1) (abst_dbtm name i t2)" apply (simp add: eqvt_def abst_dbtm_graph_aux_def, auto) apply (metis dbtm.exhaust) done nominal_termination (eqvt) by lexicographic_order nominal_function subst_dbtm :: "dbtm \ name \ dbtm \ dbtm" where "subst_dbtm u i DBZero = DBZero" | "subst_dbtm u i (DBVar name) = (if i = name then u else DBVar name)" | "subst_dbtm u i (DBInd j) = DBInd j" | "subst_dbtm u i (DBEats t1 t2) = DBEats (subst_dbtm u i t1) (subst_dbtm u i t2)" by (auto simp: eqvt_def subst_dbtm_graph_aux_def) (metis dbtm.exhaust) nominal_termination (eqvt) by lexicographic_order lemma fresh_iff_non_subst_dbtm: "subst_dbtm DBZero i t = t \ atom i \ t" by (induct t rule: dbtm.induct) (auto simp: pure_fresh fresh_at_base(2)) lemma lookup_append: "lookup (e @ [i]) n j = abst_dbtm i (length e + n) (lookup e n j)" by (induct e arbitrary: n) (auto simp: fresh_Cons) lemma trans_tm_abs: "trans_tm (e@[name]) t = abst_dbtm name (length e) (trans_tm e t)" by (induct t rule: tm.induct) (auto simp: lookup_notin lookup_append) subsection\Well-Formed Formulas\ nominal_function abst_dbfm :: "name \ nat \ dbfm \ dbfm" where "abst_dbfm name i (DBMem t1 t2) = DBMem (abst_dbtm name i t1) (abst_dbtm name i t2)" | "abst_dbfm name i (DBEq t1 t2) = DBEq (abst_dbtm name i t1) (abst_dbtm name i t2)" | "abst_dbfm name i (DBDisj A1 A2) = DBDisj (abst_dbfm name i A1) (abst_dbfm name i A2)" | "abst_dbfm name i (DBNeg A) = DBNeg (abst_dbfm name i A)" | "abst_dbfm name i (DBEx A) = DBEx (abst_dbfm name (i+1) A)" apply (simp add: eqvt_def abst_dbfm_graph_aux_def, auto) apply (metis dbfm.exhaust) done nominal_termination (eqvt) by lexicographic_order nominal_function subst_dbfm :: "dbtm \ name \ dbfm \ dbfm" where "subst_dbfm u i (DBMem t1 t2) = DBMem (subst_dbtm u i t1) (subst_dbtm u i t2)" | "subst_dbfm u i (DBEq t1 t2) = DBEq (subst_dbtm u i t1) (subst_dbtm u i t2)" | "subst_dbfm u i (DBDisj A1 A2) = DBDisj (subst_dbfm u i A1) (subst_dbfm u i A2)" | "subst_dbfm u i (DBNeg A) = DBNeg (subst_dbfm u i A)" | "subst_dbfm u i (DBEx A) = DBEx (subst_dbfm u i A)" by (auto simp: eqvt_def subst_dbfm_graph_aux_def) (metis dbfm.exhaust) nominal_termination (eqvt) by lexicographic_order lemma fresh_iff_non_subst_dbfm: "subst_dbfm DBZero i t = t \ atom i \ t" by (induct t rule: dbfm.induct) (auto simp: fresh_iff_non_subst_dbtm) section\Well formed terms and formulas (de Bruijn representation)\ inductive wf_dbfm :: "dbfm \ bool" where Mem: "wf_dbtm t1 \ wf_dbtm t2 \ wf_dbfm (DBMem t1 t2)" | Eq: "wf_dbtm t1 \ wf_dbtm t2 \ wf_dbfm (DBEq t1 t2)" | Disj: "wf_dbfm A1 \ wf_dbfm A2 \ wf_dbfm (DBDisj A1 A2)" | Neg: "wf_dbfm A \ wf_dbfm (DBNeg A)" | Ex: "wf_dbfm A \ wf_dbfm (DBEx (abst_dbfm name 0 A))" equivariance wf_dbfm lemma atom_fresh_abst_dbtm [simp]: "atom i \ abst_dbtm i n t" by (induct t rule: dbtm.induct) (auto simp: pure_fresh) lemma atom_fresh_abst_dbfm [simp]: "atom i \ abst_dbfm i n A" by (nominal_induct A arbitrary: n rule: dbfm.strong_induct) auto text\Setting up strong induction: "avoiding" for name. Necessary to allow some proofs to go through\ nominal_inductive wf_dbfm avoids Ex: name by (auto simp: fresh_star_def) inductive_cases Mem_wf_dbfm [elim!]: "wf_dbfm (DBMem t1 t2)" inductive_cases Eq_wf_dbfm [elim!]: "wf_dbfm (DBEq t1 t2)" inductive_cases Disj_wf_dbfm [elim!]: "wf_dbfm (DBDisj A1 A2)" inductive_cases Neg_wf_dbfm [elim!]: "wf_dbfm (DBNeg A)" inductive_cases Ex_wf_dbfm [elim!]: "wf_dbfm (DBEx z)" declare wf_dbfm.intros [intro] lemma trans_fm_abs: "trans_fm (e@[name]) A = abst_dbfm name (length e) (trans_fm e A)" apply (nominal_induct A avoiding: name e rule: fm.strong_induct) apply (auto simp: trans_tm_abs fresh_Cons fresh_append) apply (metis One_nat_def Suc_eq_plus1 append_Cons list.size(4)) done lemma abst_trans_fm: "abst_dbfm name 0 (trans_fm [] A) = trans_fm [name] A" by (metis append_Nil list.size(3) trans_fm_abs) lemma abst_trans_fm2: "i \ j \ abst_dbfm i (Suc 0) (trans_fm [j] A) = trans_fm [j,i] A" using trans_fm_abs [where e="[j]" and name=i] by auto lemma wf_dbfm_imp_is_fm: assumes "wf_dbfm x" shows "\A::fm. x = trans_fm [] A" using assms proof (induct rule: wf_dbfm.induct) case (Mem t1 t2) thus ?case by (metis trans_fm.simps(1) wf_dbtm_imp_is_tm) next case (Eq t1 t2) thus ?case by (metis trans_fm.simps(2) wf_dbtm_imp_is_tm) next case (Disj fm1 fm2) thus ?case by (metis trans_fm.simps(3)) next case (Neg fm) thus ?case by (metis trans_fm.simps(4)) next case (Ex fm name) thus ?case apply auto apply (rule_tac x="Ex name A" in exI) apply (auto simp: abst_trans_fm) done qed lemma wf_dbfm_trans_fm: "wf_dbfm (trans_fm [] A)" apply (nominal_induct A rule: fm.strong_induct) apply (auto simp: wf_dbtm_trans_tm abst_trans_fm) apply (metis abst_trans_fm wf_dbfm.Ex) done lemma wf_dbfm_iff_is_fm: "wf_dbfm x \ (\A::fm. x = trans_fm [] A)" by (metis wf_dbfm_imp_is_fm wf_dbfm_trans_fm) lemma dbtm_abst_ignore [simp]: "abst_dbtm name i (abst_dbtm name j t) = abst_dbtm name j t" by (induct t rule: dbtm.induct) auto lemma abst_dbtm_fresh_ignore [simp]: "atom name \ u \ abst_dbtm name j u = u" by (induct u rule: dbtm.induct) auto lemma dbtm_subst_ignore [simp]: "subst_dbtm u name (abst_dbtm name j t) = abst_dbtm name j t" by (induct t rule: dbtm.induct) auto lemma dbtm_abst_swap_subst: "name \ name' \ atom name' \ u \ subst_dbtm u name (abst_dbtm name' j t) = abst_dbtm name' j (subst_dbtm u name t)" by (induct t rule: dbtm.induct) auto lemma dbfm_abst_swap_subst: "name \ name' \ atom name' \ u \ subst_dbfm u name (abst_dbfm name' j A) = abst_dbfm name' j (subst_dbfm u name A)" by (induct A arbitrary: j rule: dbfm.induct) (auto simp: dbtm_abst_swap_subst) lemma subst_trans_commute [simp]: "atom i \ e \ subst_dbtm (trans_tm e u) i (trans_tm e t) = trans_tm e (subst i u t)" apply (induct t rule: tm.induct) apply (auto simp: lookup_notin fresh_imp_notin_env) apply (metis abst_dbtm_fresh_ignore dbtm_subst_ignore lookup_fresh lookup_notin subst_dbtm.simps(2)) done lemma subst_fm_trans_commute [simp]: "subst_dbfm (trans_tm [] u) name (trans_fm [] A) = trans_fm [] (A (name::= u))" apply (nominal_induct A avoiding: name u rule: fm.strong_induct) apply (auto simp: lookup_notin abst_trans_fm [symmetric]) apply (metis dbfm_abst_swap_subst fresh_at_base(2) fresh_trans_tm_iff) done lemma subst_fm_trans_commute_eq: "du = trans_tm [] u \ subst_dbfm du i (trans_fm [] A) = trans_fm [] (A(i::=u))" by (metis subst_fm_trans_commute) section\Quotations\ fun HTuple :: "nat \ tm" where "HTuple 0 = HPair Zero Zero" | "HTuple (Suc k) = HPair Zero (HTuple k)" lemma fresh_HTuple [simp]: "x \ HTuple n" by (induct n) auto lemma HTuple_eqvt[eqvt]: "(p \ HTuple n) = HTuple (p \ n)" by (induct n, auto simp: HPair_eqvt permute_pure) subsection \Quotations of de Bruijn terms\ definition nat_of_name :: "name \ nat" where "nat_of_name x = nat_of (atom x)" lemma nat_of_name_inject [simp]: "nat_of_name n1 = nat_of_name n2 \ n1 = n2" by (metis nat_of_name_def atom_components_eq_iff atom_eq_iff sort_of_atom_eq) definition name_of_nat :: "nat \ name" where "name_of_nat n \ Abs_name (Atom (Sort ''SyntaxN.name'' []) n)" lemma nat_of_name_Abs_eq [simp]: "nat_of_name (Abs_name (Atom (Sort ''SyntaxN.name'' []) n)) = n" by (auto simp: nat_of_name_def atom_name_def Abs_name_inverse) lemma nat_of_name_name_eq [simp]: "nat_of_name (name_of_nat n) = n" by (simp add: name_of_nat_def) lemma name_of_nat_nat_of_name [simp]: "name_of_nat (nat_of_name i) = i" by (metis nat_of_name_inject nat_of_name_name_eq) lemma HPair_neq_ORD_OF [simp]: "HPair x y \ ORD_OF i" by (metis HPair_def ORD_OF.elims SUCC_def tm.distinct(3) tm.eq_iff(3)) text\Infinite support, so we cannot use nominal primrec.\ function quot_dbtm :: "dbtm \ tm" where "quot_dbtm DBZero = Zero" | "quot_dbtm (DBVar name) = ORD_OF (Suc (nat_of_name name))" | "quot_dbtm (DBInd k) = HPair (HTuple 6) (ORD_OF k)" | "quot_dbtm (DBEats t u) = HPair (HTuple 1) (HPair (quot_dbtm t) (quot_dbtm u))" by (rule dbtm.exhaust) auto termination by lexicographic_order subsection \Quotations of de Bruijn formulas\ text\Infinite support, so we cannot use nominal primrec.\ function quot_dbfm :: "dbfm \ tm" where "quot_dbfm (DBMem t u) = HPair (HTuple 0) (HPair (quot_dbtm t) (quot_dbtm u))" | "quot_dbfm (DBEq t u) = HPair (HTuple 2) (HPair (quot_dbtm t) (quot_dbtm u))" | "quot_dbfm (DBDisj A B) = HPair (HTuple 3) (HPair (quot_dbfm A) (quot_dbfm B))" | "quot_dbfm (DBNeg A) = HPair (HTuple 4) (quot_dbfm A)" | "quot_dbfm (DBEx A) = HPair (HTuple 5) (quot_dbfm A)" by (rule_tac y=x in dbfm.exhaust, auto) termination by lexicographic_order lemma HTuple_minus_1: "n > 0 \ HTuple n = HPair Zero (HTuple (n - 1))" by (metis Suc_diff_1 HTuple.simps(2)) lemmas HTS = HTuple_minus_1 HTuple.simps \ \for freeness reasoning on codes\ class quot = fixes quot :: "'a \ tm" ("\_\") instantiation tm :: quot begin definition quot_tm :: "tm \ tm" where "quot_tm t = quot_dbtm (trans_tm [] t)" instance .. end lemma quot_dbtm_fresh [simp]: "s \ (quot_dbtm t)" by (induct t rule: dbtm.induct) auto lemma quot_tm_fresh [simp]: fixes t::tm shows "s \ \t\" by (simp add: quot_tm_def) lemma quot_Zero [simp]: "\Zero\ = Zero" by (simp add: quot_tm_def) lemma quot_Var: "\Var x\ = SUCC (ORD_OF (nat_of_name x))" by (simp add: quot_tm_def) lemma quot_Eats: "\Eats x y\ = HPair (HTuple 1) (HPair \x\ \y\)" by (simp add: quot_tm_def) instantiation fm :: quot begin definition quot_fm :: "fm \ tm" where "quot_fm A = quot_dbfm (trans_fm [] A)" instance .. end lemma quot_dbfm_fresh [simp]: "s \ (quot_dbfm A)" by (induct A rule: dbfm.induct) auto lemma quot_fm_fresh [simp]: fixes A::fm shows "s \ \A\" by (simp add: quot_fm_def) lemma quot_fm_permute [simp]: fixes A:: fm shows "p \ \A\ = \A\" by (metis fresh_star_def perm_supp_eq quot_fm_fresh) lemma quot_Mem: "\x IN y\ = HPair (HTuple 0) (HPair (\x\) (\y\))" by (simp add: quot_fm_def quot_tm_def) lemma quot_Eq: "\x EQ y\ = HPair (HTuple 2) (HPair (\x\) (\y\))" by (simp add: quot_fm_def quot_tm_def) lemma quot_Disj: "\A OR B\ = HPair (HTuple 3) (HPair (\A\) (\B\))" by (simp add: quot_fm_def) lemma quot_Neg: "\Neg A\ = HPair (HTuple 4) (\A\)" by (simp add: quot_fm_def) lemma quot_Ex: "\Ex i A\ = HPair (HTuple 5) (quot_dbfm (trans_fm [i] A))" by (simp add: quot_fm_def) lemmas quot_simps = quot_Var quot_Eats quot_Eq quot_Mem quot_Disj quot_Neg quot_Ex section\Definitions Involving Coding\ abbreviation Q_Eats :: "tm \ tm \ tm" where "Q_Eats t u \ HPair (HTuple (Suc 0)) (HPair t u)" abbreviation Q_Succ :: "tm \ tm" where "Q_Succ t \ Q_Eats t t" lemma quot_Succ: "\SUCC x\ = Q_Succ \x\" by (auto simp: SUCC_def quot_Eats) abbreviation Q_HPair :: "tm \ tm \ tm" where "Q_HPair t u \ Q_Eats (Q_Eats Zero (Q_Eats (Q_Eats Zero u) t)) (Q_Eats (Q_Eats Zero t) t)" abbreviation Q_Mem :: "tm \ tm \ tm" where "Q_Mem t u \ HPair (HTuple 0) (HPair t u)" abbreviation Q_Eq :: "tm \ tm \ tm" where "Q_Eq t u \ HPair (HTuple 2) (HPair t u)" abbreviation Q_Disj :: "tm \ tm \ tm" where "Q_Disj t u \ HPair (HTuple 3) (HPair t u)" abbreviation Q_Neg :: "tm \ tm" where "Q_Neg t \ HPair (HTuple 4) t" abbreviation Q_Conj :: "tm \ tm \ tm" where "Q_Conj t u \ Q_Neg (Q_Disj (Q_Neg t) (Q_Neg u))" abbreviation Q_Imp :: "tm \ tm \ tm" where "Q_Imp t u \ Q_Disj (Q_Neg t) u" abbreviation Q_Ex :: "tm \ tm" where "Q_Ex t \ HPair (HTuple 5) t" abbreviation Q_All :: "tm \ tm" where "Q_All t \ Q_Neg (Q_Ex (Q_Neg t))" lemma quot_subst_eq: "\A(i::=t)\ = quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))" by (metis quot_fm_def subst_fm_trans_commute) lemma Q_Succ_cong: "H \ x EQ x' \ H \ Q_Succ x EQ Q_Succ x'" by (metis HPair_cong Refl) subsection\The set \\\ of Definition 1.1, constant terms used for coding\ inductive coding_tm :: "tm \ bool" where Ord: "\i. x = ORD_OF i \ coding_tm x" | HPair: "coding_tm x \ coding_tm y \ coding_tm (HPair x y)" declare coding_tm.intros [intro] lemma coding_tm_Zero [intro]: "coding_tm Zero" by (metis ORD_OF.simps(1) Ord) lemma coding_tm_HTuple [intro]: "coding_tm (HTuple k)" by (induct k, auto) inductive_simps coding_tm_HPair [simp]: "coding_tm (HPair x y)" lemma quot_dbtm_coding [simp]: "coding_tm (quot_dbtm t)" apply (induct t rule: dbtm.induct, auto) apply (metis ORD_OF.simps(2) Ord) done lemma quot_dbfm_coding [simp]: "coding_tm (quot_dbfm fm)" by (induct fm rule: dbfm.induct, auto) lemma quot_fm_coding: fixes A::fm shows "coding_tm \A\" by (metis quot_dbfm_coding quot_fm_def) section \V-Coding for terms and formulas, for the Second Theorem\ text\Infinite support, so we cannot use nominal primrec.\ function vquot_dbtm :: "name set \ dbtm \ tm" where "vquot_dbtm V DBZero = Zero" | "vquot_dbtm V (DBVar name) = (if name \ V then Var name else ORD_OF (Suc (nat_of_name name)))" | "vquot_dbtm V (DBInd k) = HPair (HTuple 6) (ORD_OF k)" | "vquot_dbtm V (DBEats t u) = HPair (HTuple 1) (HPair (vquot_dbtm V t) (vquot_dbtm V u))" by (auto, rule_tac y=b in dbtm.exhaust, auto) termination by lexicographic_order lemma fresh_vquot_dbtm [simp]: "i \ vquot_dbtm V tm \ i \ tm \ i \ atom ` V" by (induct tm rule: dbtm.induct) (auto simp: fresh_at_base pure_fresh) text\Infinite support, so we cannot use nominal primrec.\ function vquot_dbfm :: "name set \ dbfm \ tm" where "vquot_dbfm V (DBMem t u) = HPair (HTuple 0) (HPair (vquot_dbtm V t) (vquot_dbtm V u))" | "vquot_dbfm V (DBEq t u) = HPair (HTuple 2) (HPair (vquot_dbtm V t) (vquot_dbtm V u))" | "vquot_dbfm V (DBDisj A B) = HPair (HTuple 3) (HPair (vquot_dbfm V A) (vquot_dbfm V B))" | "vquot_dbfm V (DBNeg A) = HPair (HTuple 4) (vquot_dbfm V A)" | "vquot_dbfm V (DBEx A) = HPair (HTuple 5) (vquot_dbfm V A)" by (auto, rule_tac y=b in dbfm.exhaust, auto) termination by lexicographic_order lemma fresh_vquot_dbfm [simp]: "i \ vquot_dbfm V fm \ i \ fm \ i \ atom ` V" by (induct fm rule: dbfm.induct) (auto simp: HPair_def HTuple_minus_1) class vquot = fixes vquot :: "'a \ name set \ tm" ("\_\_" [0,1000]1000) instantiation tm :: vquot begin definition vquot_tm :: "tm \ name set \ tm" where "vquot_tm t V = vquot_dbtm V (trans_tm [] t)" instance .. end lemma vquot_dbtm_empty [simp]: "vquot_dbtm {} t = quot_dbtm t" by (induct t rule: dbtm.induct) auto lemma vquot_tm_empty [simp]: fixes t::tm shows "\t\{} = \t\" by (simp add: vquot_tm_def quot_tm_def) lemma vquot_dbtm_eq: "atom ` V \ supp t = atom ` W \ supp t \ vquot_dbtm V t = vquot_dbtm W t" by (induct t rule: dbtm.induct) (auto simp: image_iff, blast+) instantiation fm :: vquot begin definition vquot_fm :: "fm \ name set \ tm" where "vquot_fm A V = vquot_dbfm V (trans_fm [] A)" instance .. end lemma vquot_fm_fresh [simp]: fixes A::fm shows "i \ \A\V \ i \ A \ i \ atom ` V" by (simp add: vquot_fm_def) lemma vquot_dbfm_empty [simp]: "vquot_dbfm {} A = quot_dbfm A" by (induct A rule: dbfm.induct) auto lemma vquot_fm_empty [simp]: fixes A::fm shows "\A\{} = \A\" by (simp add: vquot_fm_def quot_fm_def) lemma vquot_dbfm_eq: "atom ` V \ supp A = atom ` W \ supp A \ vquot_dbfm V A = vquot_dbfm W A" by (induct A rule: dbfm.induct) (auto simp: intro!: vquot_dbtm_eq, blast+) lemma vquot_fm_insert: fixes A::fm shows "atom i \ supp A \ \A\(insert i V) = \A\V" by (auto simp: vquot_fm_def supp_conv_fresh intro: vquot_dbfm_eq) declare HTuple.simps [simp del] end diff --git a/thys/Robinson_Arithmetic/Robinson_Arithmetic.thy b/thys/Robinson_Arithmetic/Robinson_Arithmetic.thy --- a/thys/Robinson_Arithmetic/Robinson_Arithmetic.thy +++ b/thys/Robinson_Arithmetic/Robinson_Arithmetic.thy @@ -1,1252 +1,1253 @@ (*<*) theory Robinson_Arithmetic imports Nominal2.Nominal2 begin (*>*) section \Terms and Formulas\ text \nat is a pure permutation type\ instance nat :: pure by standard atom_decl name declare fresh_set_empty [simp] lemma supp_name [simp]: fixes i::name shows "supp i = {atom i}" by (rule supp_at_base) subsection \The datatypes\ nominal_datatype trm = zer | Var name | suc trm | pls trm trm | tms trm trm nominal_datatype fmla = eql trm trm (infixr "EQ" 150) | dsj fmla fmla (infixr "OR" 130) | neg fmla | exi x::name f::fmla binds x in f text \eql are atomic formulas; dsj, neg, exi are non-atomic\ declare trm.supp [simp] fmla.supp [simp] subsection \Substitution\ nominal_function subst :: "name \ trm \ trm \ trm" where "subst i x zer = zer" | "subst i x (Var k) = (if i=k then x else Var k)" | "subst i x (suc t) = suc (subst i x t)" | "subst i x (pls t u) = pls (subst i x t) (subst i x u)" | "subst i x (tms t u) = tms (subst i x t) (subst i x u)" by (auto simp: eqvt_def subst_graph_aux_def) (metis trm.strong_exhaust) nominal_termination (eqvt) by lexicographic_order lemma fresh_subst_if [simp]: "j \ subst i x t \ (atom i \ t \ j \ t) \ (j \ x \ (j \ t \ j = atom i))" by (induct t rule: trm.induct) (auto simp: fresh_at_base) lemma forget_subst_trm [simp]: "atom a \ trm \ subst a x trm = trm" by (induct trm rule: trm.induct) (simp_all add: fresh_at_base) lemma subst_trm_id [simp]: "subst a (Var a) trm = trm" by (induct trm rule: trm.induct) simp_all lemma subst_trm_commute [simp]: "atom j \ trm \ subst j u (subst i t trm) = subst i (subst j u t) trm" by (induct trm rule: trm.induct) (auto simp: fresh_Pair) lemma subst_trm_commute2 [simp]: "atom j \ t \ atom i \ u \ i \ j \ subst j u (subst i t trm) = subst i t (subst j u trm)" by (induct trm rule: trm.induct) auto lemma repeat_subst_trm [simp]: "subst i u (subst i t trm) = subst i (subst i u t) trm" by (induct trm rule: trm.induct) auto nominal_function subst_fmla :: "fmla \ name \ trm \ fmla" ("_'(_::=_')" [1000, 0, 0] 200) where eql: "(eql t u)(i::=x) = eql (subst i x t) (subst i x u)" | dsj: "(dsj A B)(i::=x) = dsj (A(i::=x)) (B(i::=x))" | neg: "(neg A)(i::=x) = neg (A(i::=x))" | exi: "atom j \ (i, x) \ (exi j A)(i::=x) = exi j (A(i::=x))" subgoal by (simp add: eqvt_def subst_fmla_graph_aux_def) subgoal by auto subgoal by (metis fmla.strong_exhaust fresh_star_insert old.prod.exhaust) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (simp add: eqvt_at_def fresh_star_def fresh_Pair fresh_at_base) (metis flip_at_base_simps(3) flip_fresh_fresh) . nominal_termination (eqvt) by lexicographic_order lemma size_subst_fmla [simp]: "size (A(i::=x)) = size A" by (nominal_induct A avoiding: i x rule: fmla.strong_induct) auto lemma forget_subst_fmla [simp]: "atom a \ A \ A(a::=x) = A" by (nominal_induct A avoiding: a x rule: fmla.strong_induct) (auto simp: fresh_at_base) lemma subst_fmla_id [simp]: "A(a::=Var a) = A" by (nominal_induct A avoiding: a rule: fmla.strong_induct) (auto simp: fresh_at_base) lemma fresh_subst_fmla_if [simp]: "j \ (A(i::=x)) \ (atom i \ A \ j \ A) \ (j \ x \ (j \ A \ j = atom i))" by (nominal_induct A avoiding: i x rule: fmla.strong_induct) (auto simp: fresh_at_base) lemma subst_fmla_commute [simp]: "atom j \ A \ (A(i::=t))(j::=u) = A(i ::= subst j u t)" by (nominal_induct A avoiding: i j t u rule: fmla.strong_induct) (auto simp: fresh_at_base) lemma repeat_subst_fmla [simp]: "(A(i::=t))(i::=u) = A(i ::= subst i u t)" by (nominal_induct A avoiding: i t u rule: fmla.strong_induct) auto lemma subst_fmla_exi_with_renaming: "atom i' \ (A, i, j, t) \ (exi i A)(j ::= t) = exi i' (((i \ i') \ A)(j ::= t))" by (rule subst [of "exi i' ((i \ i') \ A)" "exi i A"]) (auto simp: Abs1_eq_iff flip_def swap_commute) text \the simplifier cannot apply the rule above, because it introduces a new variable at the right hand side.\ lemma flip_subst_trm: "atom y \ t \ (x \ y) \ t = subst x (Var y) t" apply(nominal_induct t avoiding: x y rule: trm.strong_induct) by auto lemma flip_subst_fmla: "atom y \ \ \ (x \ y) \ \ = \(x::=Var y)" apply(nominal_induct \ avoiding: x y rule: fmla.strong_induct) apply (auto simp: flip_subst_trm) using fresh_at_base(2) by blast lemma exi_ren_subst_fresh: "atom y \ \ \ exi x \ = exi y (\(x::=Var y))" using flip_subst_fmla by auto subsection\Semantics\ definition e0 :: "(name, nat) finfun" \ \the null environment\ where "e0 \ finfun_const 0" nominal_function eval_trm :: "(name, nat) finfun \ trm \ nat" where "eval_trm e zer = 0" | "eval_trm e (Var k) = finfun_apply e k" | "eval_trm e (suc t) = Suc (eval_trm e t)" | "eval_trm e (pls t u) = eval_trm e t + eval_trm e u" | "eval_trm e (tms t u) = eval_trm e t * eval_trm e u" by (auto simp: eqvt_def eval_trm_graph_aux_def) (metis trm.strong_exhaust) nominal_termination (eqvt) by lexicographic_order nominal_function eval_fmla :: "(name, nat) finfun \ fmla \ bool" where "eval_fmla e (t EQ u) \ eval_trm e t = eval_trm e u" | "eval_fmla e (A OR B) \ eval_fmla e A \ eval_fmla e B" | "eval_fmla e (neg A) \ (~ eval_fmla e A)" | "atom k \ e \ eval_fmla e (exi k A) \ (\x. eval_fmla (finfun_update e k x) A)" +supply [[simproc del: defined_all]] apply(simp add: eqvt_def eval_fmla_graph_aux_def) apply(auto del: iffI) [11] apply(rule_tac y=b and c="(a)" in fmla.strong_exhaust) apply(auto simp: fresh_star_def)[4] using [[simproc del: alpha_lst]] apply clarsimp apply(erule_tac c="(ea)" in Abs_lst1_fcb2') apply(rule pure_fresh) apply(simp add: fresh_star_def) apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq) done nominal_termination (eqvt) by lexicographic_order lemma eval_trm_rename: assumes "atom k' \ t" shows "eval_trm (finfun_update e k x) t = eval_trm (finfun_update e k' x) ((k' \ k) \ t)" using assms by (induct t rule: trm.induct) (auto simp: permute_flip_at) lemma eval_fmla_rename: assumes "atom k' \ A" shows "eval_fmla (finfun_update e k x) A = eval_fmla (finfun_update e k' x) ((k' \ k) \ A)" using assms apply (nominal_induct A avoiding: e k k' x rule: fmla.strong_induct) apply (simp_all add: eval_trm_rename[symmetric], metis) apply (simp add: fresh_finfun_update fresh_at_base finfun_update_twist) done lemma better_ex_eval_fmla[simp]: "eval_fmla e (exi k A) \ (\x. eval_fmla (finfun_update e k x) A)" proof - obtain k'::name where k': "atom k' \ (k, e, A)" by (rule obtain_fresh) then have eq: "exi k' ((k' \ k) \ A) = exi k A" by (simp add: Abs1_eq_iff flip_def) have "eval_fmla e (exi k' ((k' \ k) \ A)) = (\x. eval_fmla (finfun_update e k' x) ((k' \ k) \ A))" using k' by simp also have "... = (\x. eval_fmla (finfun_update e k x) A)" by (metis eval_fmla_rename k' fresh_Pair) finally show ?thesis by (metis eq) qed lemma forget_eval_trm [simp]: "atom i \ t \ eval_trm (finfun_update e i x) t = eval_trm e t" by (induct t rule: trm.induct) (simp_all add: fresh_at_base) lemma forget_eval_fmla [simp]: "atom k \ A \ eval_fmla (finfun_update e k x) A = eval_fmla e A" by (nominal_induct A avoiding: k e rule: fmla.strong_induct) (simp_all add: fresh_at_base finfun_update_twist) lemma eval_subst_trm: "eval_trm e (subst i t u) = eval_trm (finfun_update e i (eval_trm e t)) u" by (induct u rule: trm.induct) (auto) lemma eval_subst_fmla: "eval_fmla e (fmla(i::= t)) = eval_fmla (finfun_update e i (eval_trm e t)) fmla" by (nominal_induct fmla avoiding: i t e rule: fmla.strong_induct) (simp_all add: eval_subst_trm finfun_update_twist fresh_at_base) subsection \Derived logical connectives\ abbreviation imp :: "fmla \ fmla \ fmla" (infixr "IMP" 125) where "imp A B \ dsj (neg A) B" abbreviation all :: "name \ fmla \ fmla" where "all i A \ neg (exi i (neg A))" subsubsection \Conjunction\ definition cnj :: "fmla \ fmla \ fmla" (infixr "AND" 135) where "cnj A B \ neg (dsj (neg A) (neg B))" lemma cnj_eqvt [eqvt]: "p \ (A AND B) = (p \ A) AND (p \ B)" by (simp add: cnj_def) lemma fresh_cnj [simp]: "a \ A AND B \ (a \ A \ a \ B)" by (auto simp: cnj_def) lemma supp_cnj [simp]: "supp (A AND B) = supp A \ supp B" by (auto simp: cnj_def) lemma size_cnj [simp]: "size (A AND B) = size A + size B + 4" by (simp add: cnj_def) lemma cnj_injective_iff [iff]: "(A AND B) = (A' AND B') \ (A = A' \ B = B')" by (auto simp: cnj_def) lemma subst_fmla_cnj [simp]: "(A AND B)(i::=x) = (A(i::=x)) AND (B(i::=x))" by (auto simp: cnj_def) lemma eval_fmla_cnj [simp]: "eval_fmla e (cnj A B) \ (eval_fmla e A \ eval_fmla e B)" by (auto simp: cnj_def) subsubsection \If and only if\ definition Iff :: "fmla \ fmla \ fmla" (infixr "IFF" 125) where "Iff A B = cnj (imp A B) (imp B A)" lemma Iff_eqvt [eqvt]: "p \ (A IFF B) = (p \ A) IFF (p \ B)" by (simp add: Iff_def) lemma fresh_Iff [simp]: "a \ A IFF B \ (a \ A \ a \ B)" by (auto simp: cnj_def Iff_def) lemma size_Iff [simp]: "size (A IFF B) = 2*(size A + size B) + 8" by (simp add: Iff_def) lemma Iff_injective_iff [iff]: "(A IFF B) = (A' IFF B') \ (A = A' \ B = B')" by (auto simp: Iff_def) lemma subst_fmla_Iff [simp]: "(A IFF B)(i::=x) = (A(i::=x)) IFF (B(i::=x))" by (auto simp: Iff_def) lemma eval_fmla_Iff [simp]: "eval_fmla e (Iff A B) \ (eval_fmla e A \ eval_fmla e B)" by (auto simp: Iff_def) subsubsection \False\ definition fls where "fls \ neg (zer EQ zer)" lemma fls_eqvt [eqvt]: "(p \ fls) = fls" by (simp add: fls_def) lemma fls_fresh [simp]: "a \ fls" by (simp add: fls_def) section \Axioms and Theorems\ subsection \Logical axioms\ inductive_set boolean_axioms :: "fmla set" where Ident: "A IMP A \ boolean_axioms" | dsjI1: "A IMP (A OR B) \ boolean_axioms" | dsjCont: "(A OR A) IMP A \ boolean_axioms" | dsjAssoc: "(A OR (B OR C)) IMP ((A OR B) OR C) \ boolean_axioms" | dsjcnj: "(C OR A) IMP (((neg C) OR B) IMP (A OR B)) \ boolean_axioms" lemma boolean_axioms_hold: "A \ boolean_axioms \ eval_fmla e A" by (induct rule: boolean_axioms.induct, auto) inductive_set special_axioms :: "fmla set" where I: "A(i::=x) IMP (exi i A) \ special_axioms" lemma special_axioms_hold: "A \ special_axioms \ eval_fmla e A" by (induct rule: special_axioms.induct, auto) (metis eval_subst_fmla) lemma twist_forget_eval_fmla [simp]: "atom j \ (i, A) \ eval_fmla (finfun_update (finfun_update (finfun_update e i x) j y) i z) A = eval_fmla (finfun_update e i z) A" by (metis finfun_update_twice finfun_update_twist forget_eval_fmla fresh_Pair) subsection \Concrete variables\ declare Abs_name_inject[simp] abbreviation "X0 \ Abs_name (Atom (Sort ''Theory_Syntax_Q.name'' []) 0)" abbreviation "X1 \ Abs_name (Atom (Sort ''Robinson_Arithmetic.name'' []) (Suc 0))" \ \We prefer @{term "Suc 0"} because simplification will transform 1 to that form anyway.\ abbreviation "X2 \ Abs_name (Atom (Sort ''Robinson_Arithmetic.name'' []) 2)" abbreviation "X3 \ Abs_name (Atom (Sort ''Robinson_Arithmetic.name'' []) 3)" abbreviation "X4 \ Abs_name (Atom (Sort ''Robinson_Arithmetic.name'' []) 4)" subsection \Equality axioms\ definition refl_ax :: fmla where "refl_ax = Var X1 EQ Var X1" lemma refl_ax_holds: "eval_fmla e refl_ax" by (auto simp: refl_ax_def) definition eq_cong_ax :: fmla where "eq_cong_ax = ((Var X1 EQ Var X2) AND (Var X3 EQ Var X4)) IMP ((Var X1 EQ Var X3) IMP (Var X2 EQ Var X4))" lemma eq_cong_ax_holds: "eval_fmla e eq_cong_ax" by (auto simp: cnj_def eq_cong_ax_def) definition syc_cong_ax :: fmla where "syc_cong_ax = ((Var X1 EQ Var X2)) IMP ((suc (Var X1)) EQ (suc (Var X2)))" lemma syc_cong_ax_holds: "eval_fmla e syc_cong_ax" by (auto simp: cnj_def syc_cong_ax_def) definition pls_cong_ax :: fmla where "pls_cong_ax = ((Var X1 EQ Var X2) AND (Var X3 EQ Var X4)) IMP ((pls (Var X1) (Var X3)) EQ (pls (Var X2) (Var X4)))" lemma pls_cong_ax_holds: "eval_fmla e pls_cong_ax" by (auto simp: cnj_def pls_cong_ax_def) definition tms_cong_ax :: fmla where "tms_cong_ax = ((Var X1 EQ Var X2) AND (Var X3 EQ Var X4)) IMP ((tms (Var X1) (Var X3)) EQ (tms (Var X2) (Var X4)))" lemma tms_cong_ax_holds: "eval_fmla e tms_cong_ax" by (auto simp: cnj_def tms_cong_ax_def) definition equality_axioms :: "fmla set" where "equality_axioms = {refl_ax, eq_cong_ax, syc_cong_ax, pls_cong_ax, tms_cong_ax}" lemma equality_axioms_hold: "A \ equality_axioms \ eval_fmla e A" by (auto simp: equality_axioms_def refl_ax_holds eq_cong_ax_holds syc_cong_ax_holds pls_cong_ax_holds tms_cong_ax_holds) subsection \The Q (Robinson-arithmetic-specific) axioms\ definition "Q_axioms \ {A | A X1 X2. X1 \ X2 \ (A = neg (zer EQ suc (Var X1)) \ A = suc (Var X1) EQ suc (Var X2) IMP Var X1 EQ Var X2 \ A = Var X2 EQ zer OR exi X1 (Var X2 EQ suc (Var X1)) \ A = pls (Var X1) zer EQ Var X1 \ A = pls (Var X1) (suc (Var X2)) EQ suc (pls (Var X1) (Var X2)) \ A = tms (Var X1) zer EQ zer \ A = tms (Var X1) (suc (Var X2)) EQ pls (tms (Var X1) (Var X2)) (Var X1))}" subsection \The proof system\ inductive nprv :: "fmla set \ fmla \ bool" (infixl "\" 55) where Hyp: "A \ H \ H \ A" | Q: "A \ Q_axioms \ H \ A" | Bool: "A \ boolean_axioms \ H \ A" | eql: "A \ equality_axioms \ H \ A" | Spec: "A \ special_axioms \ H \ A" | MP: "H \ A IMP B \ H' \ A \ H \ H' \ B" | exiists: "H \ A IMP B \ atom i \ B \ \C \ H. atom i \ C \ H \ (exi i A) IMP B" subsection\Derived rules of inference\ lemma contraction: "insert A (insert A H) \ B \ insert A H \ B" by (metis insert_absorb2) lemma thin_Un: "H \ A \ H \ H' \ A" by (metis Bool MP boolean_axioms.Ident sup_commute) lemma thin: "H \ A \ H \ H' \ H' \ A" by (metis Un_absorb1 thin_Un) lemma thin0: "{} \ A \ H \ A" by (metis sup_bot_left thin_Un) lemma thin1: "H \ B \ insert A H \ B" by (metis subset_insertI thin) lemma thin2: "insert A1 H \ B \ insert A1 (insert A2 H) \ B" by (blast intro: thin) lemma thin3: "insert A1 (insert A2 H) \ B \ insert A1 (insert A2 (insert A3 H)) \ B" by (blast intro: thin) lemma thin4: "insert A1 (insert A2 (insert A3 H)) \ B \ insert A1 (insert A2 (insert A3 (insert A4 H))) \ B" by (blast intro: thin) lemma rotate2: "insert A2 (insert A1 H) \ B \ insert A1 (insert A2 H) \ B" by (blast intro: thin) lemma rotate3: "insert A3 (insert A1 (insert A2 H)) \ B \ insert A1 (insert A2 (insert A3 H)) \ B" by (blast intro: thin) lemma rotate4: "insert A4 (insert A1 (insert A2 (insert A3 H))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 H))) \ B" by (blast intro: thin) lemma rotate5: "insert A5 (insert A1 (insert A2 (insert A3 (insert A4 H)))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 H)))) \ B" by (blast intro: thin) lemma rotate6: "insert A6 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 H))))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 H))))) \ B" by (blast intro: thin) lemma rotate7: "insert A7 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 H)))))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 H)))))) \ B" by (blast intro: thin) lemma rotate8: "insert A8 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 H))))))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 H))))))) \ B" by (blast intro: thin) lemma rotate9: "insert A9 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 H)))))))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 H)))))))) \ B" by (blast intro: thin) lemma rotate10: "insert A10 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 H))))))))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 H))))))))) \ B" by (blast intro: thin) lemma rotate11: "insert A11 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 H)))))))))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 H)))))))))) \ B" by (blast intro: thin) lemma rotate12: "insert A12 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 H))))))))))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 H))))))))))) \ B" by (blast intro: thin) lemma rotate13: "insert A13 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 H)))))))))))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 H)))))))))))) \ B" by (blast intro: thin) lemma rotate14: "insert A14 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 H))))))))))))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 (insert A14 H))))))))))))) \ B" by (blast intro: thin) lemma rotate15: "insert A15 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 (insert A14 H)))))))))))))) \ B \ insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 (insert A14 (insert A15 H)))))))))))))) \ B" by (blast intro: thin) lemma MP_same: "H \ A IMP B \ H \ A \ H \ B" by (metis MP Un_absorb) lemma MP_thin: "HA \ A IMP B \ HB \ A \ HA \ HB \ H \ H \ B" by (metis MP_same le_sup_iff thin) lemma MP_null: "{} \ A IMP B \ H \ A \ H \ B" by (metis MP_same thin0) lemma dsj_commute: "H \ B OR A \ H \ A OR B" using dsjcnj [of B A B] Ident [of B] by (metis Bool MP_same) lemma S: assumes "H \ A IMP (B IMP C)" "H' \ A IMP B" shows "H \ H' \ A IMP C" proof - have "H' \ H \ (neg A) OR (C OR (neg A))" by (metis Bool MP MP_same boolean_axioms.dsjcnj dsj_commute dsjAssoc assms) thus ?thesis by (metis Bool dsj_commute Un_commute MP_same dsjAssoc dsjCont dsjI1) qed lemma Assume: "insert A H \ A" by (metis Hyp insertI1) lemmas AssumeH = Assume Assume [THEN rotate2] Assume [THEN rotate3] Assume [THEN rotate4] Assume [THEN rotate5] Assume [THEN rotate6] Assume [THEN rotate7] Assume [THEN rotate8] Assume [THEN rotate9] Assume [THEN rotate10] Assume [THEN rotate11] Assume [THEN rotate12] declare AssumeH [intro!] lemma imp_triv_I: "H \ B \ H \ A IMP B" by (metis Bool dsj_commute MP_same boolean_axioms.dsjI1) lemma dsjAssoc1: "H \ A OR (B OR C) \ H \ (A OR B) OR C" by (metis Bool MP_same boolean_axioms.dsjAssoc) lemma dsjAssoc2: "H \ (A OR B) OR C \ H \ A OR (B OR C)" by (metis dsjAssoc1 dsj_commute) lemma dsj_commute_imp: "H \ (B OR A) IMP (A OR B)" using dsjcnj [of B A B] Ident [of B] by (metis Bool dsjAssoc2 dsj_commute MP_same) lemma dsj_Semicong_1: "H \ A OR C \ H \ A IMP B \ H \ B OR C" using dsjcnj [of A C B] by (metis Bool dsj_commute MP_same) lemma imp_imp_commute: "H \ B IMP (A IMP C) \ H \ A IMP (B IMP C)" by (metis dsjAssoc1 dsjAssoc2 dsj_Semicong_1 dsj_commute_imp) subsection\The deduction theorem\ lemma deduction_Diff: assumes "H \ B" shows "H - {C} \ C IMP B" using assms proof (induct) case (Hyp A H) thus ?case by (metis Bool imp_triv_I boolean_axioms.Ident nprv.Hyp member_remove remove_def) next case (Q H) thus ?case by (metis imp_triv_I nprv.Q) next case (Bool A H) thus ?case by (metis imp_triv_I nprv.Bool) next case (eql A H) thus ?case by (metis imp_triv_I nprv.eql) next case (Spec A H) thus ?case by (metis imp_triv_I nprv.Spec) next case (MP H A B H') hence "(H-{C}) \ (H'-{C}) \ imp C B" by (simp add: S) thus ?case by (metis Un_Diff) next case (exiists H A B i) show ?case proof (cases "C \ H") case True hence "atom i \ C" using exiists by auto moreover have "H - {C} \ A IMP C IMP B" using exiists by (metis imp_imp_commute) ultimately have "H - {C} \ (exi i A) IMP C IMP B" using exiists using nprv.eql by (simp add: nprv.exiists) thus ?thesis by (metis imp_imp_commute) next case False hence "H - {C} = H" by auto thus ?thesis using exiists by (metis imp_triv_I nprv.exiists) qed qed theorem imp_I [intro!]: "insert A H \ B \ H \ A IMP B" by (metis Diff_insert_absorb imp_triv_I deduction_Diff insert_absorb) lemma anti_deduction: "H \ A IMP B \ insert A H \ B" by (metis Assume MP_same thin1) subsection\Cut rules\ lemma cut: "H \ A \ insert A H' \ B \ H \ H' \ B" by (metis MP Un_commute imp_I) lemma cut_same: "H \ A \ insert A H \ B \ H \ B" by (metis Un_absorb cut) lemma cut_thin: "HA \ A \ insert A HB \ B \ HA \ HB \ H \ H \ B" by (metis thin cut) lemma cut0: "{} \ A \ insert A H \ B \ H \ B" by (metis cut_same thin0) lemma cut1: "{A} \ B \ H \ A \ H \ B" by (metis cut sup_bot_right) lemma rcut1: "{A} \ B \ insert B H \ C \ insert A H \ C" by (metis Assume cut1 cut_same rotate2 thin1) lemma cut2: "\{A,B} \ C; H \ A; H \ B\ \ H \ C" by (metis Un_empty_right Un_insert_right cut cut_same) lemma rcut2: "{A,B} \ C \ insert C H \ D \ H \ B \ insert A H \ D" by (metis Assume cut2 cut_same insert_commute thin1) lemma cut3: "\{A,B,C} \ D; H \ A; H \ B; H \ C\ \ H \ D" by (metis MP_same cut2 imp_I) lemma cut4: "\{A,B,C,D} \ E; H \ A; H \ B; H \ C; H \ D\ \ H \ E" by (metis MP_same cut3 [of B C D] imp_I) section\Miscellaneous Logical Rules\ lemma dsj_I1: "H \ A \ H \ A OR B" by (metis Bool MP_same boolean_axioms.dsjI1) lemma dsj_I2: "H \ B \ H \ A OR B" by (metis dsj_commute dsj_I1) lemma Peirce: "H \ (neg A) IMP A \ H \ A" using dsjcnj [of "neg A" A A] dsjCont [of A] by (metis Bool MP_same boolean_axioms.Ident) lemma Contra: "insert (neg A) H \ A \ H \ A" by (metis Peirce imp_I) lemma imp_neg_I: "H \ A IMP B \ H \ A IMP (neg B) \ H \ neg A" by (metis dsjcnj [of B "neg A" "neg A"] dsjCont Bool dsj_commute MP_same) lemma negneg_I: "H \ A \ H \ neg (neg A)" using dsjcnj [of "neg (neg A)" "neg A" "neg (neg A)"] by (metis Bool Ident MP_same) lemma negneg_D: "H \ neg (neg A) \ H \ A" by (metis dsj_I1 Peirce) lemma neg_D: "H \ neg A \ H \ A \ H \ B" by (metis imp_neg_I imp_triv_I negneg_D) lemma dsj_neg_1: "H \ A OR B \ H \ neg B \ H \ A" by (metis dsj_I1 dsj_Semicong_1 dsj_commute Peirce) lemma dsj_neg_2: "H \ A OR B \ H \ neg A \ H \ B" by (metis dsj_neg_1 dsj_commute) lemma neg_dsj_I: "H \ neg A \ H \ neg B \ H \ neg (A OR B)" by (metis Bool dsj_neg_1 MP_same boolean_axioms.Ident dsjAssoc) lemma cnj_I [intro!]: "H \ A \ H \ B \ H \ A AND B" by (metis cnj_def negneg_I neg_dsj_I) lemma cnj_E1: "H \ A AND B \ H \ A" by (metis cnj_def Bool dsj_neg_1 negneg_D boolean_axioms.dsjI1) lemma cnj_E2: "H \ A AND B \ H \ B" by (metis cnj_def Bool dsj_I2 dsj_neg_2 MP_same dsjAssoc Ident) lemma cnj_commute: "H \ B AND A \ H \ A AND B" by (metis cnj_E1 cnj_E2 cnj_I) lemma cnj_E: assumes "insert A (insert B H) \ C" shows "insert (A AND B) H \ C" apply (rule cut_same [where A=A], metis cnj_E1 Hyp insertI1) by (metis (full_types) AssumeH(2) cnj_E2 assms cut_same [where A=B] insert_commute thin2) lemmas cnj_EH = cnj_E cnj_E [THEN rotate2] cnj_E [THEN rotate3] cnj_E [THEN rotate4] cnj_E [THEN rotate5] cnj_E [THEN rotate6] cnj_E [THEN rotate7] cnj_E [THEN rotate8] cnj_E [THEN rotate9] cnj_E [THEN rotate10] declare cnj_EH [intro!] lemma neg_I0: assumes "(\B. atom i \ B \ insert A H \ B)" shows "H \ neg A" by (meson fls_fresh imp_I imp_neg_I assms fmla.fresh(3)) lemma neg_mono: "insert A H \ B \ insert (neg B) H \ neg A" by (rule neg_I0) (metis Hyp neg_D insert_commute insertI1 thin1) lemma cnj_mono: "insert A H \ B \ insert C H \ D \ insert (A AND C) H \ B AND D" by (metis cnj_E1 cnj_E2 cnj_I Hyp Un_absorb2 cut insertI1 subset_insertI) lemma dsj_mono: assumes "insert A H \ B" "insert C H \ D" shows "insert (A OR C) H \ B OR D" proof - { fix A B C H have "insert (A OR C) H \ (A IMP B) IMP C OR B" by (metis Bool Hyp MP_same boolean_axioms.dsjcnj insertI1) hence "insert A H \ B \ insert (A OR C) H \ C OR B" by (metis MP_same Un_absorb Un_insert_right imp_I thin_Un) } thus ?thesis by (metis cut_same assms thin2) qed lemma dsj_E: assumes A: "insert A H \ C" and B: "insert B H \ C" shows "insert (A OR B) H \ C" by (metis A B dsj_mono negneg_I Peirce) lemmas dsj_EH = dsj_E dsj_E [THEN rotate2] dsj_E [THEN rotate3] dsj_E [THEN rotate4] dsj_E [THEN rotate5] dsj_E [THEN rotate6] dsj_E [THEN rotate7] dsj_E [THEN rotate8] dsj_E [THEN rotate9] dsj_E [THEN rotate10] declare dsj_EH [intro!] lemma Contra': "insert A H \ neg A \ H \ neg A" by (metis Contra neg_mono) lemma negneg_E [intro!]: "insert A H \ B \ insert (neg (neg A)) H \ B" by (metis negneg_D neg_mono) declare negneg_E [THEN rotate2, intro!] declare negneg_E [THEN rotate3, intro!] declare negneg_E [THEN rotate4, intro!] declare negneg_E [THEN rotate5, intro!] declare negneg_E [THEN rotate6, intro!] declare negneg_E [THEN rotate7, intro!] declare negneg_E [THEN rotate8, intro!] lemma imp_E: assumes A: "H \ A" and B: "insert B H \ C" shows "insert (A IMP B) H \ C" proof - have "insert (A IMP B) H \ B" by (metis Hyp A thin1 MP_same insertI1) thus ?thesis by (metis cut [where B=C] Un_insert_right sup_commute sup_idem B) qed lemma imp_cut: assumes "insert C H \ A IMP B" "{A} \ C" shows "H \ A IMP B" by (metis Contra dsj_I1 neg_mono assms rcut1) lemma Iff_I [intro!]: "insert A H \ B \ insert B H \ A \ H \ A IFF B" by (metis Iff_def cnj_I imp_I) lemma Iff_MP_same: "H \ A IFF B \ H \ A \ H \ B" by (metis Iff_def cnj_E1 MP_same) lemma Iff_MP2_same: "H \ A IFF B \ H \ B \ H \ A" by (metis Iff_def cnj_E2 MP_same) lemma Iff_refl [intro!]: "H \ A IFF A" by (metis Hyp Iff_I insertI1) lemma Iff_sym: "H \ A IFF B \ H \ B IFF A" by (metis Iff_def cnj_commute) lemma Iff_trans: "H \ A IFF B \ H \ B IFF C \ H \ A IFF C" unfolding Iff_def by (metis cnj_E1 cnj_E2 cnj_I dsj_Semicong_1 dsj_commute) lemma Iff_E: "insert A (insert B H) \ C \ insert (neg A) (insert (neg B) H) \ C \ insert (A IFF B) H \ C" by (simp add: Assume Iff_def anti_deduction cnj_E dsj_EH(2) dsj_I1 insert_commute) lemma Iff_E1: assumes A: "H \ A" and B: "insert B H \ C" shows "insert (A IFF B) H \ C" by (metis Iff_def A B cnj_E imp_E insert_commute thin1) lemma Iff_E2: assumes A: "H \ A" and B: "insert B H \ C" shows "insert (B IFF A) H \ C" by (metis Iff_def A B Bool cnj_E2 cnj_mono imp_E boolean_axioms.Ident) lemma Iff_MP_left: "H \ A IFF B \ insert A H \ C \ insert B H \ C" by (metis Hyp Iff_E2 cut_same insertI1 insert_commute thin1) lemma Iff_MP_left': "H \ A IFF B \ insert B H \ C \ insert A H \ C" by (metis Iff_MP_left Iff_sym) lemma Swap: "insert (neg B) H \ A \ insert (neg A) H \ B" by (metis negneg_D neg_mono) lemma Cases: "insert A H \ B \ insert (neg A) H \ B \ H \ B" by (metis Contra neg_D neg_mono) lemma neg_cnj_E: "H \ B \ insert (neg A) H \ C \ insert (neg (A AND B)) H \ C" by (metis cnj_I Swap thin1) lemma dsj_CI: "insert (neg B) H \ A \ H \ A OR B" by (metis Contra dsj_I1 dsj_I2 Swap) lemma dsj_3I: "insert (neg A) (insert (neg C) H) \ B \ H \ A OR B OR C" by (metis dsj_CI dsj_commute insert_commute) lemma Contrapos1: "H \ A IMP B \ H \ neg B IMP neg A" by (metis Bool MP_same boolean_axioms.dsjcnj boolean_axioms.Ident) lemma Contrapos2: "H \ (neg B) IMP (neg A) \ H \ A IMP B" by (metis Bool MP_same boolean_axioms.dsjcnj boolean_axioms.Ident) lemma ContraAssumeN [intro]: "B \ H \ insert (neg B) H \ A" by (metis Hyp Swap thin1) lemma ContraAssume: "neg B \ H \ insert B H \ A" by (metis dsj_I1 Hyp anti_deduction) lemma ContraProve: "H \ B \ insert (neg B) H \ A" by (metis Swap thin1) lemma dsj_IE1: "insert B H \ C \ insert (A OR B) H \ A OR C" by (metis Assume dsj_mono) lemmas dsj_IE1H = dsj_IE1 dsj_IE1 [THEN rotate2] dsj_IE1 [THEN rotate3] dsj_IE1 [THEN rotate4] dsj_IE1 [THEN rotate5] dsj_IE1 [THEN rotate6] dsj_IE1 [THEN rotate7] dsj_IE1 [THEN rotate8] declare dsj_IE1H [intro!] subsection\Quantifier reasoning\ lemma exi_I: "H \ A(i::=x) \ H \ exi i A" by (metis MP_same Spec special_axioms.intros) lemma exi_E: assumes "insert A H \ B" "atom i \ B" "\C \ H. atom i \ C" shows "insert (exi i A) H \ B" by (metis exiists imp_I anti_deduction assms) lemma exi_E_with_renaming: assumes "insert ((i \ i') \ A) H \ B" "atom i' \ (A,i,B)" "\C \ H. atom i' \ C" shows "insert (exi i A) H \ B" proof - have "exi i A = exi i' ((i \ i') \ A)" using assms using flip_subst_fmla by auto thus ?thesis by (metis exi_E assms fresh_Pair) qed lemmas exi_EH = exi_E exi_E [THEN rotate2] exi_E [THEN rotate3] exi_E [THEN rotate4] exi_E [THEN rotate5] exi_E [THEN rotate6] exi_E [THEN rotate7] exi_E [THEN rotate8] exi_E [THEN rotate9] exi_E [THEN rotate10] declare exi_EH [intro!] lemma exi_mono: "insert A H \ B \ \C \ H. atom i \ C \ insert (exi i A) H \ (exi i B)" by (auto simp add: intro: exi_I [where x="Var i"]) lemma all_I [intro!]: "H \ A \ \C \ H. atom i \ C \ H \ all i A" by (auto intro: ContraProve neg_I0) lemma all_D: "H \ all i A \ H \ A(i::=x)" by (metis Assume exi_I negneg_D neg_mono neg cut_same) lemma all_E: "insert (A(i::=x)) H \ B \ insert (all i A) H \ B" by (metis exi_I negneg_D neg_mono neg) lemma all_E': "H \ all i A \ insert (A(i::=x)) H \ B \ H \ B" by (metis all_D cut_same) subsection\Congruence rules\ lemma neg_cong: "H \ A IFF A' \ H \ neg A IFF neg A'" by (metis Iff_def cnj_E1 cnj_E2 cnj_I Contrapos1) lemma dsj_cong: "H \ A IFF A' \ H \ B IFF B' \ H \ A OR B IFF A' OR B'" by (metis cnj_E1 cnj_E2 dsj_mono Iff_I Iff_def anti_deduction) lemma cnj_cong: "H \ A IFF A' \ H \ B IFF B' \ H \ A AND B IFF A' AND B'" by (metis cnj_def dsj_cong neg_cong) lemma imp_cong: "H \ A IFF A' \ H \ B IFF B' \ H \ (A IMP B) IFF (A' IMP B')" by (metis dsj_cong neg_cong) lemma Iff_cong: "H \ A IFF A' \ H \ B IFF B' \ H \ (A IFF B) IFF (A' IFF B')" by (metis Iff_def cnj_cong imp_cong) lemma exi_cong: "H \ A IFF A' \ \C \ H. atom i \ C \ H \ (exi i A) IFF (exi i A')" apply (rule Iff_I) apply (metis exi_mono Hyp Iff_MP_same Un_absorb Un_insert_right insertI1 thin_Un) apply (metis exi_mono Hyp Iff_MP2_same Un_absorb Un_insert_right insertI1 thin_Un) done lemma all_cong: "H \ A IFF A' \ \C \ H. atom i \ C \ H \ (all i A) IFF (all i A')" by (metis exi_cong neg_cong) lemma Subst: "H \ A \ \B \ H. atom i \ B \ H \ A (i::=x)" by (metis all_D all_I) section\Eqluality Reasoning\ subsection\The congruence property for @{term eql}, and other basic properties of equality\ lemma eql_cong1: "{} \ (t EQ t' AND u EQ u') IMP (t EQ u IMP t' EQ u')" proof - obtain v2::name and v3::name and v4::name where v2: "atom v2 \ (t,X1,X3,X4)" and v3: "atom v3 \ (t,t',X1,v2,X4)" and v4: "atom v4 \ (t,t',u,X1,v2,v3)" by (metis obtain_fresh) have "{} \ (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (Var X1 EQ Var X3 IMP Var X2 EQ Var X4)" by (rule eql) (simp add: eq_cong_ax_def equality_axioms_def) hence "{} \ (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (Var X1 EQ Var X3 IMP Var X2 EQ Var X4)" by (drule_tac i=X1 and x="Var X1" in Subst) simp_all hence "{} \ (Var X1 EQ Var v2 AND Var X3 EQ Var X4) IMP (Var X1 EQ Var X3 IMP Var v2 EQ Var X4)" by (drule_tac i=X2 and x="Var v2" in Subst) simp_all hence "{} \ (Var X1 EQ Var v2 AND Var v3 EQ Var X4) IMP (Var X1 EQ Var v3 IMP Var v2 EQ Var X4)" using v2 by (drule_tac i=X3 and x="Var v3" in Subst) simp_all hence "{} \ (Var X1 EQ Var v2 AND Var v3 EQ Var v4) IMP (Var X1 EQ Var v3 IMP Var v2 EQ Var v4)" using v2 v3 by (drule_tac i=X4 and x="Var v4" in Subst) simp_all hence "{} \ (t EQ Var v2 AND Var v3 EQ Var v4) IMP (t EQ Var v3 IMP Var v2 EQ Var v4)" using v2 v3 v4 by (drule_tac i=X1 and x=t in Subst) simp_all hence "{} \ (t EQ t' AND Var v3 EQ Var v4) IMP (t EQ Var v3 IMP t' EQ Var v4)" using v2 v3 v4 by (drule_tac i=v2 and x="t'" in Subst) simp_all hence "{} \ (t EQ t' AND u EQ Var v4) IMP (t EQ u IMP t' EQ Var v4)" using v3 v4 by (drule_tac i=v3 and x=u in Subst) simp_all thus ?thesis using v4 by (drule_tac i=v4 and x="u'" in Subst) simp_all qed lemma Refl [iff]: "H \ t EQ t" proof - have "{} \ Var X1 EQ Var X1" by (rule eql) (simp add: equality_axioms_def refl_ax_def) hence "{} \ t EQ t" by (drule_tac i=X1 and x=t in Subst) simp_all thus ?thesis by (metis empty_subsetI thin) qed text\Apparently necessary in order to prove the congruence property.\ lemma Sym: assumes "H \ t EQ u" shows "H \ u EQ t" proof - have "{} \ (t EQ u AND t EQ t) IMP (t EQ t IMP u EQ t)" by (rule eql_cong1) moreover have "{t EQ u} \ t EQ u AND t EQ t" by (metis Assume cnj_I Refl) ultimately have "{t EQ u} \ u EQ t" by (metis MP_same MP Refl sup_bot_left) thus "H \ u EQ t" by (metis assms cut1) qed lemma Sym_L: "insert (t EQ u) H \ A \ insert (u EQ t) H \ A" by (metis Assume Sym Un_empty_left Un_insert_left cut) lemma Trans: assumes "H \ x EQ y" "H \ y EQ z" shows "H \ x EQ z" proof - have "\H. H \ (x EQ x AND y EQ z) IMP (x EQ y IMP x EQ z)" by (metis eql_cong1 bot_least thin) moreover have "{x EQ y, y EQ z} \ x EQ x AND y EQ z" by (metis Assume cnj_I Refl thin1) ultimately have "{x EQ y, y EQ z} \ x EQ z" by (metis Hyp MP_same insertI1) thus ?thesis by (metis assms cut2) qed lemma eql_cong: assumes "H \ t EQ t'" "H \ u EQ u'" shows "H \ t EQ u IFF t' EQ u'" proof - { fix t t' u u' assume "H \ t EQ t'" "H \ u EQ u'" moreover have "{t EQ t', u EQ u'} \ t EQ u IMP t' EQ u'" using eql_cong1 by (metis Assume cnj_I MP_null insert_commute) ultimately have "H \ t EQ u IMP t' EQ u'" by (metis cut2) } thus ?thesis by (metis Iff_def cnj_I assms Sym) qed lemma eql_Trans_E: "H \ x EQ u \ insert (t EQ u) H \ A \ insert (x EQ t) H \ A" by (metis Assume Sym_L Trans cut_same thin1 thin2) subsection\The congruence properties for @{term suc}, @{term pls} and @{term tms}\ lemma suc_cong1: "{} \ (t EQ t') IMP (suc t EQ suc t')" proof - obtain v2::name and v3::name and v4::name where v2: "atom v2 \ (t,X1,X3,X4)" and v3: "atom v3 \ (t,t',X1,v2,X4)" and v4: "atom v4 \ (t,t',X1,v2,v3)" by (metis obtain_fresh) have "{} \ (Var X1 EQ Var X2) IMP (suc (Var X1) EQ suc (Var X2))" by (metis syc_cong_ax_def equality_axioms_def insert_iff eql) hence "{} \ (Var X1 EQ Var v2) IMP (suc (Var X1) EQ suc (Var v2))" by (drule_tac i=X2 and x="Var v2" in Subst) simp_all hence "{} \ (t EQ Var v2) IMP (suc t EQ suc (Var v2))" using v2 v3 v4 by (drule_tac i=X1 and x=t in Subst) simp_all hence "{} \ (t EQ t') IMP (suc t EQ suc t')" using v2 v3 v4 by (drule_tac i=v2 and x=t' in Subst) simp_all thus ?thesis using v4 by (drule_tac i=v4 in Subst) simp_all qed lemma suc_cong: "\H \ t EQ t'\ \ H \ suc t EQ suc t'" by (metis anti_deduction suc_cong1 cut1) lemma pls_cong1: "{} \ (t EQ t' AND u EQ u') IMP (pls t u EQ pls t' u')" proof - obtain v2::name and v3::name and v4::name where v2: "atom v2 \ (t,X1,X3,X4)" and v3: "atom v3 \ (t,t',X1,v2,X4)" and v4: "atom v4 \ (t,t',u,X1,v2,v3)" by (metis obtain_fresh) have "{} \ (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (pls (Var X1) (Var X3) EQ pls (Var X2) (Var X4))" by (metis pls_cong_ax_def equality_axioms_def insert_iff eql) hence "{} \ (Var X1 EQ Var v2 AND Var X3 EQ Var X4) IMP (pls (Var X1) (Var X3) EQ pls (Var v2) (Var X4))" by (drule_tac i=X2 and x="Var v2" in Subst) simp_all hence "{} \ (Var X1 EQ Var v2 AND Var v3 EQ Var X4) IMP (pls (Var X1) (Var v3) EQ pls (Var v2) (Var X4))" using v2 by (drule_tac i=X3 and x="Var v3" in Subst) simp_all hence "{} \ (Var X1 EQ Var v2 AND Var v3 EQ Var v4) IMP (pls (Var X1) (Var v3) EQ pls (Var v2) (Var v4))" using v2 v3 by (drule_tac i=X4 and x="Var v4" in Subst) simp_all hence "{} \ (t EQ Var v2 AND Var v3 EQ Var v4) IMP (pls t (Var v3) EQ pls (Var v2) (Var v4))" using v2 v3 v4 by (drule_tac i=X1 and x=t in Subst) simp_all hence "{} \ (t EQ t' AND Var v3 EQ Var v4) IMP (pls t (Var v3) EQ pls t' (Var v4))" using v2 v3 v4 by (drule_tac i=v2 and x=t' in Subst) simp_all hence "{} \ (t EQ t' AND u EQ Var v4) IMP (pls t u EQ pls t' (Var v4))" using v3 v4 by (drule_tac i=v3 and x=u in Subst) simp_all thus ?thesis using v4 by (drule_tac i=v4 and x=u' in Subst) simp_all qed lemma pls_cong: "\H \ t EQ t'; H \ u EQ u'\ \ H \ pls t u EQ pls t' u'" by (metis cnj_I anti_deduction pls_cong1 cut1) lemma tms_cong1: "{} \ (t EQ t' AND u EQ u') IMP (tms t u EQ tms t' u')" proof - obtain v2::name and v3::name and v4::name where v2: "atom v2 \ (t,X1,X3,X4)" and v3: "atom v3 \ (t,t',X1,v2,X4)" and v4: "atom v4 \ (t,t',u,X1,v2,v3)" by (metis obtain_fresh) have "{} \ (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (tms (Var X1) (Var X3) EQ tms (Var X2) (Var X4))" by (metis tms_cong_ax_def equality_axioms_def insert_iff eql) hence "{} \ (Var X1 EQ Var v2 AND Var X3 EQ Var X4) IMP (tms (Var X1) (Var X3) EQ tms (Var v2) (Var X4))" by (drule_tac i=X2 and x="Var v2" in Subst) simp_all hence "{} \ (Var X1 EQ Var v2 AND Var v3 EQ Var X4) IMP (tms (Var X1) (Var v3) EQ tms (Var v2) (Var X4))" using v2 by (drule_tac i=X3 and x="Var v3" in Subst) simp_all hence "{} \ (Var X1 EQ Var v2 AND Var v3 EQ Var v4) IMP (tms (Var X1) (Var v3) EQ tms (Var v2) (Var v4))" using v2 v3 by (drule_tac i=X4 and x="Var v4" in Subst) simp_all hence "{} \ (t EQ Var v2 AND Var v3 EQ Var v4) IMP (tms t (Var v3) EQ tms (Var v2) (Var v4))" using v2 v3 v4 by (drule_tac i=X1 and x=t in Subst) simp_all hence "{} \ (t EQ t' AND Var v3 EQ Var v4) IMP (tms t (Var v3) EQ tms t' (Var v4))" using v2 v3 v4 by (drule_tac i=v2 and x=t' in Subst) simp_all hence "{} \ (t EQ t' AND u EQ Var v4) IMP (tms t u EQ tms t' (Var v4))" using v3 v4 by (drule_tac i=v3 and x=u in Subst) simp_all thus ?thesis using v4 by (drule_tac i=v4 and x=u' in Subst) simp_all qed lemma tms_cong: "\H \ t EQ t'; H \ u EQ u'\ \ H \ tms t u EQ tms t' u'" by (metis cnj_I anti_deduction tms_cong1 cut1) subsection\Substitution for eqlualities\ lemma eql_subst_trm_Iff: "{t EQ u} \ subst i t trm EQ subst i u trm" by (induct trm rule: trm.induct) (auto simp: suc_cong pls_cong tms_cong) lemma eql_subst_fmla_Iff: "insert (t EQ u) H \ A(i::=t) IFF A(i::=u)" proof - have "{ t EQ u } \ A(i::=t) IFF A(i::=u)" by (nominal_induct A avoiding: i t u rule: fmla.strong_induct) (auto simp: dsj_cong neg_cong exi_cong eql_cong eql_subst_trm_Iff) thus ?thesis by (metis Assume cut1) qed lemma Var_eql_subst_Iff: "insert (Var i EQ t) H \ A(i::=t) IFF A" by (metis eql_subst_fmla_Iff Iff_sym subst_fmla_id) lemma Var_eql_imp_subst_Iff: "H \ Var i EQ t \ H \ A(i::=t) IFF A" by (metis Var_eql_subst_Iff cut_same) subsection\Congruence rules for predicates\ lemma P1_cong: fixes tms :: "trm list" assumes "\i t x. atom i \ tms \ (P t)(i::=x) = P (subst i x t)" and "H \ x EQ x'" shows "H \ P x IFF P x'" proof - obtain i::name where i: "atom i \ tms" by (metis obtain_fresh) have "insert (x EQ x') H \ (P (Var i))(i::=x) IFF (P(Var i))(i::=x')" by (rule eql_subst_fmla_Iff) thus ?thesis using assms i by (metis cut_same subst.simps(2)) qed lemma P2_cong: fixes tms :: "trm list" assumes sub: "\i t u x. atom i \ tms \ (P t u)(i::=x) = P (subst i x t) (subst i x u)" and eq: "H \ x EQ x'" "H \ y EQ y'" shows "H \ P x y IFF P x' y'" proof - have yy': "{ y EQ y' } \ P x' y IFF P x' y'" by (rule P1_cong [where tms="[y,x']@tms"]) (auto simp: fresh_Cons sub) have "{ x EQ x' } \ P x y IFF P x' y" by (rule P1_cong [where tms="[y,x']@tms"]) (auto simp: fresh_Cons sub) hence "{x EQ x', y EQ y'} \ P x y IFF P x' y'" by (metis Assume Iff_trans cut1 rotate2 yy') thus ?thesis by (metis cut2 eq) qed lemma P3_cong: fixes tms :: "trm list" assumes sub: "\i t u v x. atom i \ tms \ (P t u v)(i::=x) = P (subst i x t) (subst i x u) (subst i x v)" and eq: "H \ x EQ x'" "H \ y EQ y'" "H \ z EQ z'" shows "H \ P x y z IFF P x' y' z'" proof - obtain i::name where i: "atom i \ (z,z',y,y',x,x')" by (metis obtain_fresh) have tl: "{ y EQ y', z EQ z' } \ P x' y z IFF P x' y' z'" by (rule P2_cong [where tms="[z,z',y,y',x,x']@tms"]) (auto simp: fresh_Cons sub) have hd: "{ x EQ x' } \ P x y z IFF P x' y z" by (rule P1_cong [where tms="[z,y,x']@tms"]) (auto simp: fresh_Cons sub) have "{x EQ x', y EQ y', z EQ z'} \ P x y z IFF P x' y' z'" by (metis Assume thin1 hd [THEN cut1] tl Iff_trans) thus ?thesis by (rule cut3) (rule eq)+ qed lemma P4_cong: fixes tms :: "trm list" assumes sub: "\i t1 t2 t3 t4 x. atom i \ tms \ (P t1 t2 t3 t4)(i::=x) = P (subst i x t1) (subst i x t2) (subst i x t3) (subst i x t4)" and eq: "H \ x1 EQ x1'" "H \ x2 EQ x2'" "H \ x3 EQ x3'" "H \ x4 EQ x4'" shows "H \ P x1 x2 x3 x4 IFF P x1' x2' x3' x4'" proof - obtain i::name where i: "atom i \ (x4,x4',x3,x3',x2,x2',x1,x1')" by (metis obtain_fresh) have tl: "{ x2 EQ x2', x3 EQ x3', x4 EQ x4' } \ P x1' x2 x3 x4 IFF P x1' x2' x3' x4'" by (rule P3_cong [where tms="[x4,x4',x3,x3',x2,x2',x1,x1']@tms"]) (auto simp: fresh_Cons sub) have hd: "{ x1 EQ x1' } \ P x1 x2 x3 x4 IFF P x1' x2 x3 x4" by (auto simp: fresh_Cons sub intro!: P1_cong [where tms="[x4,x3,x2,x1']@tms"]) have "{x1 EQ x1', x2 EQ x2', x3 EQ x3', x4 EQ x4'} \ P x1 x2 x3 x4 IFF P x1' x2' x3' x4'" by (metis Assume thin1 hd [THEN cut1] tl Iff_trans) thus ?thesis by (rule cut4) (rule eq)+ qed subsection\The formula @{term fls}\ lemma neg_I [intro!]: "insert A H \ fls \ H \ neg A" unfolding fls_def by (meson neg_D neg_I0 Refl) lemma neg_E [intro!]: "H \ A \ insert (neg A) H \ fls" by (rule ContraProve) declare neg_E [THEN rotate2, intro!] declare neg_E [THEN rotate3, intro!] declare neg_E [THEN rotate4, intro!] declare neg_E [THEN rotate5, intro!] declare neg_E [THEN rotate6, intro!] declare neg_E [THEN rotate7, intro!] declare neg_E [THEN rotate8, intro!] lemma neg_imp_I [intro!]: "H \ A \ insert B H \ fls \ H \ neg (A IMP B)" by (metis negneg_I neg_dsj_I neg_I) lemma neg_imp_E [intro!]: "insert (neg B) (insert A H) \ C \ insert (neg (A IMP B)) H \ C" apply (rule cut_same [where A=A]) apply (metis Assume dsj_I1 negneg_D neg_mono) apply (metis Swap imp_I rotate2 thin1) done declare neg_imp_E [THEN rotate2, intro!] declare neg_imp_E [THEN rotate3, intro!] declare neg_imp_E [THEN rotate4, intro!] declare neg_imp_E [THEN rotate5, intro!] declare neg_imp_E [THEN rotate6, intro!] declare neg_imp_E [THEN rotate7, intro!] declare neg_imp_E [THEN rotate8, intro!] lemma fls_E [intro!]: "insert fls H \ A" by (simp add: ContraProve fls_def) declare fls_E [THEN rotate2, intro!] declare fls_E [THEN rotate3, intro!] declare fls_E [THEN rotate4, intro!] declare fls_E [THEN rotate5, intro!] declare fls_E [THEN rotate6, intro!] declare fls_E [THEN rotate7, intro!] declare fls_E [THEN rotate8, intro!] lemma truth_provable: "H \ (neg fls)" by (metis fls_E neg_I) lemma exFalso: "H \ fls \ H \ A" by (metis neg_D truth_provable) text\Soundness of the provability relation\ theorem nprv_sound: assumes "H \ A" shows "(\B\H. eval_fmla e B) \ eval_fmla e A" using assms proof (induct arbitrary: e) case (Hyp A H) thus ?case by auto next case (Q H) thus ?case unfolding Q_axioms_def using not0_implies_Suc by fastforce next case (Bool A H) thus ?case by (metis boolean_axioms_hold) next case (eql A H) thus ?case by (metis equality_axioms_hold) next case (Spec A H) thus ?case by (metis special_axioms_hold) next case (MP H A B H') thus ?case by auto next case (exiists H A B i e) thus ?case by auto (metis forget_eval_fmla) qed (*<*) end (*>*)