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.
first attempt of strong induction for lets with assignments
authorChristian Urban <urbanc@in.tum.de>
Thu, 25 Mar 2010 08:05:03 +0100
changeset 1638 36798cdbc452
parent 1637 a5501c9fad9b
child 1639 a98d03fb9d53
first attempt of strong induction for lets with assignments
Nominal/ExLet.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/ExLet.thy	Thu Mar 25 07:21:41 2010 +0100
+++ b/Nominal/ExLet.thy	Thu Mar 25 08:05:03 2010 +0100
@@ -25,10 +25,82 @@
 thm trm_lts.eq_iff
 thm trm_lts.bn
 thm trm_lts.perm
-thm trm_lts.induct
+thm trm_lts.induct[no_vars]
+thm trm_lts.inducts[no_vars]
 thm trm_lts.distinct
 thm trm_lts.fv[simplified trm_lts.supp]
 
+lemma 
+  fixes t::trm
+  and   l::lts
+  and   c::"'a::fs"
+  assumes a1: "\<And>name c. P1 c (Vr name)" 
+  and     a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
+  and     a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" 
+  and     a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
+  and     a5: "\<And>c. P2 c Lnil"
+  and     a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
+  shows "P1 c t" and "P2 c l"
+proof -
+  have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
+       "(\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> l))"
+    apply(induct rule: trm_lts.inducts)
+    apply(simp)
+    apply(rule a1)
+    apply(simp)
+    apply(rule a2)
+    apply(simp)
+    apply(simp)
+    apply(simp)
+    apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
+    apply(erule exE)
+    apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)" 
+               and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst)
+    apply(rule supp_perm_eq)
+    apply(simp)
+    apply(simp)
+    apply(rule a3)
+    apply(simp add: atom_eqvt)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(rule at_set_avoiding2_atom)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: fresh_def)
+    apply(simp add: trm_lts.fv[simplified trm_lts.supp])
+    apply(simp)
+    apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Lt (p \<bullet> lts) (p \<bullet> trm)) \<sharp>* q")
+    apply(erule exE)
+    apply(rule_tac t="Lt (p \<bullet> lts) (p \<bullet> trm)" 
+               and s="q \<bullet> Lt (p \<bullet> lts) (p \<bullet> trm)" in subst)
+    apply(rule supp_perm_eq)
+    apply(simp)
+    apply(simp)
+    apply(rule a4)
+    apply(simp add: eqvts)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(rule at_set_avoiding2)
+    apply(simp add: finite_supp)
+    defer
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: fresh_star_def)
+    apply(simp add: fresh_def)
+    apply(simp add: trm_lts.fv[simplified trm_lts.supp])
+    defer
+    apply(simp)
+    apply(rule a5)
+    apply(simp)
+    apply(rule a6)
+    apply(simp)
+    apply(simp)
+    oops
+    
+
+
 lemma lets_bla:
   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
   by (simp add: trm_lts.eq_iff)
nominal2