--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 \<bullet> (f::foo) = f"
instance
-apply(default)
+apply(standard)
apply(simp_all add: permute_foo_def)
done
--- 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 \<and> [[atom x]]lst. s = [[atom y]]lst. sa
\<longleftrightarrow> [[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 \<Rightarrow> lam \<Rightarrow> bool"
--- 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 \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>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
--- 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 \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
where
- "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
+ "fset (atom |`| Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
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)
--- 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 \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl (p \<bullet> (f x))"
using a
by clarsimp
-
+
nominal_function (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
where
"subst \<theta> (Var X) = lookup \<theta> X"
| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
-| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
+| "fset (atom |`| xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
thm subst_substs_graph_def subst_substs_graph_aux_def
apply(simp add: subst_substs_graph_aux_def eqvt_def)
apply(rule TrueI)
--- 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 \<times> ty) fset \<Rightarrow> bool"
where
v2_Empty[intro]: "valid2 {||}"
-| v2_Insert[intro]: "\<lbrakk>(x, T) |\<notin>| Gamma; valid2 Gamma\<rbrakk> \<Longrightarrow> valid2 (insert_fset (x, T) Gamma)"
+| v2_Insert[intro]: "\<lbrakk>(x, T) |\<notin>| Gamma; valid2 Gamma\<rbrakk> \<Longrightarrow> valid2 (finsert (x, T) Gamma)"
equivariance valid2
@@ -116,7 +116,7 @@
where
t2_Var[intro]: "\<lbrakk>valid2 \<Gamma>; (x, T) |\<in>| \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Var x : T"
| t2_App[intro]: "\<lbrakk>\<Gamma> 2\<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> 2\<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> App t1 t2 : T2"
- | t2_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; insert_fset (x, T1) \<Gamma> 2\<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Lam [x]. t : T1 \<rightarrow> T2"
+ | t2_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; finsert (x, T1) \<Gamma> 2\<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Lam [x]. t : T1 \<rightarrow> T2"
equivariance typing2
@@ -133,12 +133,8 @@
apply(nominal_induct \<Gamma> 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 \<leftrightarrow> x) \<bullet> t)" in subst)
defer
apply(rule t2_Lam)
-apply(simp add: fresh_insert_fset)
+apply(simp add: fresh_finsert)
oops
--- 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 =
--- 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 \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
have "[{atom a}]set. x = [{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
- also have "\<dots> = (a \<leftrightarrow> b) \<bullet> ([{atom b}]set. y)" by (simp add: permute_set_def assms)
+ also have "\<dots> = (a \<leftrightarrow> b) \<bullet> ([{atom b}]set. y)" by (simp add: permute_set_def)
also have "\<dots> = [{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 \<noteq> b" and **: "Abs_res {atom a} x = Abs_res {atom b} y"
have #: "atom a \<sharp> Abs_res {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff)
- have "Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_res {atom b} y)" by (simp add: assms)
+ have "Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_res {atom b} y)" by simp
also have "\<dots> = Abs_res {atom b} y"
by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
also have "\<dots> = Abs_res {atom a} x" using ** by simp
@@ -878,7 +878,7 @@
moreover
{ assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
have "Abs_res {atom a} x = Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
- also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_res {atom b} y" by (simp add: permute_set_def assms)
+ also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_res {atom b} y" by (simp add: permute_set_def)
also have "\<dots> = 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 \<noteq> b" and **: "Abs_lst [atom a] x = Abs_lst [atom b] y"
have #: "atom a \<sharp> Abs_lst [atom b] y" by (simp add: **[symmetric] Abs_fresh_iff)
- have "Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_lst [atom b] y)" by (simp add: assms)
+ have "Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_lst [atom b] y)" by simp
also have "\<dots> = Abs_lst [atom b] y"
by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
also have "\<dots> = Abs_lst [atom a] x" using ** by simp
@@ -902,7 +902,7 @@
moreover
{ assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
have "Abs_lst [atom a] x = Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
- also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_lst [atom b] y" by (simp add: assms)
+ also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_lst [atom b] y" by simp
also have "\<dots> = 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 \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
-using assms by (auto simp: Abs1_eq_iff fresh_permute_left)
+by (auto simp: Abs1_eq_iff fresh_permute_left)
ML {*
--- 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 \<bullet> {#}) = ({#} ::('a::pt) multiset)"
- and "(p \<bullet> {# x #}) = {# p \<bullet> x #}"
+ and "(p \<bullet> add_mset x M) = add_mset (p \<bullet> x) (p \<bullet> M)"
and "(p \<bullet> (M + N)) = (p \<bullet> M) + (p \<bullet> 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 \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
- "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
- by (simp add: set_eqvt[symmetric])
-
+context includes fset.lifting begin
+lift_definition
+ "permute_fset" :: "perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is "permute :: perm \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
+end
+
+context includes fset.lifting begin
instance
proof
fix x :: "'a fset" and p q :: "perm"
- show "0 \<bullet> x = x" by (descending) (simp)
- show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
+ show "0 \<bullet> x = x" by transfer simp
+ show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by transfer simp
qed
+end
end
+context includes fset.lifting
+begin
lemma permute_fset [simp]:
fixes S::"('a::pt) fset"
shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
- and "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
- by (lifting permute_list.simps)
+ and "(p \<bullet> finsert x S) = finsert (p \<bullet> x) (p \<bullet> S)"
+ apply (transfer, simp add: empty_eqvt)
+ apply (transfer, simp add: insert_eqvt)
+ done
lemma fset_eqvt:
shows "p \<bullet> (fset S) = fset (p \<bullet> 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 \<bullet> unpermute p x \<equiv> 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 \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
- unfolding Int_def by simp
-
lemma Bex_eqvt [eqvt]:
shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> 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 \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+ unfolding Int_def by simp
+
+lemma Inter_eqvt [eqvt]:
+ shows "p \<bullet> \<Inter>S = \<Inter>(p \<bullet> S)"
+ unfolding Inter_eq by simp
+
lemma union_eqvt [eqvt]:
shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
unfolding Un_def by simp
-lemma UNION_eqvt [eqvt]:
- shows "p \<bullet> (UNION A f) = (UNION (p \<bullet> A) (p \<bullet> f))"
-unfolding UNION_eq
-by (perm_simp) (simp)
+lemma Union_eqvt [eqvt]:
+ shows "p \<bullet> \<Union>A = \<Union>(p \<bullet> A)"
+ unfolding Union_eq
+ by perm_simp rule
lemma Diff_eqvt [eqvt]:
fixes A B :: "'a::pt set"
@@ -1030,16 +1037,6 @@
shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
unfolding vimage_def by simp
-lemma Union_eqvt [eqvt]:
- shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
- unfolding Union_eq by simp
-
-lemma Inter_eqvt [eqvt]:
- shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)"
- unfolding Inter_eq by simp
-
-thm foldr.simps
-
lemma foldr_eqvt[eqvt]:
"p \<bullet> foldr f xs = foldr (p \<bullet> f) (p \<bullet> xs)"
apply(induct xs)
@@ -1052,7 +1049,6 @@
lemma Sigma_eqvt:
shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> 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 \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
-unfolding in_fset by simp
+ by transfer simp
lemma union_fset_eqvt [eqvt]:
shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
@@ -1210,21 +1207,16 @@
lemma inter_fset_eqvt [eqvt]:
shows "(p \<bullet> (S |\<inter>| T)) = ((p \<bullet> S) |\<inter>| (p \<bullet> T))"
- apply(descending)
- unfolding list_eq_def inter_list_def
- apply(simp)
- done
+ by transfer simp
lemma subset_fset_eqvt [eqvt]:
shows "(p \<bullet> (S |\<subseteq>| T)) = ((p \<bullet> S) |\<subseteq>| (p \<bullet> T))"
- apply(descending)
- unfolding sub_list_def
- apply(simp)
- done
+ by transfer simp
lemma map_fset_eqvt [eqvt]:
- shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
- by (lifting map_eqvt)
+ shows "p \<bullet> (f |`| S) = (p \<bullet> f) |`| (p \<bullet> 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 "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
@@ -2146,30 +2138,22 @@
qed
lemma Union_supports_multiset:
- shows "\<Union>{supp x | x. x :# M} supports M"
+ shows "\<Union>{supp x | x. x \<in># M} supports M"
proof -
- have sw: "\<And>a b. ((\<And>x. x :# M \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x) \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> M = M)"
- unfolding permute_multiset_def
- apply(induct M)
- apply(simp_all)
- done
- show "(\<Union>{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: "\<And>a b. ((\<And>x. x \<in># M \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x) \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> M = M)"
+ unfolding permute_multiset_def by (induct M) simp_all
+ have "(\<Union>x\<in>set_mset M. supp x) supports M"
+ by (auto intro!: sw swap_fresh_fresh simp add: fresh_def supports_def)
+ also have "(\<Union>x\<in>set_mset M. supp x) = (\<Union>{supp x | x. x \<in># M})"
+ by auto
+ finally show "(\<Union>{supp x | x. x \<in># M}) supports M" .
qed
lemma Union_included_multiset:
fixes M::"('a::fs multiset)"
shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M"
proof -
- have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_mset M})" by simp
- also have "... \<subseteq> (\<Union>x \<in> set_mset M. supp x)" by auto
+ have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>x \<in> set_mset M. supp x)" by auto
also have "... = supp (set_mset M)"
by (simp add: supp_of_finite_sets)
also have " ... \<subseteq> supp M" by (rule supp_set_mset)
@@ -2178,7 +2162,7 @@
lemma supp_of_multisets:
fixes M::"('a::fs multiset)"
- shows "(supp M) = (\<Union>{supp x | x. x :# M})"
+ shows "(supp M) = (\<Union>{supp x | x. x \<in># 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 \<union> supp S"
+ shows "supp (finsert x S) = supp x \<union> 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 \<sharp> insert_fset x S \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S"
+ shows "a \<sharp> finsert x S \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> 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:
--- 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
--- 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;
--- 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;
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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}
--- 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 =
--- 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)
--- 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> sharp (freshness)
\<bullet> bullet (permutation application)
-*}
+*)
theory Tutorial1
--- 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> sharp (freshness)
\<bullet> bullet (permutation application)
-*}
+*)
theory Tutorial1s
imports Lambda