# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1285757101 14400
# Node ID c7534584a7a007719ab4963613ca3eb5cfb18150
# Parent  7f311ed9204d68ae3dbb10e2ddd94d0fb3aaf3bc
use also induct_schema for the Let-example (permute_bn is used)

diff -r 7f311ed9204d -r c7534584a7a0 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Wed Sep 29 04:42:37 2010 -0400
+++ b/Nominal/Ex/Let.thy	Wed Sep 29 06:45:01 2010 -0400
@@ -28,6 +28,7 @@
 thm trm_assn.distinct
 thm trm_assn.supp
 thm trm_assn.fresh
+thm trm_assn.exhaust
 
 
 lemma fin_bn:
@@ -60,7 +61,7 @@
 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
 
 lemma uu:
-  shows "alpha_bn (permute_bn p as) as"
+  shows "alpha_bn as (permute_bn p as)"
 apply(induct as rule: trm_assn.inducts(2))
 apply(auto)[4]
 apply(simp add: permute_bn)
@@ -78,72 +79,64 @@
 apply(simp add: atom_eqvt)
 done
 
-thm trm_assn.supp
-
-lemma "as \<sharp>* x \<longleftrightarrow> (\<forall>a\<in>as. a \<sharp> x)"
-apply(simp add: fresh_def)
-apply(simp add: fresh_star_def)
-oops
-
-inductive
-    test_trm :: "trm \<Rightarrow> bool"
-and test_assn :: "assn \<Rightarrow> bool"
-where
-  "test_trm (Var x)"
-| "\<lbrakk>test_trm t1; test_trm t2\<rbrakk> \<Longrightarrow> test_trm (App t1 t2)"
-| "\<lbrakk>test_trm t; {atom x} \<sharp>* Lam x t\<rbrakk> \<Longrightarrow> test_trm (Lam x t)"
-| "\<lbrakk>test_assn as; test_trm t; set (bn as) \<sharp>* Let as t\<rbrakk> \<Longrightarrow> test_trm (Let as t)"
-| "test_assn ANil"
-| "\<lbrakk>test_trm t; test_assn as\<rbrakk> \<Longrightarrow> test_assn (ACons x t as)"
-
-declare trm_assn.fv_bn_eqvt[eqvt]
-equivariance test_trm
-
-lemma 
-  fixes p::"perm"
-  shows "test_trm (p \<bullet> t)" and "test_assn (p \<bullet> as)"
-apply(induct t and as arbitrary: p and p rule: trm_assn.inducts)
+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"
+  shows "P"
+apply(rule_tac y="y" in trm_assn.exhaust(1))
+apply(rule assms(1))
+apply(auto)[2]
+apply(rule assms(2))
+apply(auto)[2]
+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 test_trm_test_assn.intros)
-apply(simp)
-apply(rule test_trm_test_assn.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
-apply(rule test_trm_test_assn.intros)
-apply(assumption)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
 apply(simp add: trm_assn.fresh fresh_star_def)
-apply(simp)
-defer
-apply(simp)
-apply(rule test_trm_test_assn.intros)
-apply(simp)
-apply(rule test_trm_test_assn.intros)
-apply(assumption)
-apply(assumption)
-apply(subgoal_tac "finite (set (bn (p \<bullet> assn)))")
-apply(subgoal_tac "set (bn (p \<bullet> assn)) \<sharp>* (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm))")
-apply(drule_tac c="()" in at_set_avoiding2)
-apply(simp add: supp_Unit)
-prefer 2
-apply(assumption)
-apply(simp add: finite_supp)
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* c \<and> supp ([bn assn]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
-apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" and
-               s = "Let (permute_bn pa (p \<bullet> assn)) (pa \<bullet> (p \<bullet> trm))" in subst)
-apply(rule trm_assn.eq_iff(4)[THEN iffD2])
-apply(simp add: uu)
-apply(drule supp_perm_eq)
+apply(rule assms(4))
+apply(simp add: set_eqvt)
 apply(simp add: tt)
-apply(rule test_trm_test_assn.intros(4))
-defer
-apply(subst permute_plus[symmetric])
-apply(blast)
-oops
+apply(rule refl)
+apply(simp)
+apply(simp add: trm_assn.eq_iff)
+apply(drule supp_perm_eq[symmetric])
+apply(simp)
+apply(simp add: tt uu)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: Abs_fresh_star)
+done
 
 
-(* 
+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" 
+  shows "P"
+apply(rule_tac y="as" in trm_assn.exhaust(2))
+apply(rule assms(1))
+apply(auto)[2]
+apply(rule assms(2))
+apply(auto)[2]
+done
+
+
 lemma 
   fixes t::trm
   and   as::assn
@@ -154,7 +147,26 @@
   and     a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)"
   and     a5: "\<And>c. P2 c ANil"
   and     a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)"
-  shows "P1 c t" and "P2 c as"
+  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(rule_tac as="as" in strong_exhaust2)
+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]
+done
+
+text {* *}
+
+
+(*
 proof -
   have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)" 
    and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)"