--- a/Nominal/Ex/Let.thy	Mon Sep 27 04:10:36 2010 -0400
+++ b/Nominal/Ex/Let.thy	Mon Sep 27 04:56:28 2010 -0400
@@ -2,41 +2,231 @@
 imports "../Nominal2" 
 begin
 
-text {* example 3 or example 5 from Terms.thy *}
-
 atom_decl name
 
-declare [[STEPS = 29]]
-
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind  x in t
-| Let a::"lts" t::"trm"   bind "bn a" in t
-and lts =
-  Lnil
-| Lcons "name" "trm" "lts"
+| Let as::"assn" t::"trm"   bind "bn as" in t
+and assn =
+  ANil
+| ACons "name" "trm" "assn"
 binder
   bn
 where
-  "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
+  "bn ANil = []"
+| "bn (ACons x t as) = (atom x) # (bn as)"
+
+thm trm_assn.fv_defs
+thm trm_assn.eq_iff trm_assn.bn_defs
+thm trm_assn.bn_defs
+thm trm_assn.perm_simps
+thm trm_assn.induct[no_vars]
+thm trm_assn.inducts[no_vars]
+thm trm_assn.distinct
+thm trm_assn.supp
+thm trm_assn.fv_defs[simplified trm_assn.supp(1-2)]
+
+
+
+lemma fv_supp:
+  shows "fv_trm = supp"
+  and   "fv_assn = supp"
+apply(rule ext)
+apply(rule trm_assn.supp)
+apply(rule ext)
+apply(rule trm_assn.supp)
+done
+
+lemmas eq_iffs = trm_assn.eq_iff[folded fv_supp[symmetric], folded Abs_eq_iff]
+
+lemmas supps = trm_assn.fv_defs[simplified trm_assn.supp(1-2)]
+
+lemma supp_fresh_eq:
+  assumes "supp x = supp y"
+  shows "a \<sharp> x \<longleftrightarrow> a \<sharp> y"
+using assms
+by (simp add: fresh_def)
+
+lemma supp_not_in:
+  assumes "x = y"
+  shows "a \<notin> x \<longleftrightarrow> a \<notin> y"
+using assms
+by (simp add: fresh_def)
+
+lemmas freshs =
+  supps(1)[THEN supp_not_in, folded fresh_def]
+  supps(2)[THEN supp_not_in, simplified, folded fresh_def]
+  supps(3)[THEN supp_not_in, folded fresh_def]
+  supps(4)[THEN supp_not_in, folded fresh_def]
+  supps(5)[THEN supp_not_in, simplified, folded fresh_def]
+  supps(6)[THEN supp_not_in, simplified, folded fresh_def]
+
+lemma fin_bn:
+  shows "finite (set (bn l))"
+  apply(induct l rule: trm_assn.inducts(2))
+  apply(simp_all)
+  done
+
+
+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)
+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(simp add: freshs 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(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
+apply(rule eq_iffs(4)[THEN iffD2])
+defer
+apply(rule test_trm_test_assn.intros)
+prefer 3
+thm freshs
+--"HERE"
+
+thm supps
+apply(rule test_trm_test_assn.intros)
+apply(assumption)
+
+apply(assumption)
+
+
+
+lemma 
+  fixes t::trm
+  and   as::assn
+  and   c::"'a::fs"
+  assumes a1: "\<And>x c. P1 c (Var x)"
+  and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"
+  and     a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"
+  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"
+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)"
+    apply(induct rule: trm_assn.inducts)
+    apply(simp)
+    apply(rule a1)
+    apply(simp)
+    apply(rule a2)
+    apply(assumption)
+    apply(assumption)
+    -- "lam case"
+    apply(simp)
+    apply(subgoal_tac "\<exists>q. (q \<bullet> {atom (p \<bullet> name)}) \<sharp>* c \<and> supp (Lam (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
+    apply(erule exE)
+    apply(erule conjE)
+    apply(drule supp_perm_eq[symmetric])
+    apply(simp)
+    apply(thin_tac "?X = ?Y")
+    apply(rule a3)
+    apply(simp add: atom_eqvt permute_set_eq)
+    apply(simp only: permute_plus[symmetric])
+    apply(rule at_set_avoiding2)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: freshs fresh_star_def)
+    --"let case"
+    apply(simp)
+    thm trm_assn.eq_iff
+    thm eq_iffs
+    apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> assn))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm)) \<sharp>* q")
+    apply(erule exE)
+    apply(erule conjE)
+    prefer 2
+    apply(rule at_set_avoiding2)
+    apply(rule fin_bn)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: abs_fresh)
+    apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
+    prefer 2
+    apply(rule a4)
+    prefer 4
+    apply(simp add: eq_iffs)
+    apply(rule conjI)
+    prefer 2
+    apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    prefer 2
+    apply(simp add: eq_iffs)
+    thm eq_iffs
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(simp add: supps)
+    apply(simp add: fresh_star_def freshs)
+    apply(drule supp_perm_eq[symmetric])
+    apply(simp)
+    apply(simp add: eq_iffs)
+    apply(simp)
+    apply(thin_tac "?X = ?Y")
+    apply(rule a4) 
+    apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(simp add: supps)
+    thm at_set_avoiding2
+    --"HERE"
+    apply(rule at_set_avoiding2)
+    apply(rule fin_bn)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: fresh_star_def freshs)
+    apply(rule ballI)
+    apply(simp add: eqvts permute_bn)
+    apply(rule a5)
+    apply(simp add: permute_bn)
+    apply(rule a6)
+    apply simp
+    apply simp
+    done
+  then have a: "P1 c (0 \<bullet> t)" by blast
+  have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
+  then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
+qed
+*)
 
 text {* *}
 
 (*
 
-thm trm_lts.fv
-thm trm_lts.eq_iff
-thm trm_lts.bn
-thm trm_lts.perm
-thm trm_lts.induct[no_vars]
-thm trm_lts.inducts[no_vars]
-thm trm_lts.distinct
-thm trm_lts.supp
-thm trm_lts.fv[simplified trm_lts.supp(1-2)]
-
-
 primrec
   permute_bn_raw
 where

--- a/Nominal/Ex/SingleLet.thy	Mon Sep 27 04:10:36 2010 -0400
+++ b/Nominal/Ex/SingleLet.thy	Mon Sep 27 04:56:28 2010 -0400
@@ -37,7 +37,8 @@
 thm single_let.supp
 thm single_let.size
 
-
+thm single_let.supp(1-2)
+thm single_let.fv_defs[simplified single_let.supp(1-2)]
 
 
 end