--- a/Nominal/Ex/Foo1.thy Thu Dec 23 00:22:41 2010 +0000
+++ b/Nominal/Ex/Foo1.thy Thu Dec 23 00:46:06 2010 +0000
@@ -44,6 +44,7 @@
thm foo.induct
thm foo.inducts
thm foo.exhaust
+thm foo.strong_exhaust
thm foo.fv_defs
thm foo.bn_defs
thm foo.perm_simps
@@ -56,62 +57,6 @@
thm foo.fresh
thm foo.bn_finite
-lemma strong_exhaust1:
- fixes c::"'a::fs"
- assumes "\<exists>name. y = Var name \<Longrightarrow> P"
- and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
- and "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P"
- and "\<exists>(c::'a::fs) assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P"
- and "\<exists>(c::'a::fs) assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P"
- and "\<exists>(c::'a::fs) assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P"
- and "\<exists>(c::'a::fs) assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P"
- shows "P"
-oops
-
-
-lemma strong_exhaust2:
- fixes c::"'a::fs"
- assumes "\<And>name. y = Var name \<Longrightarrow> P"
- and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
- and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P"
- shows "P"
-oops
-
-lemma strong_exhaust1:
- fixes c::"'a::fs"
- assumes "\<And>name. y = Var name \<Longrightarrow> P"
- and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
- and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P"
- shows "P"
-oops
-
-lemma strong_exhaust2:
- assumes "\<And>x y t. as = As x y t \<Longrightarrow> P"
- shows "P"
-apply(rule_tac y="as" in foo.exhaust(2))
-apply(rule assms(1))
-apply(assumption)
-done
-
-lemma strong_exhaust3:
- assumes "as' = BNil \<Longrightarrow> P"
- and "\<And>a as. as' = BAs a as \<Longrightarrow> P"
- shows "P"
-apply(rule_tac y="as'" in foo.exhaust(3))
-apply(rule assms(1))
-apply(assumption)
-apply(rule assms(2))
-apply(assumption)
-done
-
lemma
fixes t::trm
and as::assg
@@ -128,20 +73,17 @@
and a9: "\<And>c. P3 c (BNil)"
and a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)"
shows "P1 c t" "P2 c as" "P3 c as'"
-oops
-(*
using assms
apply(induction_schema)
-apply(rule_tac y="t" and c="c" in strong_exhaust1)
+apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1))
apply(simp_all)[7]
-apply(rule_tac as="as" in strong_exhaust2)
-apply(simp)
-apply(rule_tac as'="as'" in strong_exhaust3)
+apply(rule_tac ya="as"in foo.strong_exhaust(2))
+apply(simp_all)[1]
+apply(rule_tac yb="as'" in foo.strong_exhaust(3))
apply(simp_all)[2]
-apply(relation "measure (sum_case (size o snd) (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z))))")
+apply(relation "measure (sum_case (size o snd) (sum_case (size o snd) (size o snd)))")
apply(simp_all add: foo.size)
done
-*)
end
--- a/Nominal/Ex/Foo2.thy Thu Dec 23 00:22:41 2010 +0000
+++ b/Nominal/Ex/Foo2.thy Thu Dec 23 00:46:06 2010 +0000
@@ -24,10 +24,6 @@
"bn (As x y t a) = [atom x] @ bn a"
| "bn (As_Nil) = []"
-
-
-
-
thm foo.bn_defs
thm foo.permute_bn
thm foo.perm_bn_alpha
@@ -39,6 +35,7 @@
thm foo.induct
thm foo.inducts
thm foo.exhaust
+thm foo.strong_exhaust
thm foo.fv_defs
thm foo.bn_defs
thm foo.perm_simps
@@ -50,308 +47,6 @@
thm foo.supp
thm foo.fresh
-lemma at_set_avoiding5:
- assumes "finite xs"
- and "finite (supp c)"
- shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs"
-using assms
-apply(erule_tac c="c" in at_set_avoiding)
-apply(auto)
-done
-
-
-lemma Abs_rename_lst3:
- fixes x::"'a::fs"
- assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)"
- shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs"
-proof -
- from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter
- by (simp add: fresh_star_Pair fresh_star_set)
- with list_renaming_perm
- obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis
- have "[bs]lst. x = q \<bullet> ([bs]lst. x)"
- apply(rule perm_supp_eq[symmetric])
- using a **
- unfolding fresh_star_Pair
- unfolding Abs_fresh_star_iff
- unfolding fresh_star_def
- by auto
- also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp
- also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp
- finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .
- then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs"
- using * ** by metis
-qed
-
-
-lemma
- fixes c::"'a::fs"
- assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
- shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
-apply -
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
- supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
-defer
-apply(rule at_set_avoiding5)
-apply(simp add: foo.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(erule exE)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-thm Abs_rename_lst
-apply(insert Abs_rename_lst)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg1" in meta_spec)
-apply(drule_tac x="trm1" in meta_spec)
-apply(insert Abs_rename_lst)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg2" in meta_spec)
-apply(drule_tac x="trm2" in meta_spec)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(erule exE)+
-apply(rule a)
-apply(assumption)
-apply(simp only: foo.eq_iff)
-apply(perm_simp add: foo.permute_bn)
-apply(rule conjI)
-apply(rule refl)
-apply(rule conjI)
-apply(rule foo.perm_bn_alpha)
-apply(rule conjI)
-apply(perm_simp add: foo.permute_bn)
-apply(rule refl)
-apply(rule foo.perm_bn_alpha)
-done
-
-lemma
- fixes c::"'a::fs"
- assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
- shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
-apply -
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
- supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
-defer
-apply(rule at_set_avoiding5)
-apply(simp add: foo.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(erule exE)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-apply(insert Abs_rename_lst3)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg1" in meta_spec)
-apply(drule_tac x="trm1" in meta_spec)
-apply(insert Abs_rename_lst3)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg2" in meta_spec)
-apply(drule_tac x="trm2" in meta_spec)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(erule exE)+
-apply(erule conjE)+
-apply(simp add: foo.permute_bn)
-apply(rule a)
-apply(assumption)
-apply(clarify)
-apply(simp (no_asm) only: foo.eq_iff)
-apply(rule conjI)
-apply(assumption)
-apply(rule conjI)
-apply(rule foo.perm_bn_alpha)
-apply(rule conjI)
-apply(assumption)
-apply(rule foo.perm_bn_alpha)
-done
-
-
-lemma
- fixes c::"'a::fs"
- assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
- shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
-apply -
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
- supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
-defer
-apply(rule at_set_avoiding5)
-apply(simp add: foo.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(erule exE)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-apply(simp (no_asm_use) only: foo.permute_bn set_eqvt union_eqvt)
-apply(rule a)
-apply(assumption)
-apply(clarify)
-apply(simp (no_asm) only: foo.eq_iff)
-apply(rule conjI)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(rule fresh_star_supp_conv)
-apply(simp (no_asm_use) add: fresh_star_def)
-apply(simp (no_asm_use) add: Abs_fresh_iff)[1]
-apply(rule ballI)
-apply(auto simp add: fresh_Pair)[1]
-apply(simp (no_asm_use) only: permute_Abs)
-apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt)
-apply(simp)
-apply(rule at_set_avoiding5)
-apply(simp add: multi_recs.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(rule finite_sets_supp)
-apply(simp add: multi_recs.bn_finite)
-done
-
-
-
-lemma test6:
- fixes c::"'a::fs"
- assumes "\<And>name. y = Var name \<Longrightarrow> P"
- and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
- and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>a1 trm1 a2 trm2. \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P"
- and "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
- shows "P"
-apply(rule_tac y="y" in foo.exhaust(1))
-apply(rule assms(1))
-apply(assumption)
-apply(rule assms(2))
-apply(assumption)
-(* lam case *)
-apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
-apply(erule exE)
-apply(insert Abs_rename_lst)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="[atom name]" in meta_spec)
-apply(drule_tac x="trm" in meta_spec)
-apply(simp only: fresh_star_Pair set.simps)
-apply(drule meta_mp)
-apply(simp add: fresh_star_def fresh_Nil fresh_Cons fresh_atom_at_base)
-apply(erule exE)
-apply(rule assms(3))
-apply(perm_simp)
-apply(erule conjE)+
-apply(assumption)
-apply(clarify)
-apply(simp (no_asm) add: foo.eq_iff)
-apply(perm_simp)
-apply(assumption)
-apply(rule at_set_avoiding1)
-apply(simp)
-apply(simp add: finite_supp)
-(* let1 case *)
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)")
-apply(erule exE)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-apply(insert Abs_rename_lst)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg1" in meta_spec)
-apply(drule_tac x="trm1" in meta_spec)
-apply(insert Abs_rename_lst)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg2" in meta_spec)
-apply(drule_tac x="trm2" in meta_spec)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(erule exE)+
-apply(rule assms(4))
-apply(assumption)
-apply(simp add: foo.eq_iff refl)
-apply(rule conjI)
-apply(perm_simp add: foo.permute_bn)
-apply(rule refl)
-apply(rule conjI)
-apply(rule foo.perm_bn_alpha)
-apply(rule conjI)
-apply(perm_simp add: foo.permute_bn)
-apply(rule refl)
-apply(rule foo.perm_bn_alpha)
-apply(rule at_set_avoiding1)
-apply(simp)
-apply(simp add: finite_supp)
-(* let2 case *)
-apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)")
-apply(erule exE)
-apply(rule assms(5))
-apply(simp only:)
-apply(simp only: foo.eq_iff)
-apply(insert Abs_rename_list)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec)
-apply(drule_tac x="trm1" in meta_spec)
-apply(insert Abs_rename_list)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="[atom name2]" in meta_spec)
-apply(drule_tac x="trm2" in meta_spec)
-apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_Pair fresh_star_list fresh_star_Un, simp)
-apply(auto)[1]
-apply(perm_simp)
-apply(auto simp add: fresh_star_def)[1]
-apply(perm_simp)
-apply(auto simp add: fresh_star_def)[1]
-apply(perm_simp)
-apply(auto simp add: fresh_star_def)[1]
-apply(drule meta_mp)
-apply(perm_simp)
-apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1]
-apply(erule exE)+
-apply(rule exI)+
-apply(perm_simp add: foo.permute_bn)
-apply(rule conjI)
-prefer 2
-apply(rule conjI)
-apply(assumption)
-apply(assumption)
-apply(simp add: fresh_star_Pair)
-apply(simp add: fresh_star_def)
-apply(rule at_set_avoiding1)
-apply(simp)
-apply(simp add: finite_supp)
-done
-
-lemma test5:
- fixes c::"'a::fs"
- assumes "\<And>name. y = Var name \<Longrightarrow> P"
- and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
- and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>a1 trm1 a2 trm2. \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P"
- and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P"
- shows "P"
-apply(rule_tac y="y" in test6)
-apply(erule exE)+
-apply(rule assms(1))
-apply(assumption)
-apply(erule exE)+
-apply(rule assms(2))
-apply(assumption)
-apply(rule assms(3))
-apply(auto)[2]
-apply(erule exE)+
-apply(rule assms(4))
-apply(auto)[2]
-apply(erule exE)+
-apply(rule assms(5))
-apply(auto)[2]
-done
-
-
lemma strong_induct:
fixes c :: "'a :: fs"
and assg :: assg and trm :: trm
@@ -362,15 +57,15 @@
\<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; \<And>d. P2 c a1; \<And>d. P1 d t1; \<And>d. P2 d a2; \<And>d. P1 d t2\<rbrakk>
\<Longrightarrow> P1 c (Let1 a1 t1 a2 t2)"
and a4: "\<And>n1 n2 t1 t2 c.
- \<lbrakk>{atom n1, atom n2} \<sharp>* c; \<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (Let2 n1 n2 t1 t2)"
+ \<lbrakk>({atom n1} \<union> {atom n2}) \<sharp>* c; \<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (Let2 n1 n2 t1 t2)"
and a5: "\<And>c. P2 c As_Nil"
and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)"
shows "P1 c trm" "P2 c assg"
using assms
apply(induction_schema)
- apply(rule_tac y="trm" and c="c" in test5)
+ apply(rule_tac y="trm" and c="c" in foo.strong_exhaust(1))
apply(simp_all)[5]
- apply(rule_tac y="assg" in foo.exhaust(2))
+ apply(rule_tac ya="assg" in foo.strong_exhaust(2))
apply(simp_all)[2]
apply(relation "measure (sum_case (size o snd) (size o snd))")
apply(simp_all add: foo.size)
--- a/Nominal/Nominal2.thy Thu Dec 23 00:22:41 2010 +0000
+++ b/Nominal/Nominal2.thy Thu Dec 23 00:46:06 2010 +0000
@@ -16,250 +16,6 @@
use "nominal_dt_quot.ML"
ML {* open Nominal_Dt_Quot *}
-text {* TEST *}
-
-
-ML {*
-(* adds a freshness condition to the assumptions *)
-fun mk_ecase_prems lthy c (params, prems, concl) bclauses =
- let
- val tys = map snd params
- val binders = get_all_binders bclauses
-
- fun prep_binder (opt, i) =
- let
- val t = Bound (length tys - i - 1)
- in
- case opt of
- NONE => setify_ty lthy (nth tys i) t
- | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)
- end
-
- val prems' =
- case binders of
- [] => prems (* case: no binders *)
- | _ => binders (* case: binders *)
- |> map prep_binder
- |> fold_union_env tys
- |> (fn t => mk_fresh_star t c)
- |> (fn t => HOLogic.mk_Trueprop t :: prems)
- in
- mk_full_horn params prems' concl
- end
-*}
-
-
-ML {*
-(* derives the freshness theorem that there exists a p, such that
- (p o as) #* (c, t1,\<dots>, tn) *)
-fun fresh_thm ctxt c parms binders bn_finite_thms =
- let
- fun prep_binder (opt, i) =
- case opt of
- NONE => setify ctxt (nth parms i)
- | SOME bn => to_set (bn $ (nth parms i))
-
- fun prep_binder2 (opt, i) =
- case opt of
- NONE => atomify ctxt (nth parms i)
- | SOME bn => bn $ (nth parms i)
-
- val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders))
- val lhs = binders
- |> map prep_binder
- |> fold_union
- |> mk_perm (Bound 0)
-
- val goal = mk_fresh_star lhs rhs
- |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t))
- |> HOLogic.mk_Trueprop
-
- val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp}
- @ @{thms finite.intros finite_Un finite_set finite_fset}
- in
- Goal.prove ctxt [] [] goal
- (K (HEADGOAL (rtac @{thm at_set_avoiding1}
- THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
- end
-*}
-
-ML {*
-fun abs_const bmode ty =
- let
- val (const_name, binder_ty, abs_ty) =
- case bmode of
- Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})
- | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set})
- | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res})
- in
- Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty]))
- end
-
-fun mk_abs bmode trm1 trm2 =
- abs_const bmode (fastype_of trm2) $ trm1 $ trm2
-
-fun is_abs_eq thm =
- let
- fun is_abs trm =
- case (head_of trm) of
- Const (@{const_name "Abs_set"}, _) => true
- | Const (@{const_name "Abs_lst"}, _) => true
- | Const (@{const_name "Abs_res"}, _) => true
- | _ => false
- in
- thm |> prop_of
- |> HOLogic.dest_Trueprop
- |> HOLogic.dest_eq
- |> fst
- |> is_abs
- end
-*}
-
-
-
-ML {*
-(* derives an abs_eq theorem of the form
-
- Exists q. [as].x = [p o as].(q o x) for non-recursive binders
- Exists q. [as].x = [q o as].(q o x) for recursive binders
-*)
-fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns
- (bclause as (BC (bmode, binders, bodies))) =
- case binders of
- [] => []
- | _ =>
- let
- val rec_flag = is_recursive_binder bclause
- val binder_trm = comb_binders ctxt bmode parms binders
- val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
-
- val abs_lhs = mk_abs bmode binder_trm body_trm
- val abs_rhs =
- if rec_flag
- then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm)
- else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm)
-
- val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
- val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm)
-
- val goal = HOLogic.mk_conj (abs_eq, peq)
- |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
- |> HOLogic.mk_Trueprop
-
- val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
- @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
- fresh_star_set} @ @{thms finite.intros finite_fset}
-
- val tac1 =
- if rec_flag
- then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
- else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
-
- val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss]
- in
- [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
- |> (if rec_flag
- then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
- else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ]
- end
-*}
-
-
-
-lemma setify:
- shows "xs = ys \<Longrightarrow> set xs = set ys"
- by simp
-
-ML {*
-fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas
- prems bclausess qexhaust_thm =
- let
- fun aux_tac prem bclauses =
- case (get_all_binders bclauses) of
- [] => EVERY' [rtac prem, atac]
- | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>
- let
- val parms = map (term_of o snd) params
- val fthm = fresh_thm ctxt c parms binders bn_finite_thms
-
- val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
- val (([(_, fperm)], fprops), ctxt') = Obtain.result
- (K (EVERY1 [etac exE,
- full_simp_tac (HOL_basic_ss addsimps ss),
- REPEAT o (etac @{thm conjE})])) [fthm] ctxt
-
- val abs_eq_thms = flat
- (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses)
-
- val ((_, eqs), ctxt'') = Obtain.result
- (K (EVERY1
- [ REPEAT o (etac @{thm exE}),
- REPEAT o (etac @{thm conjE}),
- REPEAT o (dtac @{thm setify}),
- full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt'
-
- val (abs_eqs, peqs) = split_filter is_abs_eq eqs
-
- val fprops' =
- map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
- @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
-
- (* for freshness conditions *)
- val tac1 = SOLVED' (EVERY'
- [ simp_tac (HOL_basic_ss addsimps peqs),
- rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
- conj_tac (DETERM o resolve_tac fprops') ])
-
- (* for equalities between constructors *)
- val tac2 = SOLVED' (EVERY'
- [ rtac (@{thm ssubst} OF prems),
- rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
- rewrite_goal_tac (map safe_mk_equiv abs_eqs),
- conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ])
-
- (* proves goal "P" *)
- val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
- (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
- |> singleton (ProofContext.export ctxt'' ctxt)
- in
- rtac side_thm 1
- end) ctxt
- in
- EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]
- end
-*}
-
-ML {*
-fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns
- perm_bn_alphas =
- let
- val ((_, exhausts'), lthy') = Variable.import true exhausts lthy
-
- val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
- val c = Free (c, TFree (a, @{sort fs}))
-
- val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)
- |> map prop_of
- |> map Logic.strip_horn
- |> split_list
-
- val ecases' = (map o map) strip_full_horn ecases
-
- val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss
-
- fun tac bclausess exhaust {prems, context} =
- case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas
- prems bclausess exhaust
-
- fun prove prems bclausess exhaust concl =
- Goal.prove lthy'' [] prems concl (tac bclausess exhaust)
- in
- map4 prove premss bclausesss exhausts' main_concls
- |> ProofContext.export lthy'' lthy
- end
-*}
-
-
ML {*
val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
--- a/Nominal/ROOT.ML Thu Dec 23 00:22:41 2010 +0000
+++ b/Nominal/ROOT.ML Thu Dec 23 00:46:06 2010 +0000
@@ -22,8 +22,8 @@
"Ex/SystemFOmega",
"Ex/TypeSchemes",
"Ex/TypeVarsTest",
- (*"Ex/Foo1",
- "Ex/Foo2",*)
+ "Ex/Foo1",
+ "Ex/Foo2",
"Ex/CoreHaskell",
"Ex/CoreHaskell2"
];
--- a/Nominal/nominal_dt_quot.ML Thu Dec 23 00:22:41 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML Thu Dec 23 00:46:06 2010 +0000
@@ -3,7 +3,7 @@
Author: Cezary Kaliszyk
Performing quotient constructions, lifting theorems and
- deriving support propoerties for the quotient types.
+ deriving support properties for the quotient types.
*)
signature NOMINAL_DT_QUOT =
@@ -38,6 +38,10 @@
val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
thm list -> Proof.context -> thm list
+
+ val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list ->
+ thm list -> thm list -> thm list -> thm list -> thm list
+
end
structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -373,5 +377,236 @@
|> map (simplify (HOL_basic_ss addsimps @{thms id_def}))
end
+
+(** proves strong exhauts theorems **)
+
+
+(* fixme: move into nominal_library *)
+fun abs_const bmode ty =
+ let
+ val (const_name, binder_ty, abs_ty) =
+ case bmode of
+ Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})
+ | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set})
+ | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res})
+ in
+ Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty]))
+ end
+
+fun mk_abs bmode trm1 trm2 =
+ abs_const bmode (fastype_of trm2) $ trm1 $ trm2
+
+fun is_abs_eq thm =
+ let
+ fun is_abs trm =
+ case (head_of trm) of
+ Const (@{const_name "Abs_set"}, _) => true
+ | Const (@{const_name "Abs_lst"}, _) => true
+ | Const (@{const_name "Abs_res"}, _) => true
+ | _ => false
+ in
+ thm |> prop_of
+ |> HOLogic.dest_Trueprop
+ |> HOLogic.dest_eq
+ |> fst
+ |> is_abs
+ end
+
+
+(* adds a freshness condition to the assumptions *)
+fun mk_ecase_prems lthy c (params, prems, concl) bclauses =
+ let
+ val tys = map snd params
+ val binders = get_all_binders bclauses
+
+ fun prep_binder (opt, i) =
+ let
+ val t = Bound (length tys - i - 1)
+ in
+ case opt of
+ NONE => setify_ty lthy (nth tys i) t
+ | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)
+ end
+
+ val prems' =
+ case binders of
+ [] => prems (* case: no binders *)
+ | _ => binders (* case: binders *)
+ |> map prep_binder
+ |> fold_union_env tys
+ |> (fn t => mk_fresh_star t c)
+ |> (fn t => HOLogic.mk_Trueprop t :: prems)
+ in
+ mk_full_horn params prems' concl
+ end
+
+
+(* derives the freshness theorem that there exists a p, such that
+ (p o as) #* (c, t1,..., tn) *)
+fun fresh_thm ctxt c parms binders bn_finite_thms =
+ let
+ fun prep_binder (opt, i) =
+ case opt of
+ NONE => setify ctxt (nth parms i)
+ | SOME bn => to_set (bn $ (nth parms i))
+
+ fun prep_binder2 (opt, i) =
+ case opt of
+ NONE => atomify ctxt (nth parms i)
+ | SOME bn => bn $ (nth parms i)
+
+ val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders))
+ val lhs = binders
+ |> map prep_binder
+ |> fold_union
+ |> mk_perm (Bound 0)
+
+ val goal = mk_fresh_star lhs rhs
+ |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t))
+ |> HOLogic.mk_Trueprop
+
+ val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp}
+ @ @{thms finite.intros finite_Un finite_set finite_fset}
+ in
+ Goal.prove ctxt [] [] goal
+ (K (HEADGOAL (rtac @{thm at_set_avoiding1}
+ THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
+ end
+
+
+(* derives an abs_eq theorem of the form
+
+ Exists q. [as].x = [p o as].(q o x) for non-recursive binders
+ Exists q. [as].x = [q o as].(q o x) for recursive binders
+*)
+fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns
+ (bclause as (BC (bmode, binders, bodies))) =
+ case binders of
+ [] => []
+ | _ =>
+ let
+ val rec_flag = is_recursive_binder bclause
+ val binder_trm = comb_binders ctxt bmode parms binders
+ val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
+
+ val abs_lhs = mk_abs bmode binder_trm body_trm
+ val abs_rhs =
+ if rec_flag
+ then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm)
+ else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm)
+
+ val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
+ val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm)
+
+ val goal = HOLogic.mk_conj (abs_eq, peq)
+ |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
+ |> HOLogic.mk_Trueprop
+
+ val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
+ @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
+ fresh_star_set} @ @{thms finite.intros finite_fset}
+
+ val tac1 =
+ if rec_flag
+ then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
+ else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
+
+ val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss]
+ in
+ [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
+ |> (if rec_flag
+ then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
+ else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ]
+ end
+
+
+val setify = @{lemma "xs = ys ==> set xs = set ys" by simp}
+
+fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas
+ prems bclausess qexhaust_thm =
+ let
+ fun aux_tac prem bclauses =
+ case (get_all_binders bclauses) of
+ [] => EVERY' [rtac prem, atac]
+ | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>
+ let
+ val parms = map (term_of o snd) params
+ val fthm = fresh_thm ctxt c parms binders bn_finite_thms
+
+ val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
+ val (([(_, fperm)], fprops), ctxt') = Obtain.result
+ (K (EVERY1 [etac exE,
+ full_simp_tac (HOL_basic_ss addsimps ss),
+ REPEAT o (etac @{thm conjE})])) [fthm] ctxt
+
+ val abs_eq_thms = flat
+ (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses)
+
+ val ((_, eqs), ctxt'') = Obtain.result
+ (K (EVERY1
+ [ REPEAT o (etac @{thm exE}),
+ REPEAT o (etac @{thm conjE}),
+ REPEAT o (dtac setify),
+ full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt'
+
+ val (abs_eqs, peqs) = split_filter is_abs_eq eqs
+
+ val fprops' =
+ map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
+ @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
+
+ (* for freshness conditions *)
+ val tac1 = SOLVED' (EVERY'
+ [ simp_tac (HOL_basic_ss addsimps peqs),
+ rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
+ conj_tac (DETERM o resolve_tac fprops') ])
+
+ (* for equalities between constructors *)
+ val tac2 = SOLVED' (EVERY'
+ [ rtac (@{thm ssubst} OF prems),
+ rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
+ rewrite_goal_tac (map safe_mk_equiv abs_eqs),
+ conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ])
+
+ (* proves goal "P" *)
+ val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
+ (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
+ |> singleton (ProofContext.export ctxt'' ctxt)
+ in
+ rtac side_thm 1
+ end) ctxt
+ in
+ EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]
+ end
+
+
+fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns
+ perm_bn_alphas =
+ let
+ val ((_, exhausts'), lthy') = Variable.import true exhausts lthy
+
+ val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
+ val c = Free (c, TFree (a, @{sort fs}))
+
+ val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)
+ |> map prop_of
+ |> map Logic.strip_horn
+ |> split_list
+
+ val ecases' = (map o map) strip_full_horn ecases
+
+ val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss
+
+ fun tac bclausess exhaust {prems, context} =
+ case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas
+ prems bclausess exhaust
+
+ fun prove prems bclausess exhaust concl =
+ Goal.prove lthy'' [] prems concl (tac bclausess exhaust)
+ in
+ map4 prove premss bclausesss exhausts' main_concls
+ |> ProofContext.export lthy'' lthy
+ end
+
end (* structure *)