# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1290665205 -32400
# Node ID 64abcfddb0c1a299b291acb305e6680a7b036fb1
# Parent  d8a676a6904795f10000b4d055d6991a6553e4d8
foo2 strong induction

diff -r d8a676a69047 -r 64abcfddb0c1 Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Wed Nov 24 17:44:50 2010 +0900
+++ b/Nominal/Ex/Foo2.thy	Thu Nov 25 15:06:45 2010 +0900
@@ -112,7 +112,7 @@
   apply simp
   by (metis assms(2) atom_eqvt fresh_perm)
 
-lemma strong_exhaust1:
+lemma strong_exhaust1_pre:
   fixes c::"'a::fs"
   assumes "\<And>name. y = Var name \<Longrightarrow> P" 
   and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
@@ -209,7 +209,7 @@
 apply (simp add: fresh_star_def supp_atom)
 done
 
-lemma strong_exhaust2:
+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"
@@ -218,7 +218,7 @@
     \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 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 strong_exhaust1)
+  apply (rule strong_exhaust1_pre)
   apply (erule assms)
   apply (erule assms)
   apply (erule assms) apply assumption
@@ -271,6 +271,28 @@
 apply (simp add: fresh_def supp_Pair supp_Abs supp_atom)
 done
 
+lemma strong_induct:
+  fixes c :: "'a :: fs"
+  and assg :: assg and trm :: trm
+  assumes a0: "\<And>name c. P1 c (Var name)"
+  and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)"
+  and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)"
+  and a3: "\<And>assg1 trm1 assg2 trm2 c. \<lbrakk>\<And>d. P2 c assg1; \<And>d. P1 d trm1; \<And>d. P2 d assg2; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let1 assg1 trm1 assg2 trm2)"
+  and a4: "\<And>name1 name2 trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let2 name1 name2 trm1 trm2)"
+  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 strong_exhaust1)
+apply(simp_all)[5]
+apply(rule_tac y="assg" in foo.exhaust(2))
+apply(simp_all)[2]
+apply(relation "measure (sum_case (size o snd) (\<lambda>y. size (snd y)))")
+apply(simp_all add: foo.size)
+done
+
+
 end