Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified exhaust proofs
authorChristian Urban <urbanc@in.tum.de>
Wed, 29 Sep 2010 16:49:13 -0400
changeset 2503 cc5d23547341
parent 2500 3b6a70e73006
child 2504 68ee6913fa8d
simplified exhaust proofs
Nominal/Ex/Foo1.thy file | annotate | diff | comparison | revisions
Nominal/Ex/Lambda.thy file | annotate | diff | comparison | revisions
Nominal/Ex/Let.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/Foo1.thy	Wed Sep 29 09:47:26 2010 -0400
+++ b/Nominal/Ex/Foo1.thy	Wed Sep 29 16:49:13 2010 -0400
@@ -157,26 +157,26 @@
 
 lemma strong_exhaust1:
   fixes c::"'a::fs"
-  assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>assn trm ca. \<lbrakk>set (bn1 assn) \<sharp>* ca; c = ca; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>assn trm ca. \<lbrakk>set (bn2 assn) \<sharp>* ca; c = ca; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>assn trm ca. \<lbrakk>set (bn3 assn) \<sharp>* ca; c = ca; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
+  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"
   shows "P"
 apply(rule_tac y="y" in foo.exhaust(1))
 apply(rule assms(1))
-apply(auto)[2]
+apply(assumption)
 apply(rule assms(2))
-apply(auto)[2]
+apply(assumption)
 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
 apply(rule assms(3))
 apply(perm_simp)
 apply(assumption)
-apply(rule refl)
 apply(drule supp_perm_eq[symmetric])
+apply(perm_simp)
 apply(simp)
 apply(rule at_set_avoiding2)
 apply(simp add: finite_supp)
@@ -187,13 +187,10 @@
 apply(erule exE)
 apply(erule conjE)
 apply(rule assms(4))
-apply(simp add: set_eqvt)
-apply(simp add: tt1)
-apply(rule refl)
-apply(simp)
+apply(perm_simp add: tt1)
+apply(assumption)
+apply(drule supp_perm_eq[symmetric])
 apply(simp add: foo.eq_iff)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
 apply(simp add: tt1 uu1)
 apply(rule at_set_avoiding2)
 apply(simp add: finite_supp)
@@ -206,8 +203,6 @@
 apply(rule assms(5))
 apply(simp add: set_eqvt)
 apply(simp add: tt2)
-apply(rule refl)
-apply(simp)
 apply(simp add: foo.eq_iff)
 apply(drule supp_perm_eq[symmetric])
 apply(simp)
@@ -223,8 +218,6 @@
 apply(rule assms(6))
 apply(simp add: set_eqvt)
 apply(simp add: tt3)
-apply(rule refl)
-apply(simp)
 apply(simp add: foo.eq_iff)
 apply(drule supp_perm_eq[symmetric])
 apply(simp)
@@ -236,14 +229,12 @@
 apply(simp add: Abs_fresh_star)
 done
 
-thm foo.exhaust
-
 lemma strong_exhaust2:
-  assumes "\<And>x y t ca. \<lbrakk>c = ca; as = As x y t\<rbrakk> \<Longrightarrow> P" 
+  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(auto)[2]
+apply(assumption)
 done
 
 
@@ -261,17 +252,11 @@
   shows "P1 c t" "P2 c as"
 using assms
 apply(induction_schema)
-apply(rule_tac y="t" in strong_exhaust1)
-apply(blast)
-apply(blast)
-apply(blast)
-apply(blast)
-apply(blast)
-apply(blast)
+apply(rule_tac y="t" and c="c" in strong_exhaust1)
+apply(simp_all)[6]
 apply(rule_tac as="as" in strong_exhaust2)
-apply(blast)
+apply(simp)
 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")
-apply(auto)[1]
 apply(simp_all add: foo.size)
 done
 
--- a/Nominal/Ex/Lambda.thy	Wed Sep 29 09:47:26 2010 -0400
+++ b/Nominal/Ex/Lambda.thy	Wed Sep 29 16:49:13 2010 -0400
@@ -26,20 +26,19 @@
 
 lemma strong_exhaust:
   fixes c::"'a::fs"
