# HG changeset patch # User wenzelm # Date 1713388952 -7200 # Node ID ef2134570abb6090fa65107661ec8c3f4ffc06e0 # Parent 8262d4f63b58844651b406547a2b7403633a83f6# Parent 68fc6839679e6bd0841cd7461f89628406926f0e merged diff -r 68fc6839679e -r ef2134570abb src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Wed Apr 17 23:12:21 2024 +0200 +++ b/src/HOL/Nominal/Nominal.thy Wed Apr 17 23:22:32 2024 +0200 @@ -1,5 +1,6 @@ theory Nominal -imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype" + imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype" + keywords "atom_decl" :: thy_decl and "nominal_datatype" :: thy_defn and @@ -726,17 +727,13 @@ and b :: "'x" assumes at: "at TYPE('x)" shows "(pi1@pi2) \ ((pi1\pi2)@pi1)" -apply(induct_tac pi2) -apply(simp add: prm_eq_def) -apply(auto simp add: prm_eq_def) -apply(simp add: at2[OF at]) -apply(drule_tac x="aa" in spec) -apply(drule sym) -apply(simp) -apply(simp add: at_append[OF at]) -apply(simp add: at2[OF at]) -apply(simp add: at_ds8_aux[OF at]) -done +proof(induct_tac pi2) + show "(pi1 @ []) \ (pi1 \ [] @ pi1)" + by(simp add: prm_eq_def) + show "\a l. (pi1 @ l) \ (pi1 \ l @ pi1) \ + (pi1 @ a # l) \ (pi1 \ (a # l) @ pi1) " + by(auto simp add: prm_eq_def at at2 at_append at_ds8_aux) +qed lemma at_ds9: fixes pi1 :: "'x prm" @@ -745,32 +742,16 @@ and b :: "'x" assumes at: "at TYPE('x)" shows " ((rev pi2)@(rev pi1)) \ ((rev pi1)@(rev (pi1\pi2)))" -apply(induct_tac pi2) -apply(simp add: prm_eq_def) -apply(auto simp add: prm_eq_def) -apply(simp add: at_append[OF at]) -apply(simp add: at2[OF at] at1[OF at]) -apply(drule_tac x="swap(pi1\a,pi1\b) aa" in spec) -apply(drule sym) -apply(simp) -apply(simp add: at_ds8_aux[OF at]) -apply(simp add: at_rev_pi[OF at]) -done + using at at_ds8 at_prm_rev_eq1 rev_append by fastforce lemma at_ds10: fixes pi :: "'x prm" and a :: "'x" and b :: "'x" - assumes at: "at TYPE('x)" - and a: "b\(rev pi)" + assumes "at TYPE('x)" + and "b\(rev pi)" shows "([(pi\a,b)]@pi) \ (pi@[(a,b)])" -using a -apply - -apply(rule at_prm_eq_trans) -apply(rule at_ds2[OF at]) -apply(simp add: at_prm_fresh[OF at] at_rev_pi[OF at]) -apply(rule at_prm_eq_refl) -done + by (metis assms at_bij1 at_ds2 at_prm_fresh) \ \there always exists an atom that is not being in a finite set\ lemma ex_in_inf: @@ -778,14 +759,7 @@ assumes at: "at TYPE('x)" and fs: "finite A" obtains c::"'x" where "c\A" -proof - - from fs at4[OF at] have "infinite ((UNIV::'x set) - A)" - by (simp add: Diff_infinite_finite) - hence "((UNIV::'x set) - A) \ ({}::'x set)" by (force simp only:) - then obtain c::"'x" where "c\((UNIV::'x set) - A)" by force - then have "c\A" by simp - then show ?thesis .. -qed + using at at4 ex_new_if_finite fs by blast text \there always exists a fresh name for an object with finite support\ lemma at_exists_fresh': @@ -806,16 +780,8 @@ fixes S::"'a set" assumes a: "at TYPE('a)" and b: "finite S" - shows "\x. x \ S" - using a b - apply(drule_tac S="UNIV::'a set" in Diff_infinite_finite) - apply(simp add: at_def) - apply(subgoal_tac "UNIV - S \ {}") - apply(simp only: ex_in_conv [symmetric]) - apply(blast) - apply(rule notI) - apply(simp) - done + shows "\x. x \ S" + by (meson a b ex_in_inf) lemma at_different: assumes at: "at TYPE('x)" @@ -823,12 +789,8 @@ proof - have "infinite (UNIV::'x set)" by (rule at4[OF at]) hence inf2: "infinite (UNIV-{a})" by (rule infinite_remove) - have "(UNIV-{a}) \ ({}::'x set)" - proof (rule_tac ccontr, drule_tac notnotD) - assume "UNIV-{a} = ({}::'x set)" - with inf2 have "infinite ({}::'x set)" by simp - then show "False" by auto - qed + have "(UNIV-{a}) \ ({}::'x set)" + by (metis finite.emptyI inf2) hence "\(b::'x). b\(UNIV-{a})" by blast then obtain b::"'x" where mem2: "b\(UNIV-{a})" by blast from mem2 have "a\b" by blast @@ -839,11 +801,7 @@ lemma at_pt_inst: assumes at: "at TYPE('x)" shows "pt TYPE('x) TYPE('x)" -apply(auto simp only: pt_def) -apply(simp only: at1[OF at]) -apply(simp only: at_append[OF at]) -apply(simp only: prm_eq_def) -done + using at at_append at_def prm_eq_def pt_def by fastforce section \finite support properties\ (*===================================*) @@ -858,56 +816,36 @@ fixes a :: "'x" assumes at: "at TYPE('x)" shows "fs TYPE('x) TYPE('x)" -apply(simp add: fs_def) -apply(simp add: at_supp[OF at]) -done + by (simp add: at at_supp fs_def) lemma fs_unit_inst: shows "fs TYPE(unit) TYPE('x)" -apply(simp add: fs_def) -apply(simp add: supp_unit) -done + by(simp add: fs_def supp_unit) lemma fs_prod_inst: assumes fsa: "fs TYPE('a) TYPE('x)" and fsb: "fs TYPE('b) TYPE('x)" shows "fs TYPE('a\'b) TYPE('x)" -apply(unfold fs_def) -apply(auto simp add: supp_prod) -apply(rule fs1[OF fsa]) -apply(rule fs1[OF fsb]) -done + by (simp add: assms fs1 supp_prod fs_def) + lemma fs_nprod_inst: assumes fsa: "fs TYPE('a) TYPE('x)" and fsb: "fs TYPE('b) TYPE('x)" shows "fs TYPE(('a,'b) nprod) TYPE('x)" -apply(unfold fs_def, rule allI) -apply(case_tac x) -apply(auto simp add: supp_nprod) -apply(rule fs1[OF fsa]) -apply(rule fs1[OF fsb]) -done + unfolding fs_def by (metis assms finite_Un fs_def nprod.exhaust supp_nprod) lemma fs_list_inst: - assumes fs: "fs TYPE('a) TYPE('x)" + assumes "fs TYPE('a) TYPE('x)" shows "fs TYPE('a list) TYPE('x)" -apply(simp add: fs_def, rule allI) -apply(induct_tac x) -apply(simp add: supp_list_nil) -apply(simp add: supp_list_cons) -apply(rule fs1[OF fs]) -done + unfolding fs_def + by (clarify, induct_tac x) (auto simp: fs1 assms supp_list_nil supp_list_cons) lemma fs_option_inst: assumes fs: "fs TYPE('a) TYPE('x)" shows "fs TYPE('a option) TYPE('x)" -apply(simp add: fs_def, rule allI) -apply(case_tac x) -apply(simp add: supp_none) -apply(simp add: supp_some) -apply(rule fs1[OF fs]) -done + unfolding fs_def + by (metis assms finite.emptyI fs1 option.exhaust supp_none supp_some) section \Lemmas about the permutation properties\ (*=================================================*) @@ -954,13 +892,10 @@ using cp by (simp add: cp_def) lemma cp_pt_inst: - assumes pt: "pt TYPE('a) TYPE('x)" - and at: "at TYPE('x)" + assumes "pt TYPE('a) TYPE('x)" + and "at TYPE('x)" shows "cp TYPE('a) TYPE('x) TYPE('x)" -apply(auto simp add: cp_def pt2[OF pt,symmetric]) -apply(rule pt3[OF pt]) -apply(rule at_ds8[OF at]) -done + using assms at_ds8 cp_def pt2 pt3 by fastforce section \disjointness properties\ (*=================================*) @@ -998,8 +933,7 @@ fixes a::"'x" assumes dj: "disjoint TYPE('x) TYPE('y)" shows "(supp a) = ({}::'y set)" -apply(simp add: supp_def dj_perm_forget[OF dj]) -done + by (simp add: supp_def dj_perm_forget[OF dj]) lemma at_fresh_ineq: fixes a :: "'x" @@ -1016,15 +950,8 @@ and ptb: "pt TYPE('b) TYPE('x)" and at: "at TYPE('x)" shows "pt TYPE('a\'b) TYPE('x)" -apply(auto simp only: pt_def) -apply(simp_all add: perm_fun_def) -apply(simp add: pt1[OF pta] pt1[OF ptb]) -apply(simp add: pt2[OF pta] pt2[OF ptb]) -apply(subgoal_tac "(rev pi1) \ (rev pi2)")(*A*) -apply(simp add: pt3[OF pta] pt3[OF ptb]) -(*A*) -apply(simp add: at_prm_rev_eq[OF at]) -done + unfolding pt_def using assms + by (auto simp add: perm_fun_def pt1 pt2 ptb pt3 pt3_rev) lemma pt_bool_inst: shows "pt TYPE(bool) TYPE('x)" @@ -1033,11 +960,8 @@ lemma pt_set_inst: assumes pt: "pt TYPE('a) TYPE('x)" shows "pt TYPE('a set) TYPE('x)" -apply(simp add: pt_def) -apply(simp_all add: perm_set_def) -apply(simp add: pt1[OF pt]) -apply(force simp add: pt2[OF pt] pt3[OF pt]) -done + unfolding pt_def + by(auto simp add: perm_set_def pt1[OF pt] pt2[OF pt] pt3[OF pt]) lemma pt_unit_inst: shows "pt TYPE(unit) TYPE('x)" @@ -1046,23 +970,15 @@ lemma pt_prod_inst: assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" - shows "pt TYPE('a \ 'b) TYPE('x)" - apply(auto simp add: pt_def) - apply(rule pt1[OF pta]) - apply(rule pt1[OF ptb]) - apply(rule pt2[OF pta]) - apply(rule pt2[OF ptb]) - apply(rule pt3[OF pta],assumption) - apply(rule pt3[OF ptb],assumption) - done +shows "pt TYPE('a \ 'b) TYPE('x)" + using assms pt1 pt2 pt3 + by(auto simp add: pt_def) lemma pt_list_nil: fixes xs :: "'a list" assumes pt: "pt TYPE('a) TYPE ('x)" shows "([]::'x prm)\xs = xs" -apply(induct_tac xs) -apply(simp_all add: pt1[OF pt]) -done + by (induct_tac xs) (simp_all add: pt1[OF pt]) lemma pt_list_append: fixes pi1 :: "'x prm" @@ -1070,9 +986,7 @@ and xs :: "'a list" assumes pt: "pt TYPE('a) TYPE ('x)" shows "(pi1@pi2)\xs = pi1\(pi2\xs)" -apply(induct_tac xs) -apply(simp_all add: pt2[OF pt]) -done + by (induct_tac xs) (simp_all add: pt2[OF pt]) lemma pt_list_prm_eq: fixes pi1 :: "'x prm" @@ -1080,55 +994,67 @@ and xs :: "'a list" assumes pt: "pt TYPE('a) TYPE ('x)" shows "pi1 \ pi2 \ pi1\xs = pi2\xs" -apply(induct_tac xs) -apply(simp_all add: prm_eq_def pt3[OF pt]) -done + by (induct_tac xs) (simp_all add: pt3[OF pt]) lemma pt_list_inst: assumes pt: "pt TYPE('a) TYPE('x)" shows "pt TYPE('a list) TYPE('x)" -apply(auto simp only: pt_def) -apply(rule pt_list_nil[OF pt]) -apply(rule pt_list_append[OF pt]) -apply(rule pt_list_prm_eq[OF pt],assumption) -done + by (simp add: pt pt_def pt_list_append pt_list_nil pt_list_prm_eq) lemma pt_option_inst: assumes pta: "pt TYPE('a) TYPE('x)" shows "pt TYPE('a option) TYPE('x)" -apply(auto simp only: pt_def) -apply(case_tac "x") -apply(simp_all add: pt1[OF pta]) -apply(case_tac "x") -apply(simp_all add: pt2[OF pta]) -apply(case_tac "x") -apply(simp_all add: pt3[OF pta]) -done +proof - + have "([]::('x \ _) list) \ x = x" for x :: "'a option" + by (metis assms none_eqvt not_None_eq pt1 some_eqvt) + moreover have "(pi1 @ pi2) \ x = pi1 \ pi2 \ x" + for pi1 pi2 :: "('x \ 'x) list" and x :: "'a option" + by (metis assms none_eqvt option.collapse pt2 some_eqvt) + moreover have "pi1 \ x = pi2 \ x" + if "pi1 \ pi2" for pi1 pi2 :: "('x \ 'x) list" and x :: "'a option" + using that pt3[OF pta] by (metis none_eqvt not_Some_eq some_eqvt) + ultimately show ?thesis + by (auto simp add: pt_def) +qed lemma pt_noption_inst: assumes pta: "pt TYPE('a) TYPE('x)" shows "pt TYPE('a noption) TYPE('x)" -apply(auto simp only: pt_def) -apply(case_tac "x") -apply(simp_all add: pt1[OF pta]) -apply(case_tac "x") -apply(simp_all add: pt2[OF pta]) -apply(case_tac "x") -apply(simp_all add: pt3[OF pta]) -done +proof - + have "([]::('x \ _) list) \ x = x" for x :: "'a noption" + by (metis assms nnone_eqvt noption.exhaust nsome_eqvt pt1) + moreover have "(pi1 @ pi2) \ x = pi1 \ pi2 \ x" + for pi1 pi2 :: "('x \ 'x) list" and x :: "'a noption" + using pt2[OF pta] + by (metis nnone_eqvt noption.exhaust nsome_eqvt) + moreover have "pi1 \ x = pi2 \ x" + if "pi1 \ pi2" + for pi1 pi2 :: "('x \ 'x) list" + and x :: "'a noption" + using that pt3[OF pta] by (metis nnone_eqvt noption.exhaust nsome_eqvt) + ultimately show ?thesis + by (auto simp add: pt_def) +qed lemma pt_nprod_inst: assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" shows "pt TYPE(('a,'b) nprod) TYPE('x)" - apply(auto simp add: pt_def) - apply(case_tac x) - apply(simp add: pt1[OF pta] pt1[OF ptb]) - apply(case_tac x) - apply(simp add: pt2[OF pta] pt2[OF ptb]) - apply(case_tac x) - apply(simp add: pt3[OF pta] pt3[OF ptb]) - done +proof - + have "([]::('x \ _) list) \ x = x" + for x :: "('a, 'b) nprod" + by (metis assms(1) nprod.exhaust perm_nprod.simps pt1 ptb) + moreover have "(pi1 @ pi2) \ x = pi1 \ pi2 \ x" + for pi1 pi2 :: "('x \ 'x) list" and x :: "('a, 'b) nprod" + using pt2[OF pta] pt2[OF ptb] + by (metis nprod.exhaust perm_nprod.simps) + moreover have "pi1 \ x = pi2 \ x" + if "pi1 \ pi2" for pi1 pi2 :: "('x \ 'x) list" and x :: "('a, 'b) nprod" + using that pt3[OF pta] pt3[OF ptb] by (smt (verit) nprod.exhaust perm_nprod.simps) + ultimately show ?thesis + by (auto simp add: pt_def) +qed + section \further lemmas for permutation types\ (*==============================================*) @@ -1236,12 +1162,7 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "[(a,b)]\([(b,a)]\x) = x" -apply(simp add: pt2[OF pt,symmetric]) -apply(rule trans) -apply(rule pt3[OF pt]) -apply(rule at_ds5'[OF at]) -apply(rule pt1[OF pt]) -done + by (metis assms at_ds5 pt_def pt_swap_bij) lemma pt_swap_bij'': fixes a :: "'x" @@ -1249,11 +1170,7 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "[(a,a)]\x = x" -apply(rule trans) -apply(rule pt3[OF pt]) -apply(rule at_ds1[OF at]) -apply(rule pt1[OF pt]) -done + by (metis assms at_ds1 pt_def) lemma supp_singleton: shows "supp {x} = supp x" @@ -1320,14 +1237,6 @@ shows "(pi\x)\X" using a by (simp add: pt_set_bij1[OF pt, OF at]) -(* FIXME: is this lemma needed anywhere? *) -lemma pt_set_bij3: - fixes pi :: "'x prm" - and x :: "'a" - and X :: "'a set" - shows "pi\(x\X) = (x\X)" -by (simp add: perm_bool) - lemma pt_subseteq_eqvt: fixes pi :: "'x prm" and Y :: "'a set" @@ -1351,10 +1260,13 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\{x::'a. P x} = {x. P ((rev pi)\x)}" -apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at]) -apply(rule_tac x="(rev pi)\x" in exI) -apply(simp add: pt_pi_rev[OF pt, OF at]) -done +proof - + have "\y. x = pi \ y \ P y" + if "P (rev pi \ x)" for x + using that by (metis at pt pt_pi_rev) + then show ?thesis + by (auto simp add: perm_set_def pt_rev_pi [OF assms]) +qed \ \some helper lemmas for the pt_perm_supp_ineq lemma\ lemma Collect_permI: @@ -1459,14 +1371,7 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\((supp x)::'x set)) = supp (pi\x)" -apply(rule pt_perm_supp_ineq) -apply(rule pt) -apply(rule at_pt_inst) -apply(rule at)+ -apply(rule cp_pt_inst) -apply(rule pt) -apply(rule at) -done + by (rule pt_perm_supp_ineq) (auto simp: assms at_pt_inst cp_pt_inst) lemma pt_supp_finite_pi: fixes pi :: "'x prm" @@ -1475,10 +1380,7 @@ and at: "at TYPE('x)" and f: "finite ((supp x)::'x set)" shows "finite ((supp (pi\x))::'x set)" -apply(simp add: pt_perm_supp[OF pt, OF at, symmetric]) -apply(simp add: pt_set_finite_ineq[OF at_pt_inst[OF at], OF at]) -apply(rule f) -done + by (metis at at_pt_inst f pt pt_perm_supp pt_set_finite_ineq) lemma pt_fresh_left_ineq: fixes pi :: "'x prm" @@ -1489,10 +1391,8 @@ and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "a\(pi\x) = ((rev pi)\a)\x" -apply(simp add: fresh_def) -apply(simp add: pt_set_bij1[OF ptb, OF at]) -apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp]) -done + using pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp] pt_set_bij1[OF ptb, OF at] + by (simp add: fresh_def) lemma pt_fresh_right_ineq: fixes pi :: "'x prm" @@ -1503,10 +1403,7 @@ and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "(pi\a)\x = a\((rev pi)\x)" -apply(simp add: fresh_def) -apply(simp add: pt_set_bij1[OF ptb, OF at]) -apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp]) -done + by (simp add: assms pt_fresh_left_ineq) lemma pt_fresh_bij_ineq: fixes pi :: "'x prm" @@ -1517,9 +1414,7 @@ and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "(pi\a)\(pi\x) = a\x" -apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp]) -apply(simp add: pt_rev_pi[OF ptb, OF at]) -done + using assms pt_bij1 pt_fresh_right_ineq by fastforce lemma pt_fresh_left: fixes pi :: "'x prm" @@ -1528,14 +1423,7 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "a\(pi\x) = ((rev pi)\a)\x" -apply(rule pt_fresh_left_ineq) -apply(rule pt) -apply(rule at_pt_inst) -apply(rule at)+ -apply(rule cp_pt_inst) -apply(rule pt) -apply(rule at) -done + by (simp add: assms at_pt_inst cp_pt_inst pt_fresh_left_ineq) lemma pt_fresh_right: fixes pi :: "'x prm" @@ -1544,14 +1432,7 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\a)\x = a\((rev pi)\x)" -apply(rule pt_fresh_right_ineq) -apply(rule pt) -apply(rule at_pt_inst) -apply(rule at)+ -apply(rule cp_pt_inst) -apply(rule pt) -apply(rule at) -done + by (simp add: assms at_pt_inst cp_pt_inst pt_fresh_right_ineq) lemma pt_fresh_bij: fixes pi :: "'x prm" @@ -1560,14 +1441,7 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\a)\(pi\x) = a\x" -apply(rule pt_fresh_bij_ineq) -apply(rule pt) -apply(rule at_pt_inst) -apply(rule at)+ -apply(rule cp_pt_inst) -apply(rule pt) -apply(rule at) -done + by (metis assms pt_bij1 pt_fresh_right) lemma pt_fresh_bij1: fixes pi :: "'x prm" @@ -1796,21 +1670,20 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(\(x::'a). P x) = (\(x::'a). pi\(P ((rev pi)\x)))" -apply(auto simp add: perm_bool perm_fun_def) -apply(drule_tac x="pi\x" in spec) -apply(simp add: pt_rev_pi[OF pt, OF at]) -done + by (smt (verit, ccfv_threshold) assms pt_bij1 true_eqvt) lemma pt_ex_eqvt: fixes pi :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" - shows "pi\(\(x::'a). P x) = (\(x::'a). pi\(P ((rev pi)\x)))" -apply(auto simp add: perm_bool perm_fun_def) -apply(rule_tac x="pi\x" in exI) -apply(simp add: pt_rev_pi[OF pt, OF at]) -done +shows "pi\(\(x::'a). P x) = (\(x::'a). pi\(P ((rev pi)\x)))" +proof - + have "\x. P x \ P (rev pi \ pi \ x)" + by (simp add: assms(1) at pt_rev_pi) + then show ?thesis + by(auto simp add: perm_bool perm_fun_def) +qed lemma pt_ex1_eqvt: fixes pi :: "'x prm" @@ -1828,12 +1701,7 @@ and at: "at TYPE('x)" and unique: "\!x. P x" shows "pi\(THE(x::'a). P x) = (THE(x::'a). pi\(P ((rev pi)\x)))" - apply(rule the1_equality [symmetric]) - apply(simp add: pt_ex1_eqvt[OF pt at,symmetric]) - apply(simp add: perm_bool unique) - apply(simp add: perm_bool pt_rev_pi [OF pt at]) - apply(rule theI'[OF unique]) - done + by (smt (verit, best) assms perm_bool_def pt_rev_pi theI_unique unique) section \facts about supports\ (*==============================*) @@ -1934,13 +1802,17 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" and a: "\x\X. (\(a::'x) (b::'x). a\S\b\S \ ([(a,b)]\x)\X)" - shows "S supports X" -using a -apply(auto simp add: supports_def) -apply(simp add: pt_set_bij1a[OF pt, OF at]) -apply(force simp add: pt_swap_bij[OF pt, OF at]) -apply(simp add: pt_set_bij1a[OF pt, OF at]) -done +shows "S supports X" +proof - + have "x \ X" + if "a \ S" "b \ S" and "x \ [(a, b)] \ X" for a b x + using that by (metis a assms(1) at pt_pi_rev pt_set_bij1a) + moreover have "x \ [(a, b)] \ X" + if "a \ S" "b \ S" and "x \ X" for a b x + using that by (simp add: a assms(1) at pt_set_bij1a) + ultimately show ?thesis + by (meson subsetI subset_antisym supports_def) +qed lemma supports_fresh: fixes S :: "'x set" @@ -1950,10 +1822,7 @@ and a2: "finite S" and a3: "a\S" shows "a\x" -proof (simp add: fresh_def) - have "(supp x)\S" using a1 a2 by (rule supp_is_subset) - thus "a\(supp x)" using a3 by force -qed + by (meson assms fresh_def in_mono supp_is_subset) lemma at_fin_set_supports: fixes X::"'x set" @@ -1969,12 +1838,7 @@ assumes a1:"infinite X" and a2:"\b\X. P(b)" shows "infinite {b\X. P(b)}" - using a1 a2 - apply auto - apply (subgoal_tac "infinite (X - {b\X. P b})") - apply (simp add: set_diff_eq) - apply (simp add: Diff_infinite_finite) - done + using assms rev_finite_subset by fastforce lemma at_fin_set_supp: fixes X::"'x set" @@ -2206,32 +2070,15 @@ proof - have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at) show ?thesis - proof (rule equalityI) - show "pi\(\x\X. f x) \ (\x\(pi\X). (pi\f) x)" - apply(auto simp add: perm_set_def) - apply(rule_tac x="pi\xb" in exI) - apply(rule conjI) - apply(rule_tac x="xb" in exI) - apply(simp) - apply(subgoal_tac "(pi\f) (pi\xb) = pi\(f xb)")(*A*) - apply(simp) - apply(rule pt_set_bij2[OF pt_x, OF at]) - apply(assumption) - (*A*) - apply(rule sym) - apply(rule pt_fun_app_eq[OF pt, OF at]) - done - next - show "(\x\(pi\X). (pi\f) x) \ pi\(\x\X. f x)" - apply(auto simp add: perm_set_def) - apply(rule_tac x="(rev pi)\x" in exI) - apply(rule conjI) - apply(simp add: pt_pi_rev[OF pt_x, OF at]) - apply(rule_tac x="xb" in bexI) - apply(simp add: pt_set_bij1[OF pt_x, OF at]) - apply(simp add: pt_fun_app_eq[OF pt, OF at]) - apply(assumption) - done + proof - + have "\x. (\u. x = pi \ u \ u \ X) \ pi \ z \ (pi \ f) x" + if "y \ X" and "z \ f y" for y z + using that by (metis assms at_pt_inst pt_fun_app_eq pt_set_bij) + moreover have "\u. x = pi \ u \ (\x\X. u \ f x)" + if "x \ (pi \ f) (pi \ y)" and "y \ X" for x y + using that by (metis at at_pi_rev pt pt_fun_app_eq pt_set_bij1a pt_x) + ultimately show ?thesis + by (auto simp: perm_set_def) qed qed @@ -2241,34 +2088,14 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(X_to_Un_supp X) = ((X_to_Un_supp (pi\X))::'x set)" - apply(simp add: X_to_Un_supp_def) - apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def) - apply(simp add: pt_perm_supp[OF pt, OF at]) - apply(simp add: pt_pi_rev[OF pt, OF at]) - done + by (metis UNION_f_eqvt X_to_Un_supp_def assms pt_fun_eq pt_perm_supp) lemma Union_supports_set: fixes X::"('a set)" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(\x\X. ((supp x)::'x set)) supports X" - apply(simp add: supports_def fresh_def[symmetric]) - apply(rule allI)+ - apply(rule impI) - apply(erule conjE) - apply(simp add: perm_set_def) - apply(auto) - apply(subgoal_tac "[(a,b)]\xa = xa")(*A*) - apply(simp) - apply(rule pt_fresh_fresh[OF pt, OF at]) - apply(force) - apply(force) - apply(rule_tac x="x" in exI) - apply(simp) - apply(rule sym) - apply(rule pt_fresh_fresh[OF pt, OF at]) - apply(force)+ - done + by (simp add: assms fresh_def pt_fresh_fresh supports_set) lemma Union_of_fin_supp_sets: fixes X::"('a set)" @@ -2286,19 +2113,14 @@ shows "(\x\X. ((supp x)::'x set)) \ supp X" proof - have "supp ((X_to_Un_supp X)::'x set) \ ((supp X)::'x set)" - apply(rule pt_empty_supp_fun_subset) - apply(force intro: pt_set_inst at_pt_inst pt at)+ - apply(rule pt_eqvt_fun2b) - apply(force intro: pt_set_inst at_pt_inst pt at)+ - apply(rule allI)+ - apply(rule X_to_Un_supp_eqvt[OF pt, OF at]) - done + proof (rule pt_empty_supp_fun_subset) + show "supp (\a. X_to_Un_supp (a::'a set)::'x set) = ({}::'x set)" + by (simp add: X_to_Un_supp_eqvt at at_pt_inst pt pt_eqvt_fun2b pt_set_inst) + qed (use assms at_pt_inst pt_set_inst in auto) hence "supp (\x\X. ((supp x)::'x set)) \ ((supp X)::'x set)" by (simp add: X_to_Un_supp_def) moreover have "supp (\x\X. ((supp x)::'x set)) = (\x\X. ((supp x)::'x set))" - apply(rule at_fin_set_supp[OF at]) - apply(rule Union_of_fin_supp_sets[OF fs, OF fi]) - done + using Union_of_fin_supp_sets at at_fin_set_supp fi fs by auto ultimately show ?thesis by force qed @@ -2309,12 +2131,15 @@ and fs: "fs TYPE('a) TYPE('x)" and fi: "finite X" shows "(supp X) = (\x\X. ((supp x)::'x set))" -apply(rule equalityI) -apply(rule supp_is_subset) -apply(rule Union_supports_set[OF pt, OF at]) -apply(rule Union_of_fin_supp_sets[OF fs, OF fi]) -apply(rule Union_included_in_supp[OF pt, OF at, OF fs, OF fi]) -done +proof (rule equalityI) + have "finite (\ (supp ` X)::'x set)" + using Union_of_fin_supp_sets fi fs by blast + then show "(supp X::'x set) \ \ (supp ` X)" + by (metis Union_supports_set at pt supp_is_subset) +next + show "(\x\X. (supp x::'x set)) \ supp X" + by (simp add: Union_included_in_supp at fi fs pt) +qed lemma supp_fin_union: fixes X::"('a set)" @@ -2353,9 +2178,7 @@ and f1: "finite X" and f2: "finite Y" shows "a\(X\Y) = (a\X \ a\Y)" -apply(simp add: fresh_def) -apply(simp add: supp_fin_union[OF pt, OF at, OF fs, OF f1, OF f2]) -done + by (simp add: assms fresh_def supp_fin_union) lemma fresh_fin_insert: fixes X::"('a set)" @@ -2366,9 +2189,7 @@ and fs: "fs TYPE('a) TYPE('x)" and f: "finite X" shows "a\(insert x X) = (a\x \ a\X)" -apply(simp add: fresh_def) -apply(simp add: supp_fin_insert[OF pt, OF at, OF fs, OF f]) -done + by (simp add: assms fresh_def supp_fin_insert) lemma fresh_fin_insert1: fixes X::"('a set)" @@ -2447,11 +2268,11 @@ lemma fresh_star_Un_elim: "((S \ T) \* c \ PROP C) \ (S \* c \ T \* c \ PROP C)" - apply rule - apply (simp_all add: fresh_star_def) - apply (erule meta_mp) - apply blast - done +proof + assume \
: "(S \ T) \* c \ PROP C" and c: "S \* c" "T \* c" + show "PROP C" + using c by (intro \
) (metis Un_iff fresh_star_set) +qed (auto simp: fresh_star_def) lemma fresh_star_insert_elim: "(insert x S \* c \ PROP C) \ (x \ c \ S \* c \ PROP C)" @@ -2485,22 +2306,22 @@ and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "(pi\a)\*(pi\x) = a\*x" and "(pi\b)\*(pi\x) = b\*x" -apply(unfold fresh_star_def) -apply(auto) -apply(drule_tac x="pi\xa" in bspec) -apply(erule pt_set_bij2[OF ptb, OF at]) -apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp]) -apply(drule_tac x="(rev pi)\xa" in bspec) -apply(simp add: pt_set_bij1[OF ptb, OF at]) -apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp]) -apply(drule_tac x="pi\xa" in bspec) -apply(simp add: pt_set_bij1[OF ptb, OF at]) -apply(simp add: set_eqvt pt_rev_pi[OF pt_list_inst[OF ptb], OF at]) -apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp]) -apply(drule_tac x="(rev pi)\xa" in bspec) -apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt) -apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp]) -done + unfolding fresh_star_def +proof - + have "y \ x" if "\z\pi \ a. z \ pi \ x" and "y \ a" for y + using that by (meson assms at pt_fresh_bij_ineq pt_set_bij2) + moreover have "y \ pi \ x" if "\z\a. z \ x" and "y \ pi \ a" for y + using that by (simp add: assms pt_fresh_left_ineq pt_set_bij1a) + moreover have "y \ x" + if "\z\set (pi \ b). z \ pi \ x" and "y \ set b" for y + using that by (metis at cp pt_fresh_bij_ineq pt_set_bij pta ptb set_eqvt) + moreover have "y \ pi \ x" + if "\z\set b. z \ x" and "y \ set (pi \ b)" for y + using that by (metis at cp pt_fresh_left_ineq pt_set_bij1a pta ptb set_eqvt) + ultimately show "(\xa\pi \ a. xa \ pi \ x) = (\xa\a. xa \ x)" "(\xa\set (pi \ b). xa \ pi \ x) = (\xa\set b. xa \ x)" + by blast+ +qed + lemma pt_fresh_star_bij: fixes pi :: "'x prm" @@ -2511,21 +2332,10 @@ and at: "at TYPE('x)" shows "(pi\a)\*(pi\x) = a\*x" and "(pi\b)\*(pi\x) = b\*x" -apply(rule pt_fresh_star_bij_ineq(1)) -apply(rule pt) -apply(rule at_pt_inst) -apply(rule at)+ -apply(rule cp_pt_inst) -apply(rule pt) -apply(rule at) -apply(rule pt_fresh_star_bij_ineq(2)) -apply(rule pt) -apply(rule at_pt_inst) -apply(rule at)+ -apply(rule cp_pt_inst) -apply(rule pt) -apply(rule at) -done +proof (rule pt_fresh_star_bij_ineq) + show "(pi \ b) \* (pi \ x) = b \* x" + by (simp add: at at_pt_inst cp_pt_inst pt pt_fresh_star_bij_ineq) +qed (auto simp: at pt at_pt_inst cp_pt_inst) lemma pt_fresh_star_eqvt: fixes pi :: "'x prm" @@ -2582,16 +2392,9 @@ shows "pi\x = x" using a apply(induct pi) + apply (simp add: assms(1) pt1) apply(auto simp add: fresh_star_def fresh_list_cons fresh_prod pt1[OF pt]) -apply(subgoal_tac "((a,b)#pi)\x = ([(a,b)]@pi)\x") -apply(simp only: pt2[OF pt]) -apply(rule pt_fresh_fresh[OF pt at]) -apply(simp add: fresh_def at_supp[OF at]) -apply(blast) -apply(simp add: fresh_def at_supp[OF at]) -apply(blast) -apply(simp add: pt2[OF pt]) -done + by (metis Cons_eq_append_conv append_self_conv2 assms(1) at at_fresh fresh_def pt2 pt_fresh_fresh) section \Infrastructure lemmas for strong rule inductions\ (*==========================================================*) @@ -2685,63 +2488,43 @@ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" shows "cp TYPE ('a list) TYPE('x) TYPE('y)" using c1 -apply(simp add: cp_def) -apply(auto) -apply(induct_tac x) -apply(auto) -done +apply(clarsimp simp add: cp_def) + by (induct_tac x) auto lemma cp_set_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" shows "cp TYPE ('a set) TYPE('x) TYPE('y)" -using c1 -apply(simp add: cp_def) -apply(auto) -apply(auto simp add: perm_set_def) -apply(rule_tac x="pi2\xc" in exI) -apply(auto) -done + using c1 + unfolding cp_def perm_set_def + by (smt (verit) Collect_cong mem_Collect_eq) + lemma cp_option_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" shows "cp TYPE ('a option) TYPE('x) TYPE('y)" -using c1 -apply(simp add: cp_def) -apply(auto) -apply(case_tac x) -apply(auto) -done + using c1 unfolding cp_def by (metis none_eqvt not_None_eq some_eqvt) lemma cp_noption_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" shows "cp TYPE ('a noption) TYPE('x) TYPE('y)" -using c1 -apply(simp add: cp_def) -apply(auto) -apply(case_tac x) -apply(auto) -done + using c1 unfolding cp_def + by (metis nnone_eqvt noption.exhaust nsome_eqvt) lemma cp_unit_inst: shows "cp TYPE (unit) TYPE('x) TYPE('y)" -apply(simp add: cp_def) -done + by (simp add: cp_def) lemma cp_bool_inst: shows "cp TYPE (bool) TYPE('x) TYPE('y)" -apply(simp add: cp_def) -apply(rule allI)+ -apply(induct_tac x) -apply(simp_all) -done + apply(clarsimp simp add: cp_def) + by (induct_tac x) auto lemma cp_prod_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" and c2: "cp TYPE ('b) TYPE('x) TYPE('y)" shows "cp TYPE ('a\'b) TYPE('x) TYPE('y)" using c1 c2 -apply(simp add: cp_def) -done + by (simp add: cp_def) lemma cp_fun_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" @@ -2749,11 +2532,8 @@ and pt: "pt TYPE ('y) TYPE('x)" and at: "at TYPE ('x)" shows "cp TYPE ('a\'b) TYPE('x) TYPE('y)" -using c1 c2 -apply(auto simp add: cp_def perm_fun_def fun_eq_iff) -apply(simp add: rev_eqvt[symmetric]) -apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at]) -done + using c1 c2 + by(auto simp add: cp_def perm_fun_def fun_eq_iff at pt pt_list_inst pt_prod_inst pt_rev_pi rev_eqvt) section \Andy's freshness lemma\ @@ -2856,9 +2636,7 @@ and f1: "finite ((supp h)::'x set)" and a: "a\h" "a\h a" shows "(fresh_fun h) = (h a)" -apply(rule fresh_fun_app[OF pt, OF at, OF f1]) -apply(auto simp add: fresh_prod intro: a) -done + by (meson assms fresh_fun_app fresh_prod pt) lemma fresh_fun_equiv_ineq: fixes h :: "'y\'a" @@ -2938,11 +2716,7 @@ and f1: "finite ((supp h)::'x set)" and a: "\(a::'x). a\(h,h a)" shows "((supp h)::'x set) supports (fresh_fun h)" - apply(simp add: supports_def fresh_def[symmetric]) - apply(auto) - apply(simp add: fresh_fun_equiv[OF pt, OF at, OF f1, OF a]) - apply(simp add: pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at]) - done + by(simp flip: fresh_def add: supports_def assms at_pt_inst fresh_fun_equiv pt_fresh_fresh pt_fun_inst) section \Abstraction function\ (*==============================*) @@ -2951,7 +2725,7 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pt TYPE('x\('a noption)) TYPE('x)" - by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at]) + by (simp add: at at_pt_inst pt pt_fun_inst pt_noption_inst) definition abs_fun :: "'x\'a\('x\('a noption))" (\[_]._\ [100,100] 100) where "[a].x \ (\b. (if b=a then nSome(x) else (if b\x then nSome([(a,b)]\x) else nNone)))" @@ -2973,26 +2747,22 @@ and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" - shows "pi\([a].x) = [(pi\a)].(pi\x)" - apply(simp add: abs_fun_def perm_fun_def abs_fun_if) - apply(simp only: fun_eq_iff) - apply(rule allI) - apply(subgoal_tac "(((rev pi)\(xa::'y)) = (a::'y)) = (xa = pi\a)")(*A*) - apply(subgoal_tac "(((rev pi)\xa)\x) = (xa\(pi\x))")(*B*) - apply(subgoal_tac "pi\([(a,(rev pi)\xa)]\x) = [(pi\a,xa)]\(pi\x)")(*C*) - apply(simp) -(*C*) - apply(simp add: cp1[OF cp]) - apply(simp add: pt_pi_rev[OF ptb, OF at]) -(*B*) - apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp]) -(*A*) - apply(rule iffI) - apply(rule pt_bij2[OF ptb, OF at, THEN sym]) - apply(simp) - apply(rule pt_bij2[OF ptb, OF at]) - apply(simp) -done +shows "pi\([a].x) = [(pi\a)].(pi\x)" + unfolding fun_eq_iff +proof + fix y + have "(((rev pi)\y) = a) = (y = pi\a)" + by (metis at pt_rev_pi ptb) + moreover + have "(((rev pi)\y)\x) = (y\(pi\x))" + by (simp add: assms pt_fresh_left_ineq) + moreover + have "pi\([(a,(rev pi)\y)]\x) = [(pi\a,y)]\(pi\x)" + using assms cp1[OF cp] by (simp add: pt_pi_rev) + ultimately + show "(pi \ [a].x) y = ([(pi \ a)].(pi \ x)) y" + by (simp add: abs_fun_def perm_fun_def) +qed lemma abs_fun_pi: fixes a :: "'x" @@ -3001,25 +2771,14 @@ assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\([a].x) = [(pi\a)].(pi\x)" -apply(rule abs_fun_pi_ineq) -apply(rule pt) -apply(rule at_pt_inst) -apply(rule at)+ -apply(rule cp_pt_inst) -apply(rule pt) -apply(rule at) -done + by (simp add: abs_fun_pi_ineq at at_pt_inst cp_pt_inst pt) lemma abs_fun_eq1: fixes x :: "'a" and y :: "'a" and a :: "'x" shows "([a].x = [a].y) = (x = y)" -apply(auto simp add: abs_fun_def) -apply(auto simp add: fun_eq_iff) -apply(drule_tac x="a" in spec) -apply(simp) -done + by (metis abs_fun_def noption.inject) lemma abs_fun_eq2: fixes x :: "'a" @@ -3210,10 +2969,7 @@ and as: "[a].x = [b].y" and fr: "c\a" "c\b" "c\x" "c\y" shows "x = [(a,c)]\[(b,c)]\y" -using as fr -apply(drule_tac sym) -apply(simp add: abs_fun_fresh[OF pt, OF at] pt_swap_bij[OF pt, OF at]) -done + using assms by (metis abs_fun_fresh pt_swap_bij) lemma abs_fun_supp_approx: fixes x :: "'a" @@ -3359,12 +3115,10 @@ and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" and dj: "disjoint TYPE('y) TYPE('x)" - shows "((supp ([a].x))::'x set) = (supp x)" -apply(auto simp add: supp_def) -apply(auto simp add: abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp]) -apply(auto simp add: dj_perm_forget[OF dj]) -apply(auto simp add: abs_fun_eq1) -done +shows "((supp ([a].x))::'x set) = (supp x)" +unfolding supp_def + using abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] + by (smt (verit, ccfv_threshold) Collect_cong abs_fun_eq1) lemma fresh_abs_fun_iff_ineq: fixes a :: "'y" @@ -3453,17 +3207,7 @@ have pt_prm: "pt TYPE('x prm) TYPE('x)" by (rule pt_list_inst[OF pt_prod_inst[OF pt, OF pt]]) from a show ?thesis - apply - - apply(auto simp add: prm_eq_def) - apply(rule_tac pi="rev pi3" in pt_bij4[OF pt, OF at]) - apply(rule trans) - apply(rule pt_perm_compose[OF pt, OF at]) - apply(simp add: pt_rev_pi[OF pt_prm, OF at]) - apply(rule sym) - apply(rule trans) - apply(rule pt_perm_compose[OF pt, OF at]) - apply(simp add: pt_rev_pi[OF pt_prm, OF at]) - done + by (auto simp add: prm_eq_def at pt pt_perm_compose') qed (************************) @@ -3524,32 +3268,32 @@ by (simp add: perm_int_def) lemma numeral_int_eqvt: - shows "pi\((numeral n)::int) = numeral n" -by (simp add: perm_int_def perm_int_def) + shows "pi\((numeral n)::int) = numeral n" + using perm_int_def by blast lemma neg_numeral_int_eqvt: - shows "pi\((- numeral n)::int) = - numeral n" -by (simp add: perm_int_def perm_int_def) + shows "pi\((- numeral n)::int) = - numeral n" + by (simp add: perm_int_def) lemma max_int_eqvt: fixes x::"int" shows "pi\(max (x::int) y) = max (pi\x) (pi\y)" -by (simp add:perm_int_def) + by (simp add:perm_int_def) lemma min_int_eqvt: fixes x::"int" shows "pi\(min x y) = min (pi\x) (pi\y)" -by (simp add:perm_int_def) + by (simp add:perm_int_def) lemma plus_int_eqvt: fixes x::"int" shows "pi\(x + y) = (pi\x) + (pi\y)" -by (simp add:perm_int_def) + by (simp add:perm_int_def) lemma minus_int_eqvt: fixes x::"int" shows "pi\(x - y) = (pi\x) - (pi\y)" -by (simp add:perm_int_def) + by (simp add:perm_int_def) lemma mult_int_eqvt: fixes x::"int" @@ -3559,7 +3303,7 @@ lemma div_int_eqvt: fixes x::"int" shows "pi\(x div y) = (pi\x) div (pi\y)" -by (simp add:perm_int_def) + by (simp add:perm_int_def) (*******************************************************) (* Setup of the theorem attributes eqvt and eqvt_force *)