# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1290588290 -32400
# Node ID d8a676a6904795f10000b4d055d6991a6553e4d8
# Parent  67828f23c4e95ebd5e6df3913483757b7777cb72
foo2 full exhausts

diff -r 67828f23c4e9 -r d8a676a69047 Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Wed Nov 24 16:59:26 2010 +0900
+++ b/Nominal/Ex/Foo2.thy	Wed Nov 24 17:44:50 2010 +0900
@@ -98,6 +98,20 @@
   apply simp
   by (metis assms(2) atom_eqvt fresh_perm)
 
+lemma Let2_rename3:
+  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p"
+  and "(supp ([[atom y]]lst. t2)) \<sharp>* p"
+  and "(atom x) \<sharp> p"
+  shows "Let2 x y t1 t2 = Let2 x (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)"
+  using assms
+  apply -
+  apply(drule supp_perm_eq[symmetric])
+  apply(drule supp_perm_eq[symmetric])
+  apply(simp only: foo.eq_iff)
+  apply(simp only: eqvts)
+  apply simp
+  by (metis assms(2) atom_eqvt fresh_perm)
+
 lemma strong_exhaust1:
   fixes c::"'a::fs"
   assumes "\<And>name. y = Var name \<Longrightarrow> P" 
@@ -195,6 +209,67 @@
 apply (simp add: fresh_star_def supp_atom)
 done
 
+lemma strong_exhaust2:
+  fixes c::"'a::fs"
+  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
+  and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
+  and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>assn1 trm1 assn2 trm2. 
+    \<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 (erule assms)
+  apply (erule assms)
+  apply (erule assms) apply assumption
+  apply (erule assms) apply assumption
+apply(case_tac "x1 = x2")
+apply(subgoal_tac 
+  "\<exists>q. (q \<bullet> {atom x1, atom x2}) \<sharp>* c \<and> (supp (([[atom x1, atom x2]]lst. trm1), ([[atom x2]]lst. trm2))) \<sharp>* q")
+apply(erule exE)+
+apply(erule conjE)+
+apply(perm_simp)
+apply(rule assms(5))
+apply assumption
+apply simp
+apply (rule Let2_rename)
+apply (simp only: supp_Pair)
+apply (simp only: fresh_star_Un_elim)
+apply (simp only: supp_Pair)
+apply (simp only: fresh_star_Un_elim)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply clarify
+apply (simp add: fresh_star_def)
+apply (simp add: fresh_def supp_Pair supp_Abs)
+
+  apply(subgoal_tac 
+    "\<exists>q. (q \<bullet> {atom x2}) \<sharp>* c \<and> supp (([[atom x2]]lst. trm2), ([[atom x1, atom x2]]lst. trm1), (atom x1)) \<sharp>* q")
+  apply(erule exE)+
+  apply(erule conjE)+
+  apply(rule assms(5))
+apply(perm_simp)
+apply(simp (no_asm) add: fresh_star_insert)
+apply(rule conjI)
+apply (simp add: fresh_star_def)
+apply(rotate_tac 2)
+apply(simp add: fresh_star_def)
+apply(simp)
+apply (rule Let2_rename3)
+apply (simp add: supp_Pair fresh_star_union)
+apply (simp add: supp_Pair fresh_star_union)
+apply (simp add: supp_Pair fresh_star_union)
+apply clarify
+apply (simp add: fresh_star_def supp_atom)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: fresh_star_def)
+apply (simp add: fresh_def supp_Pair supp_Abs supp_atom)
+done
 
 end