-  assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>lam1 lam2 ca. \<lbrakk>c = ca; y = App lam1 lam2\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>name lam ca. \<lbrakk>c = ca; atom name \<sharp> ca; y = Lam name lam\<rbrakk> \<Longrightarrow> P"
+  assumes "\<And>name. \<lbrakk>y = Var name\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>lam1 lam2. \<lbrakk>y = App lam1 lam2\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>name lam. \<lbrakk>atom name \<sharp> c; y = Lam name lam\<rbrakk> \<Longrightarrow> P"
   shows "P"
 apply(rule_tac y="y" in lam.exhaust)
 apply(rule assms(1))
-apply(auto)[2]
+apply(assumption)
 apply(rule assms(2))
-apply(auto)[2]
+apply(assumption)
 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom name)) \<sharp> c \<and> supp (Lam name lam) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
 apply(rule assms(3))
-apply(rule refl)
 apply(simp add: atom_eqvt)
 apply(clarify)
 apply(drule supp_perm_eq[symmetric])
@@ -64,10 +63,7 @@
 apply(blast)
 apply(blast)
 apply(relation "measure (\<lambda>(x,y). size y)")
-apply(auto)[1]
-apply(simp add: lam.size)
-apply(simp add: lam.size)
-apply(simp add: lam.size)
+apply(simp_all add: lam.size)
 done
 
 section {* Strong Induction Principles*}
--- a/Nominal/Ex/Let.thy	Wed Sep 29 09:47:26 2010 -0400
+++ b/Nominal/Ex/Let.thy	Wed Sep 29 16:49:13 2010 -0400
@@ -74,23 +74,22 @@
 
 lemma strong_exhaust1:
   fixes c::"'a::fs"
-  assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>assn trm ca. \<lbrakk>set (bn assn) \<sharp>* ca; c = ca; y = Let assn trm\<rbrakk> \<Longrightarrow> P"
+  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 (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P"
   shows "P"
 apply(rule_tac y="y" in trm_assn.exhaust(1))
 apply(rule assms(1))
-apply(auto)[2]
+apply(assumption)
 apply(rule assms(2))
-apply(auto)[2]
+apply(assumption)
 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
 apply(rule assms(3))
 apply(perm_simp)
 apply(assumption)
-apply(rule refl)
 apply(drule supp_perm_eq[symmetric])
 apply(simp)
 apply(rule at_set_avoiding2)
@@ -98,13 +97,12 @@
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(simp add: trm_assn.fresh fresh_star_def)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* c \<and> supp ([bn assn]lst.trm) \<sharp>* q")
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
-apply(rule assms(4))
+apply(rule_tac assms(4))
 apply(simp add: set_eqvt)
 apply(simp add: tt)
-apply(rule refl)
 apply(simp)
 apply(simp add: trm_assn.eq_iff)
 apply(drule supp_perm_eq[symmetric])
@@ -119,14 +117,14 @@
 
 
 lemma strong_exhaust2:
-  assumes "\<And>ca. \<lbrakk>c = ca; as = ANil\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>x t assn ca. \<lbrakk>c = ca; as = ACons x t assn\<rbrakk> \<Longrightarrow> P" 
+  assumes "as = ANil \<Longrightarrow> P" 
+  and     "\<And>x t assn. \<lbrakk>as = ACons x t assn\<rbrakk> \<Longrightarrow> P" 
   shows "P"
 apply(rule_tac y="as" in trm_assn.exhaust(2))
 apply(rule assms(1))
-apply(auto)[2]
+apply(assumption)
 apply(rule assms(2))
-apply(auto)[2]
+apply(assumption)+
 done
 
 
@@ -152,8 +150,7 @@
 apply(blast)
 apply(blast)
 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")
-apply(auto)[1]
-apply(simp_all add: trm_assn.size)[7]
+apply(simp_all add: trm_assn.size)
 done
 
 text {* *}
nominal2