# HG changeset patch # User Christian Urban # Date 1524142637 -3600 # Node ID 017e33849f4d53778cb953ec3d1aa412cf5da1c4 # Parent a44479bde681c3f9888c727bb03fe7a4310123aa updated to Isabelle 2016-1 diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/CPS/CPS1_Plotkin.thy --- a/Nominal/Ex/CPS/CPS1_Plotkin.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Thu Apr 19 13:57:17 2018 +0100 @@ -1,4 +1,4 @@ -header {* CPS conversion *} +(* CPS conversion *) theory CPS1_Plotkin imports Lt begin diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/CPS/CPS2_DanvyNielsen.thy --- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Thu Apr 19 13:57:17 2018 +0100 @@ -1,4 +1,4 @@ -header {* CPS transformation of Danvy and Nielsen *} +(* CPS transformation of Danvy and Nielsen *) theory CPS2_DanvyNielsen imports Lt begin diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/CPS/CPS3_DanvyFilinski.thy --- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Thu Apr 19 13:57:17 2018 +0100 @@ -1,4 +1,4 @@ -header {* CPS transformation of Danvy and Filinski *} +(* CPS transformation of Danvy and Filinski *) theory CPS3_DanvyFilinski imports Lt begin nominal_function diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy --- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy Thu Apr 19 13:57:17 2018 +0100 @@ -1,4 +1,4 @@ -header {* CPS transformation of Danvy and Filinski *} +(* CPS transformation of Danvy and Filinski *) theory CPS3_DanvyFilinski_FCB2 imports Lt begin diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/CPS/Lt.thy --- a/Nominal/Ex/CPS/Lt.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/CPS/Lt.thy Thu Apr 19 13:57:17 2018 +0100 @@ -1,4 +1,4 @@ -header {* The Call-by-Value Lambda Calculus *} +(* The Call-by-Value Lambda Calculus *) theory Lt imports "../../Nominal2" begin diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/Datatypes.thy --- a/Nominal/Ex/Datatypes.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/Datatypes.thy Thu Apr 19 13:57:17 2018 +0100 @@ -44,7 +44,7 @@ "p \ (f::foo) = f" instance -apply(default) +apply(standard) apply(simp_all add: permute_foo_def) done diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/Lambda.thy Thu Apr 19 13:57:17 2018 +0100 @@ -152,7 +152,7 @@ section {* Paths to a free variables *} instance path :: pure -apply(default) +apply(standard) apply(induct_tac "x::path" rule: path.induct) apply(simp_all) done @@ -615,7 +615,7 @@ | DBLam db instance db :: pure - apply default + apply standard apply (induct_tac x rule: db.induct) apply (simp_all add: permute_pure) done @@ -930,7 +930,7 @@ and x y::"'a::at" shows "[[atom x]]lst. t = [[atom y]]lst. ta \ [[atom x]]lst. s = [[atom y]]lst. sa \ [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)" - by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair) + by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff fresh_Pair) nominal_function aux2 :: "lam \ lam \ bool" diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/Pi.thy --- a/Nominal/Ex/Pi.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/Pi.thy Thu Apr 19 13:57:17 2018 +0100 @@ -380,7 +380,6 @@ show "atom x \ g \ g[x::=\\y] = g" and "atom x \ xg \ xg[x::=\\y] = xg" and "atom x \ P \ P[x::=\y] = P" - using assms apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct) by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base) qed diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/TypeSchemes1.thy --- a/Nominal/Ex/TypeSchemes1.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/TypeSchemes1.thy Thu Apr 19 13:57:17 2018 +0100 @@ -117,7 +117,7 @@ nominal_function substs :: "(name \ ty) list \ tys \ tys" ("_<_>" [100,60] 120) where - "fset (map_fset atom Xs) \* \ \ \ = All [Xs].(\)" + "fset (atom |`| Xs) \* \ \ \ = All [Xs].(\)" apply(simp add: eqvt_def substs_graph_aux_def) apply auto[2] apply (rule_tac y="b" and c="a" in tys.strong_exhaust) @@ -284,7 +284,7 @@ apply(rule_tac y="b" and c="a" in tys.strong_exhaust) apply(simp) apply(clarify) -apply(simp only: tys.eq_iff map_fset_image) +apply(simp only: tys.eq_iff fimage.rep_eq) apply(erule_tac c="Ta" in Abs_res_fcb2) apply(simp) apply(simp) diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/TypeSchemes2.thy --- a/Nominal/Ex/TypeSchemes2.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/TypeSchemes2.thy Thu Apr 19 13:57:17 2018 +0100 @@ -2,6 +2,7 @@ imports "../Nominal2" begin + section {*** Type Schemes defined as a single nominal datatype ***} atom_decl name @@ -60,14 +61,14 @@ shows "(p \ (Sum_Type.projl (f x))) = Sum_Type.projl (p \ (f x))" using a by clarsimp - + nominal_function (default "case_sum (\x. Inl undefined) (\x. Inr undefined)") subst :: "(name \ ty) list \ ty \ ty" and substs :: "(name \ ty) list \ tys \ tys" where "subst \ (Var X) = lookup \ X" | "subst \ (Fun T1 T2) = Fun (subst \ T1) (subst \ T2)" -| "fset (map_fset atom xs) \* \ \ substs \ (All xs T) = All xs (subst \ T)" +| "fset (atom |`| xs) \* \ \ substs \ (All xs T) = All xs (subst \ T)" thm subst_substs_graph_def subst_substs_graph_aux_def apply(simp add: subst_substs_graph_aux_def eqvt_def) apply(rule TrueI) diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/Weakening.thy --- a/Nominal/Ex/Weakening.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Ex/Weakening.thy Thu Apr 19 13:57:17 2018 +0100 @@ -107,7 +107,7 @@ valid2 :: "(name \ ty) fset \ bool" where v2_Empty[intro]: "valid2 {||}" -| v2_Insert[intro]: "\(x, T) |\| Gamma; valid2 Gamma\ \ valid2 (insert_fset (x, T) Gamma)" +| v2_Insert[intro]: "\(x, T) |\| Gamma; valid2 Gamma\ \ valid2 (finsert (x, T) Gamma)" equivariance valid2 @@ -116,7 +116,7 @@ where t2_Var[intro]: "\valid2 \; (x, T) |\| \\ \ \ 2\ Var x : T" | t2_App[intro]: "\\ 2\ t1 : T1 \ T2; \ 2\ t2 : T1\ \ \ 2\ App t1 t2 : T2" - | t2_Lam[intro]: "\atom x \ \; insert_fset (x, T1) \ 2\ t : T2\ \ \ 2\ Lam [x]. t : T1 \ T2" + | t2_Lam[intro]: "\atom x \ \; finsert (x, T1) \ 2\ t : T2\ \ \ 2\ Lam [x]. t : T1 \ T2" equivariance typing2 @@ -133,12 +133,8 @@ apply(nominal_induct \ t T avoiding: x rule: typing2.strong_induct) apply(auto)[2] apply(rule t2_Lam) -apply(simp add: fresh_insert_fset fresh_ty) -apply(simp) -apply(drule_tac x="xa" in meta_spec) -apply(drule meta_mp) -apply(simp add: fresh_at_base) -apply(simp add: insert_fset_left_comm) +apply(simp add: fresh_finsert fresh_ty) +apply(force) done lemma weakening_version4: @@ -155,7 +151,7 @@ apply(rule_tac t= "Lam [x]. t" and s="Lam [a]. ((a \ x) \ t)" in subst) defer apply(rule t2_Lam) -apply(simp add: fresh_insert_fset) +apply(simp add: fresh_finsert) oops diff -r a44479bde681 -r 017e33849f4d Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Nominal2.thy Thu Apr 19 13:57:17 2018 +0100 @@ -46,7 +46,7 @@ val induct_attr = Attrib.internal (K Induct.induct_simp_add) *} -section{* Interface for nominal_datatype *} +section{* Interface for @{text nominal_datatype} *} ML {* fun get_cnstrs dts = @@ -64,7 +64,7 @@ *} -text {* Infrastructure for adding "_raw" to types and terms *} +text {* Infrastructure for adding @{text "_raw"} to types and terms *} ML {* fun add_raw s = s ^ "_raw" @@ -109,7 +109,7 @@ (raw_bind bn, SOME (replace_typ dts_env ty), NoSyn)) bn_funs val bn_eqs' = map (fn (attr, trm) => - (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs + ((attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm), [], [])) bn_eqs in (bn_funs', bn_eqs') end @@ -260,15 +260,15 @@ val raw_fv_eqvt = raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) - (Local_Theory.restore lthy_tmp) + (Local_Theory.reset lthy_tmp) val raw_size_eqvt = let val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info in raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) - (Local_Theory.restore lthy_tmp) - |> map (rewrite_rule (Local_Theory.restore lthy_tmp) + (Local_Theory.reset lthy_tmp) + |> map (rewrite_rule (Local_Theory.reset lthy_tmp) @{thms permute_nat_def[THEN eq_reflection]}) |> map (fn thm => thm RS @{thm sym}) end @@ -489,7 +489,7 @@ (* generating the prefix for the theorem names *) val thms_name = the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name - fun thms_suffix s = Binding.qualified true s thms_name + fun thms_suffix s = Binding.qualify_name true thms_name s val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms @@ -582,7 +582,7 @@ val lthy = Named_Target.theory_init thy val ((bn_funs, bn_eqs), lthy') = - Specification.read_spec bn_fun_strs bn_eq_strs lthy + Specification.read_multi_specs bn_fun_strs bn_eq_strs lthy fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) @@ -727,7 +727,7 @@ (* binding function parser *) val bnfun_parser = - Scan.optional (@{keyword "binder"} |-- Parse.fixes -- Parse_Spec.where_alt_specs) ([], []) + Scan.optional (@{keyword "binder"} |-- Parse_Spec.specification) ([], []) (* main parser *) val main_parser = diff -r a44479bde681 -r 017e33849f4d Nominal/Nominal2_Abs.thy --- a/Nominal/Nominal2_Abs.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Nominal2_Abs.thy Thu Apr 19 13:57:17 2018 +0100 @@ -854,7 +854,7 @@ moreover { assume *: "a \ b" and **: "x = (a \ b) \ y \ atom a \ y" have "[{atom a}]set. x = [{atom a}]set. ((a \ b) \ y)" using ** by simp - also have "\ = (a \ b) \ ([{atom b}]set. y)" by (simp add: permute_set_def assms) + also have "\ = (a \ b) \ ([{atom b}]set. y)" by (simp add: permute_set_def) also have "\ = [{atom b}]set. y" by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) finally have "[{atom a}]set. x = [{atom b}]set. y" . @@ -869,7 +869,7 @@ moreover { assume *: "a \ b" and **: "Abs_res {atom a} x = Abs_res {atom b} y" have #: "atom a \ Abs_res {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff) - have "Abs_res {atom a} ((a \ b) \ y) = (a \ b) \ (Abs_res {atom b} y)" by (simp add: assms) + have "Abs_res {atom a} ((a \ b) \ y) = (a \ b) \ (Abs_res {atom b} y)" by simp also have "\ = Abs_res {atom b} y" by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff) also have "\ = Abs_res {atom a} x" using ** by simp @@ -878,7 +878,7 @@ moreover { assume *: "a \ b" and **: "x = (a \ b) \ y \ atom a \ y" have "Abs_res {atom a} x = Abs_res {atom a} ((a \ b) \ y)" using ** by simp - also have "\ = (a \ b) \ Abs_res {atom b} y" by (simp add: permute_set_def assms) + also have "\ = (a \ b) \ Abs_res {atom b} y" by (simp add: permute_set_def) also have "\ = Abs_res {atom b} y" by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) finally have "Abs_res {atom a} x = Abs_res {atom b} y" . @@ -893,7 +893,7 @@ moreover { assume *: "a \ b" and **: "Abs_lst [atom a] x = Abs_lst [atom b] y" have #: "atom a \ Abs_lst [atom b] y" by (simp add: **[symmetric] Abs_fresh_iff) - have "Abs_lst [atom a] ((a \ b) \ y) = (a \ b) \ (Abs_lst [atom b] y)" by (simp add: assms) + have "Abs_lst [atom a] ((a \ b) \ y) = (a \ b) \ (Abs_lst [atom b] y)" by simp also have "\ = Abs_lst [atom b] y" by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff) also have "\ = Abs_lst [atom a] x" using ** by simp @@ -902,7 +902,7 @@ moreover { assume *: "a \ b" and **: "x = (a \ b) \ y \ atom a \ y" have "Abs_lst [atom a] x = Abs_lst [atom a] ((a \ b) \ y)" using ** by simp - also have "\ = (a \ b) \ Abs_lst [atom b] y" by (simp add: assms) + also have "\ = (a \ b) \ Abs_lst [atom b] y" by simp also have "\ = Abs_lst [atom b] y" by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) finally have "Abs_lst [atom a] x = Abs_lst [atom b] y" . @@ -918,7 +918,7 @@ shows "[{atom a}]set. x = [{atom b}]set. y \ (a = b \ x = y) \ (a \ b \ (b \ a) \ x = y \ atom b \ x)" and "[{atom a}]res. x = [{atom b}]res. y \ (a = b \ x = y) \ (a \ b \ (b \ a) \ x = y \ atom b \ x)" and "[[atom a]]lst. x = [[atom b]]lst. y \ (a = b \ x = y) \ (a \ b \ (b \ a) \ x = y \ atom b \ x)" -using assms by (auto simp: Abs1_eq_iff fresh_permute_left) +by (auto simp: Abs1_eq_iff fresh_permute_left) ML {* diff -r a44479bde681 -r 017e33849f4d Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Nominal2_Base.thy Thu Apr 19 13:57:17 2018 +0100 @@ -7,7 +7,8 @@ theory Nominal2_Base imports "~~/src/HOL/Library/Old_Datatype" "~~/src/HOL/Library/Infinite_Set" - "~~/src/HOL/Quotient_Examples/FSet" + "~~/src/HOL/Library/Multiset" + "~~/src/HOL/Library/FSet" "~~/src/HOL/Library/FinFun" keywords "atom_decl" "equivariance" :: thy_decl @@ -18,7 +19,7 @@ section {* Atoms and Sorts *} -text {* A simple implementation for atom_sorts is strings. *} +text {* A simple implementation for @{text atom_sorts} is strings. *} (* types atom_sort = string *) text {* To deal with Church-like binding we use trees of @@ -611,7 +612,7 @@ lemma permute_multiset [simp]: fixes M N::"('a::pt) multiset" shows "(p \ {#}) = ({#} ::('a::pt) multiset)" - and "(p \ {# x #}) = {# p \ x #}" + and "(p \ add_mset x M) = add_mset (p \ x) (p \ M)" and "(p \ (M + N)) = (p \ M) + (p \ N)" unfolding permute_multiset_def by (simp_all) @@ -619,38 +620,40 @@ subsection {* Permutations for @{typ "'a fset"} *} -lemma permute_fset_rsp[quot_respect]: - shows "(op = ===> list_eq ===> list_eq) permute permute" - unfolding rel_fun_def - by (simp add: set_eqvt[symmetric]) - instantiation fset :: (pt) pt begin -quotient_definition - "permute_fset :: perm \ 'a fset \ 'a fset" -is - "permute :: perm \ 'a list \ 'a list" - by (simp add: set_eqvt[symmetric]) - +context includes fset.lifting begin +lift_definition + "permute_fset" :: "perm \ 'a fset \ 'a fset" +is "permute :: perm \ 'a set \ 'a set" by simp +end + +context includes fset.lifting begin instance proof fix x :: "'a fset" and p q :: "perm" - show "0 \ x = x" by (descending) (simp) - show "(p + q) \ x = p \ q \ x" by (descending) (simp) + show "0 \ x = x" by transfer simp + show "(p + q) \ x = p \ q \ x" by transfer simp qed +end end +context includes fset.lifting +begin lemma permute_fset [simp]: fixes S::"('a::pt) fset" shows "(p \ {||}) = ({||} ::('a::pt) fset)" - and "(p \ insert_fset x S) = insert_fset (p \ x) (p \ S)" - by (lifting permute_list.simps) + and "(p \ finsert x S) = finsert (p \ x) (p \ S)" + apply (transfer, simp add: empty_eqvt) + apply (transfer, simp add: insert_eqvt) + done lemma fset_eqvt: shows "p \ (fset S) = fset (p \ S)" - by (lifting set_eqvt) + by transfer simp +end subsection {* Permutations for @{typ "('a, 'b) finfun"} *} @@ -762,7 +765,7 @@ proof qed (rule permute_int_def) -section {* Infrastructure for Equivariance and Perm_simp *} +section {* Infrastructure for Equivariance and @{text Perm_simp} *} subsection {* Basic functions about permutations *} @@ -792,7 +795,7 @@ (* multisets *) permute_multiset -subsection {* perm_simp infrastructure *} +subsection {* @{text perm_simp} infrastructure *} definition "unpermute p = permute (- p)" @@ -812,7 +815,7 @@ shows "p \ unpermute p x \ x" unfolding unpermute_def by simp -text {* provides perm_simp methods *} +text {* provides @{text perm_simp} methods *} ML_file "nominal_permeq.ML" @@ -974,10 +977,6 @@ unfolding permute_set_eq permute_fun_def by (auto simp: permute_bool_def) -lemma inter_eqvt [eqvt]: - shows "p \ (A \ B) = (p \ A) \ (p \ B)" - unfolding Int_def by simp - lemma Bex_eqvt [eqvt]: shows "p \ (\x \ S. P x) = (\x \ (p \ S). (p \ P) x)" unfolding Bex_def by simp @@ -999,14 +998,22 @@ unfolding UNIV_def by (perm_simp) (rule refl) +lemma inter_eqvt [eqvt]: + shows "p \ (A \ B) = (p \ A) \ (p \ B)" + unfolding Int_def by simp + +lemma Inter_eqvt [eqvt]: + shows "p \ \S = \(p \ S)" + unfolding Inter_eq by simp + lemma union_eqvt [eqvt]: shows "p \ (A \ B) = (p \ A) \ (p \ B)" unfolding Un_def by simp -lemma UNION_eqvt [eqvt]: - shows "p \ (UNION A f) = (UNION (p \ A) (p \ f))" -unfolding UNION_eq -by (perm_simp) (simp) +lemma Union_eqvt [eqvt]: + shows "p \ \A = \(p \ A)" + unfolding Union_eq + by perm_simp rule lemma Diff_eqvt [eqvt]: fixes A B :: "'a::pt set" @@ -1030,16 +1037,6 @@ shows "p \ (f -` A) = (p \ f) -` (p \ A)" unfolding vimage_def by simp -lemma Union_eqvt [eqvt]: - shows "p \ (\ S) = \ (p \ S)" - unfolding Union_eq by simp - -lemma Inter_eqvt [eqvt]: - shows "p \ (\ S) = \ (p \ S)" - unfolding Inter_eq by simp - -thm foldr.simps - lemma foldr_eqvt[eqvt]: "p \ foldr f xs = foldr (p \ f) (p \ xs)" apply(induct xs) @@ -1052,7 +1049,6 @@ lemma Sigma_eqvt: shows "(p \ (X \ Y)) = (p \ X) \ (p \ Y)" unfolding Sigma_def -unfolding SUP_def by (perm_simp) (rule refl) text {* @@ -1109,7 +1105,7 @@ instance apply standard -unfolding Inf_fun_def INF_def +unfolding Inf_fun_def apply(perm_simp) apply(rule refl) done @@ -1200,9 +1196,10 @@ subsubsection {* Equivariance for @{typ "'a fset"} *} +context includes fset.lifting begin lemma in_fset_eqvt [eqvt]: shows "(p \ (x |\| S)) = ((p \ x) |\| (p \ S))" -unfolding in_fset by simp + by transfer simp lemma union_fset_eqvt [eqvt]: shows "(p \ (S |\| T)) = ((p \ S) |\| (p \ T))" @@ -1210,21 +1207,16 @@ lemma inter_fset_eqvt [eqvt]: shows "(p \ (S |\| T)) = ((p \ S) |\| (p \ T))" - apply(descending) - unfolding list_eq_def inter_list_def - apply(simp) - done + by transfer simp lemma subset_fset_eqvt [eqvt]: shows "(p \ (S |\| T)) = ((p \ S) |\| (p \ T))" - apply(descending) - unfolding sub_list_def - apply(simp) - done + by transfer simp lemma map_fset_eqvt [eqvt]: - shows "p \ (map_fset f S) = map_fset (p \ f) (p \ S)" - by (lifting map_eqvt) + shows "p \ (f |`| S) = (p \ f) |`| (p \ S)" + by transfer simp +end subsubsection {* Equivariance for @{typ "('a, 'b) finfun"} *} @@ -1906,7 +1898,7 @@ end *} -subsection {* helper functions for nominal_functions *} +subsection {* helper functions for @{text nominal_functions} *} lemma THE_defaultI2: assumes "\!x. P x" "\x. P x \ Q x" @@ -2146,30 +2138,22 @@ qed lemma Union_supports_multiset: - shows "\{supp x | x. x :# M} supports M" + shows "\{supp x | x. x \# M} supports M" proof - - have sw: "\a b. ((\x. x :# M \ (a \ b) \ x = x) \ (a \ b) \ M = M)" - unfolding permute_multiset_def - apply(induct M) - apply(simp_all) - done - show "(\{supp x | x. x :# M}) supports M" - unfolding supports_def - apply(clarify) - apply(rule sw) - apply(rule swap_fresh_fresh) - apply(simp_all only: fresh_def) - apply(auto) - apply(metis neq0_conv)+ - done + have sw: "\a b. ((\x. x \# M \ (a \ b) \ x = x) \ (a \ b) \ M = M)" + unfolding permute_multiset_def by (induct M) simp_all + have "(\x\set_mset M. supp x) supports M" + by (auto intro!: sw swap_fresh_fresh simp add: fresh_def supports_def) + also have "(\x\set_mset M. supp x) = (\{supp x | x. x \# M})" + by auto + finally show "(\{supp x | x. x \# M}) supports M" . qed lemma Union_included_multiset: fixes M::"('a::fs multiset)" shows "(\{supp x | x. x \# M}) \ supp M" proof - - have "(\{supp x | x. x \# M}) = (\{supp x | x. x \ set_mset M})" by simp - also have "... \ (\x \ set_mset M. supp x)" by auto + have "(\{supp x | x. x \# M}) = (\x \ set_mset M. supp x)" by auto also have "... = supp (set_mset M)" by (simp add: supp_of_finite_sets) also have " ... \ supp M" by (rule supp_set_mset) @@ -2178,7 +2162,7 @@ lemma supp_of_multisets: fixes M::"('a::fs multiset)" - shows "(supp M) = (\{supp x | x. x :# M})" + shows "(supp M) = (\{supp x | x. x \# M})" apply(rule subset_antisym) apply(rule supp_is_subset) apply(rule Union_supports_multiset) @@ -2221,20 +2205,20 @@ unfolding fresh_def by (simp) -lemma supp_insert_fset [simp]: +lemma supp_finsert [simp]: fixes x::"'a::fs" and S::"'a fset" - shows "supp (insert_fset x S) = supp x \ supp S" + shows "supp (finsert x S) = supp x \ supp S" apply(subst supp_fset[symmetric]) apply(simp add: supp_of_finite_insert) done -lemma fresh_insert_fset: +lemma fresh_finsert: fixes x::"'a::fs" and S::"'a fset" - shows "a \ insert_fset x S \ a \ x \ a \ S" + shows "a \ finsert x S \ a \ x \ a \ S" unfolding fresh_def - by (simp) + by simp lemma fset_finite_supp: fixes S::"('a::fs) fset" @@ -3121,7 +3105,7 @@ unfolding atom_eqvt [symmetric] by simp_all -text {* the following two lemmas do not hold for at_base, +text {* the following two lemmas do not hold for @{text at_base}, only for single sort atoms from at *} lemma flip_triple: diff -r a44479bde681 -r 017e33849f4d Nominal/Nominal2_FCB.thy --- a/Nominal/Nominal2_FCB.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/Nominal2_FCB.thy Thu Apr 19 13:57:17 2018 +0100 @@ -396,7 +396,7 @@ done lemma Abs_lst1_fcb2': - fixes a b :: "'a::at" + fixes a b :: "'a::at_base" and x y :: "'b :: fs" and c::"'c :: fs" assumes e: "[[atom a]]lst. x = [[atom b]]lst. y" @@ -411,4 +411,4 @@ apply(simp_all add: fresh_star_def inv_f_f inj_on_def atom_eqvt) done -end \ No newline at end of file +end diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_atoms.ML --- a/Nominal/nominal_atoms.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_atoms.ML Thu Apr 19 13:57:17 2018 +0100 @@ -58,9 +58,9 @@ val lthy = Class.instantiation ([full_tname], [], @{sort at}) thy; val ((_, (_, permute_ldef)), lthy) = - Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; + Specification.definition NONE [] [] ((permute_def_name, []), permute_eqn) lthy; val ((_, (_, atom_ldef)), lthy) = - Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; + Specification.definition NONE [] [] ((atom_def_name, []), atom_eqn) lthy; val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); val permute_def = singleton (Proof_Context.export lthy ctxt_thy) permute_ldef; val atom_def = singleton (Proof_Context.export lthy ctxt_thy) atom_ldef; diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_basics.ML --- a/Nominal/nominal_basics.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_basics.ML Thu Apr 19 13:57:17 2018 +0100 @@ -222,4 +222,4 @@ end (* structure *) -open Nominal_Basic; \ No newline at end of file +open Nominal_Basic; diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_dt_alpha.ML Thu Apr 19 13:57:17 2018 +0100 @@ -246,7 +246,7 @@ val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) - val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) + val all_alpha_intros = map (pair Binding.empty_atts) (flat alpha_intros @ flat alpha_bn_intros) val (alpha_info, lthy') = lthy |> Inductive.add_inductive_i @@ -286,7 +286,7 @@ alpha_bn_tys = alpha_bn_tys, alpha_intros = alpha_intros, alpha_cases = alpha_cases, - alpha_raw_induct = alpha_raw_induct}, Local_Theory.restore lthy') + alpha_raw_induct = alpha_raw_induct}, Local_Theory.reset lthy') (* FIXME disrupts context *) end diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_dt_data.ML --- a/Nominal/nominal_dt_data.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_dt_data.ML Thu Apr 19 13:57:17 2018 +0100 @@ -144,4 +144,4 @@ alpha_cases : thm list, alpha_raw_induct : thm} -end \ No newline at end of file +end diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_dt_quot.ML Thu Apr 19 13:57:17 2018 +0100 @@ -82,7 +82,7 @@ val _ = if is_Const rhs then () else warning "The definiens is not a constant" in - Quotient_Def.add_quotient_def (((binding, mx), Attrib.empty_binding), (lhs, rhs)) rsp_thm ctxt + Quotient_Def.add_quotient_def (((binding, mx), Binding.empty_atts), (lhs, rhs)) rsp_thm ctxt end diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Thu Apr 19 13:57:17 2018 +0100 @@ -11,7 +11,7 @@ val is_recursive_binder: bclause -> bool val define_raw_bns: raw_dt_info -> (binding * typ option * mixfix) list -> - (Attrib.binding * term) list -> local_theory -> + Specification.multi_specs -> local_theory -> (term list * thm list * bn_info list * thm list * local_theory) val define_raw_fvs: raw_dt_info -> bn_info list -> bclause list list list -> @@ -118,7 +118,7 @@ val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy - val (info, lthy2) = prove_termination_fun raw_size_thms (Local_Theory.restore lthy1) + val (info, lthy2) = prove_termination_fun raw_size_thms (Local_Theory.reset lthy1) (* FIXME disrupts context *) val {fs, simps, inducts, ...} = info val raw_bn_induct = (the inducts) @@ -252,12 +252,12 @@ val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map raw_cns_info bclausesss) bn_info val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) - val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) + val all_fun_eqs = map (fn t => ((Binding.empty_atts, t), [], [])) (flat fv_eqs @ flat fv_bn_eqs) val (_, lthy') = Function.add_function all_fun_names all_fun_eqs Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy - val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') + val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.reset lthy') (* FIXME disrupts context *) val {fs, simps, inducts, ...} = info; @@ -324,7 +324,7 @@ val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map raw_cns_info) bn_info val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names - val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs) + val all_fun_eqs = map (fn t => ((Binding.empty_atts, t), [], [])) (flat perm_bn_eqs) val prod_simps = @{thms prod.inject HOL.simp_thms} @@ -332,7 +332,7 @@ Function_Common.default_config (pat_completeness_simp (prod_simps @ raw_inject_thms @ raw_distinct_thms)) lthy - val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') + val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.reset lthy') (* FIXME disrupts context *) val {fs, simps, ...} = info; @@ -412,7 +412,7 @@ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) in - (Attrib.empty_binding, eq) + ((Binding.empty_atts, eq), [], []) end diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_function.ML --- a/Nominal/nominal_function.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_function.ML Thu Apr 19 13:57:17 2018 +0100 @@ -12,19 +12,19 @@ include NOMINAL_FUNCTION_DATA val add_nominal_function: (binding * typ option * mixfix) list -> - (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> + Specification.multi_specs -> Nominal_Function_Common.nominal_function_config -> (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory val add_nominal_function_cmd: (binding * string option * mixfix) list -> - (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> + Specification.multi_specs_cmd -> Nominal_Function_Common.nominal_function_config -> (Proof.context -> tactic) -> bool -> local_theory -> nominal_info * local_theory val nominal_function: (binding * typ option * mixfix) list -> - (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> + Specification.multi_specs -> Nominal_Function_Common.nominal_function_config -> local_theory -> Proof.state val nominal_function_cmd: (binding * string option * mixfix) list -> - (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> + Specification.multi_specs_cmd -> Nominal_Function_Common.nominal_function_config -> bool -> local_theory -> Proof.state val get_info : Proof.context -> term -> nominal_info @@ -102,7 +102,7 @@ val simp_attribs = map (Attrib.internal o K) [Simplifier.simp_add, - Code.add_default_eqn_attribute, + Code.add_default_eqn_attribute Code.Equation, Named_Theorems.add @{named_theorems nitpick_simp}] val psimp_attribs = map (Attrib.internal o K) @@ -203,9 +203,9 @@ end val add_nominal_function = - gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type}) + gen_add_nominal_function false Specification.check_multi_specs (Type_Infer.anyT @{sort type}) fun add_nominal_function_cmd a b c d int = - gen_add_nominal_function int Specification.read_spec "_::type" a b c d + gen_add_nominal_function int Specification.read_multi_specs "_::type" a b c d fun gen_nominal_function do_print prep default_constraint fixspec eqns config lthy = let @@ -218,9 +218,9 @@ end val nominal_function = - gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type}) + gen_nominal_function false Specification.check_multi_specs (Type_Infer.anyT @{sort type}) fun nominal_function_cmd a b c int = - gen_nominal_function int Specification.read_spec "_::type" a b c + gen_nominal_function int Specification.read_multi_specs "_::type" a b c fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |> the_single |> snd @@ -241,16 +241,13 @@ >> (fn opts => fold apply_opt opts default) in fun nominal_function_parser default_cfg = - config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs + config_parser default_cfg -- Parse_Spec.specification end - -(* nominal *) val _ = Outer_Syntax.local_theory_to_proof' @{command_keyword nominal_function} "define general recursive nominal functions" (nominal_function_parser nominal_default_config - >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) - + >> (fn (config, (fixes, specs)) => nominal_function_cmd fixes specs config)) end diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_function_core.ML --- a/Nominal/nominal_function_core.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_function_core.ML Thu Apr 19 13:57:17 2018 +0100 @@ -614,7 +614,7 @@ skip_mono = true} [binding] (* relation *) [] (* no parameters *) - (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *) + (map (fn t => (Binding.empty_atts, t)) intrs) (* intro rules *) [] (* no special monos *) ||> Proof_Context.restore_naming lthy ||> Config.put Inductive.inductive_internals (Config.get lthy Inductive.inductive_internals) @@ -667,7 +667,7 @@ |> Syntax.check_term lthy in Local_Theory.define - ((Binding.name (function_name fname), mixfix), + ((Binding.name (fname ^ "C"), mixfix), ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy end @@ -1025,7 +1025,7 @@ val RCss = map find_calls trees val ((G, GIntro_thms, G_elim, G_induct), lthy) = - PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy + PROFILE "def_graph" (define_graph (defname ^ "_graph") fvar domT ranT clauses RCss) lthy val ((f, (_, f_defthm)), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy @@ -1034,10 +1034,10 @@ val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees val ((R, RIntro_thmss, R_elim), lthy) = - PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy + PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT abstract_qglrs clauses RCss) lthy val (_, lthy) = - Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy + Local_Theory.abbrev Syntax.mode_default ((Binding.name (defname ^ "_dom"), NoSyn), mk_acc domT R) lthy val newthy = Proof_Context.theory_of lthy val clauses = map (transfer_clause_ctx newthy) clauses diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_inductive.ML --- a/Nominal/nominal_inductive.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_inductive.ML Thu Apr 19 13:57:17 2018 +0100 @@ -434,7 +434,7 @@ val avoids_parser = Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) [] - val main_parser = Parse.xname -- avoids_parser + val main_parser = Parse.name -- avoids_parser in val _ = Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive} diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_library.ML Thu Apr 19 13:57:17 2018 +0100 @@ -131,7 +131,7 @@ val atom_ty = dest_fsetT ty val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; in - Const (@{const_name map_fset}, fmap_ty) $ atom_const atom_ty $ t + Const (@{const_name fimage}, fmap_ty) $ atom_const atom_ty $ t end fun mk_atom_list_ty ty t = diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_termination.ML --- a/Nominal/nominal_termination.ML Tue Mar 22 12:18:30 2016 +0000 +++ b/Nominal/nominal_termination.ML Thu Apr 19 13:57:17 2018 +0100 @@ -25,7 +25,7 @@ val simp_attribs = map (Attrib.internal o K) [Simplifier.simp_add, - Code.add_default_eqn_attribute, + Code.add_default_eqn_attribute Code.Equation, Named_Theorems.add @{named_theorems nitpick_simp}] val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) diff -r a44479bde681 -r 017e33849f4d Tutorial/Tutorial1.thy --- a/Tutorial/Tutorial1.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Tutorial/Tutorial1.thy Thu Apr 19 13:57:17 2018 +0100 @@ -1,4 +1,4 @@ -header {* +(* Nominal Isabelle Tutorial at POPL'11 ==================================== @@ -58,7 +58,7 @@ \ sharp (freshness) \ bullet (permutation application) -*} +*) theory Tutorial1 diff -r a44479bde681 -r 017e33849f4d Tutorial/Tutorial1s.thy --- a/Tutorial/Tutorial1s.thy Tue Mar 22 12:18:30 2016 +0000 +++ b/Tutorial/Tutorial1s.thy Thu Apr 19 13:57:17 2018 +0100 @@ -1,5 +1,5 @@ -header {* +(* Nominal Isabelle Tutorial at POPL'11 ==================================== @@ -59,7 +59,7 @@ \ sharp (freshness) \ bullet (permutation application) -*} +*) theory Tutorial1s imports Lambda