--- a/Nominal/Ex/Let.thy Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Ex/Let.thy Mon Sep 27 12:19:17 2010 -0400
@@ -27,26 +27,8 @@
thm trm_assn.inducts
thm trm_assn.distinct
thm trm_assn.supp
-
-
-lemma supp_fresh_eq:
- assumes "supp x = supp y"
- shows "a \<sharp> x \<longleftrightarrow> a \<sharp> y"
-using assms by (simp add: fresh_def)
+thm trm_assn.fresh
-lemma supp_not_in:
- assumes "x = y"
- shows "a \<notin> x \<longleftrightarrow> a \<notin> y"
-using assms
-by (simp add: fresh_def)
-
-lemmas freshs =
- trm_assn.supp(1)[THEN supp_not_in, folded fresh_def]
- trm_assn.supp(2)[THEN supp_not_in, simplified, folded fresh_def]
- trm_assn.supp(3)[THEN supp_not_in, folded fresh_def]
- trm_assn.supp(4)[THEN supp_not_in, folded fresh_def]
- trm_assn.supp(5)[THEN supp_not_in, simplified, folded fresh_def]
- trm_assn.supp(6)[THEN supp_not_in, simplified, folded fresh_def]
lemma fin_bn:
shows "finite (set (bn l))"
@@ -83,7 +65,7 @@
apply(simp)
apply(rule test_trm_test_assn.intros)
apply(assumption)
-apply(simp add: freshs fresh_star_def)
+apply(simp add: trm_assn.fresh fresh_star_def)
apply(simp)
defer
apply(simp)
@@ -93,10 +75,11 @@
apply(assumption)
apply(assumption)
apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
-apply(rule eq_iffs(4)[THEN iffD2])
+apply(rule trm_assn.eq_iff(4)[THEN iffD2])
defer
apply(rule test_trm_test_assn.intros)
prefer 3
+apply(simp add: fresh_star_def trm_assn.fresh)
thm freshs
--"HERE"
--- a/Nominal/Ex/SingleLet.thy Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Ex/SingleLet.thy Mon Sep 27 12:19:17 2010 -0400
@@ -13,7 +13,7 @@
| Let a::"assg" t::"trm" bind "bn a" in t
| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
| Bar x::"name" y::"name" t::"trm" bind y x in t x y
-| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set) x in t2
+| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (res) x in t2
and assg =
As "name" x::"name" t::"trm" bind x in t
binder
@@ -21,6 +21,8 @@
where
"bn (As x y t) = [atom x]"
+
+
thm single_let.distinct
thm single_let.induct
thm single_let.inducts
@@ -34,7 +36,7 @@
thm single_let.supports
thm single_let.fsupp
thm single_let.supp
-thm single_let.size
+thm single_let.fresh
end
--- a/Nominal/Ex/TypeSchemes.thy Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Ex/TypeSchemes.thy Mon Sep 27 12:19:17 2010 -0400
@@ -24,7 +24,7 @@
thm ty_tys.fv_bn_eqvt
thm ty_tys.size_eqvt
thm ty_tys.supports
-thm ty_tys.fsupp
+thm ty_tys.supp
(* defined as two separate nominal datatypes *)
@@ -45,7 +45,7 @@
thm tys2.fv_bn_eqvt
thm tys2.size_eqvt
thm tys2.supports
-thm tys2.fsupp
+thm tys2.supp
--- a/Nominal/Nominal2.thy Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Nominal2.thy Mon Sep 27 12:19:17 2010 -0400
@@ -571,12 +571,24 @@
(* postprocessing of eq and fv theorems *)
val qeq_iffs' = qeq_iffs
- |> map (simplify (HOL_basic_ss addsimps
- (@{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]} @ qfv_supp_thms)))
+ |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms))
+ |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]}))
val qsupp_constrs = qfv_defs
|> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms)))
+ val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}
+ val transform_thms =
+ [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp},
+ @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp},
+ @{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp},
+ @{thm fresh_def[symmetric]}]
+
+ val qfresh_constrs = qsupp_constrs
+ |> map (fn thm => thm RS transform_thm)
+ |> map (simplify (HOL_basic_ss addsimps transform_thms))
+
+
(* noting the theorems *)
(* generating the prefix for the theorem names *)
@@ -599,6 +611,7 @@
||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
+ ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
in
(0, lthy9')
end handle TEST ctxt => (0, ctxt)
--- a/Nominal/nominal_dt_supp.ML Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/nominal_dt_supp.ML Mon Sep 27 12:19:17 2010 -0400
@@ -20,8 +20,6 @@
structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
struct
-fun lookup xs x = the (AList.lookup (op=) xs x)
-
(* supports lemmas for constructors *)
fun mk_supports_goal ctxt qtrm =