# HG changeset patch # User Christian Urban # Date 1290768835 0 # Node ID cb16f22bc660ad007065a4f9cda217650e9a40d6 # Parent 6c4372a1f2204be90135bfd2bcce98bb256a3b4f# Parent dc988b07755ef2e5496273b04fce5fd8264818ad merged diff -r 6c4372a1f220 -r cb16f22bc660 Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Thu Nov 25 01:18:24 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Fri Nov 26 10:53:55 2010 +0000 @@ -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 "\name. y = Var name \ P" and "\trm1 trm2. y = App trm1 trm2 \ 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 "\name. y = Var name \ P" and "\trm1 trm2. y = App trm1 trm2 \ P" @@ -218,7 +218,7 @@ \((set (bn assn1)) \ (set (bn assn2))) \* c; y = Let1 assn1 trm1 assn2 trm2\ \ P" and "\x1 x2 trm1 trm2. \{atom x1, atom x2} \* c; y = Let2 x1 x2 trm1 trm2\ \ 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: "\name c. P1 c (Var name)" + and a1: "\trm1 trm2 c. \\d. P1 d trm1; \d. P1 d trm2\ \ P1 c (App trm1 trm2)" + and a2: "\name trm c. (\d. P1 d trm) \ P1 c (Lam name trm)" + and a3: "\assg1 trm1 assg2 trm2 c. \((set (bn assg1)) \ (set (bn assg2))) \* c; \d. P2 c assg1; \d. P1 d trm1; \d. P2 d assg2; \d. P1 d trm2\ \ P1 c (Let1 assg1 trm1 assg2 trm2)" + and a4: "\name1 name2 trm1 trm2 c. \{atom name1, atom name2} \* c; \d. P1 d trm1; \d. P1 d trm2\ \ P1 c (Let2 name1 name2 trm1 trm2)" + and a5: "\c. P2 c As_Nil" + and a6: "\name1 name2 trm assg c. \\d. P1 d trm; \d. P2 d assg\ \ 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) (\y. size (snd y)))") +apply(simp_all add: foo.size) +done + + end