# HG changeset patch
# User urbanc
# Date 1133063960 -3600
# Node ID 7f75925498da6a0d5794f8118a74a82ab6bba21c
# Parent  d0fcd4d684f5d9cf541592e719af7b082998d6f1
cleaned up all examples so that they work with the
current nominal-setting.

diff -r d0fcd4d684f5 -r 7f75925498da src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Sun Nov 27 03:55:16 2005 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Sun Nov 27 04:59:20 2005 +0100
@@ -1,5 +1,5 @@
 theory fsub
-imports nominal 
+imports "../nominal" 
 begin
 
 atom_decl tyvrs vrs
diff -r d0fcd4d684f5 -r 7f75925498da src/HOL/Nominal/Examples/Lam_substs.thy
--- a/src/HOL/Nominal/Examples/Lam_substs.thy	Sun Nov 27 03:55:16 2005 +0100
+++ b/src/HOL/Nominal/Examples/Lam_substs.thy	Sun Nov 27 04:59:20 2005 +0100
@@ -1433,10 +1433,10 @@
 
 
 consts
-  "dom_sss" :: "(name\<times>lam) list \<Rightarrow> (name list)"
+  "domain" :: "(name\<times>lam) list \<Rightarrow> (name list)"
 primrec
-  "dom_sss []    = []"
-  "dom_sss (x#\<theta>) = (fst x)#(dom_sss \<theta>)" 
+  "domain []    = []"
+  "domain (x#\<theta>) = (fst x)#(domain \<theta>)" 
 
 consts
   "apply_sss"  :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam" (" _ < _ >" [80,80] 80)
@@ -1446,15 +1446,15 @@
 
 lemma apply_sss_eqvt[rule_format]:
   fixes pi::"name prm"
-  shows "a\<in>set (dom_sss \<theta>) \<longrightarrow> pi\<bullet>(\<theta><a>) = (pi\<bullet>\<theta>)<pi\<bullet>a>"
+  shows "a\<in>set (domain \<theta>) \<longrightarrow> pi\<bullet>(\<theta><a>) = (pi\<bullet>\<theta>)<pi\<bullet>a>"
 apply(induct_tac \<theta>)
 apply(auto)
 apply(simp add: pt_bij[OF pt_name_inst, OF at_name_inst])
 done
 
-lemma dom_sss_eqvt[rule_format]:
+lemma domain_eqvt[rule_format]:
   fixes pi::"name prm"
-  shows "((pi\<bullet>a)\<in>set (dom_sss \<theta>)) =  (a\<in>set (dom_sss ((rev pi)\<bullet>\<theta>)))"
+  shows "((pi\<bullet>a)\<in>set (domain \<theta>)) =  (a\<in>set (domain ((rev pi)\<bullet>\<theta>)))"
 apply(induct_tac \<theta>)
 apply(auto)
 apply(simp_all add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
@@ -1463,7 +1463,7 @@
 
 constdefs 
   psubst_Var :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam"
-  "psubst_Var \<theta> \<equiv> \<lambda>a. (if a\<in>set (dom_sss \<theta>) then \<theta><a> else (Var a))"
+  "psubst_Var \<theta> \<equiv> \<lambda>a. (if a\<in>set (domain \<theta>) then \<theta><a> else (Var a))"
   
   psubst_App :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
   "psubst_App \<theta> \<equiv> \<lambda>r1 r2. App r1 r2"
@@ -1476,7 +1476,7 @@
 
 lemma supports_psubst_Var:
   shows "((supp \<theta>)::name set) supports (psubst_Var \<theta>)"
-  by (supports_simp add: psubst_Var_def apply_sss_eqvt dom_sss_eqvt)
+  by (supports_simp add: psubst_Var_def apply_sss_eqvt domain_eqvt)
 
 lemma supports_psubst_App:
   shows "((supp \<theta>)::name set) supports psubst_App \<theta>"
@@ -1516,7 +1516,7 @@
 done
 
 lemma psubst_Var:
-  shows "psubst_lam \<theta> (Var a) = (if a\<in>set (dom_sss \<theta>) then \<theta><a> else (Var a))"
+  shows "psubst_lam \<theta> (Var a) = (if a\<in>set (domain \<theta>) then \<theta><a> else (Var a))"
 apply(simp add: psubst_lam_def)
 apply(auto simp add: rfun_Var[OF fin_supp_psubst, OF fresh_psubst_Lam])
 apply(auto simp add: psubst_Var_def)
diff -r d0fcd4d684f5 -r 7f75925498da src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Sun Nov 27 03:55:16 2005 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Sun Nov 27 04:59:20 2005 +0100
@@ -1,3 +1,4 @@
+(* $Id$ *)
 
 theory sn
 imports lam_substs  Accessible_Part
@@ -790,7 +791,7 @@
 apply(blast)
 done
 
-lemma abs_RED[rule_format]: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
+lemma abs_RED: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
 apply(simp)
 apply(clarify)
 apply(subgoal_tac "t\<in>termi Beta")(*1*)
@@ -873,13 +874,38 @@
 apply(force simp add: RED_props)
 done
 
+lemma fresh_domain[rule_format]: "a\<sharp>\<theta>\<longrightarrow>a\<notin>set(domain \<theta>)"
+apply(induct_tac \<theta>)
+apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
+done
+
+lemma fresh_at[rule_format]: "a\<in>set(domain \<theta>) \<longrightarrow> c\<sharp>\<theta>\<longrightarrow>c\<sharp>(\<theta><a>)"
+apply(induct_tac \<theta>)   
+apply(auto simp add: fresh_prod fresh_list_cons)
+done
+
+lemma psubs_subs[rule_format]: "c\<sharp>\<theta>\<longrightarrow> (t[<\<theta>>])[c::=s] = t[<((c,s)#\<theta>)>]"
+apply(nominal_induct t rule: lam_induct)
+apply(auto dest: fresh_domain)
+apply(drule fresh_at)
+apply(assumption)
+apply(rule forget)
+apply(assumption)
+apply(subgoal_tac "ab\<sharp>((aa,b)#a)")(*A*)
+apply(simp add: fresh_prod)
+(*A*)
+apply(simp add: fresh_list_cons fresh_prod)
+done
+
 lemma all_RED: 
- "((\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(dom_sss \<theta>)\<and>\<theta><a>\<in>RED \<sigma>))\<and>\<Gamma>\<turnstile>t:\<tau>) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)"
+  "\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow>  (t[<\<theta>>]\<in>RED \<tau>)"
 apply(nominal_induct t rule: lam_induct)
 (* Variables *)
 apply(force dest: t1_elim)
 (* Applications *)
-apply(auto dest!: t2_elim)
+apply(clarify)
+apply(drule t2_elim)
+apply(erule exE, erule conjE)
 apply(drule_tac x="a" in spec)
 apply(drule_tac x="a" in spec)
 apply(drule_tac x="\<tau>\<rightarrow>aa" in spec)
@@ -888,14 +914,135 @@
 apply(drule_tac x="b" in spec)
 apply(force)
 (* Abstractions *)
+apply(clarify)
 apply(drule t3_elim)
 apply(simp add: fresh_prod)
-apply(auto)
-apply(drule_tac x="((ab,\<tau>)#a)" in spec)
+apply(erule exE)+
+apply(erule conjE)
+apply(simp only: fresh_prod psubst_Lam)
+apply(rule abs_RED[THEN mp])
+apply(clarify)
+apply(drule_tac x="(ab,\<tau>)#a" in spec)
 apply(drule_tac x="\<tau>'" in spec)
-apply(drule_tac x="b" in spec)
+apply(drule_tac x="(ab,s)#b" in spec)
+apply(simp (no_asm_use))
+apply(simp add: split_if)
+apply(auto)
+apply(drule fresh_context)
+apply(simp)
+apply(simp add: psubs_subs)
+done
+
+lemma all_RED: 
+ "\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow>  (t[<\<theta>>]\<in>RED \<tau>)"
+apply(nominal_induct t rule: lam_induct)
+(* Variables *)
+apply(force dest: t1_elim)
+(* Applications *)
+apply(force dest!: t2_elim)
+(* Abstractions *)
+apply(auto dest!: t3_elim simp only:)
+apply(simp add: fresh_prod)
+apply(simp only: fresh_prod psubst_Lam)
+apply(rule abs_RED[THEN mp])
+apply(force dest: fresh_context simp add: psubs_subs)
+done
+
+lemma all_RED: 
+ "\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow>  (t[<\<theta>>]\<in>RED \<tau>)"
+proof(nominal_induct t rule: lam_induct)
+  case Var 
+  show ?case by (force dest: t1_elim)
+next
+  case App
+  thus ?case by (force dest!: t2_elim)
+(* HERE *)
+next
+  case (Lam \<Gamma> \<tau> \<theta> a t)
+  have ih: 
+    "\<forall>\<Gamma> \<tau> \<theta>. (\<forall>\<sigma> c. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>) \<and> \<Gamma> \<turnstile> t : \<tau> \<longrightarrow> t[<\<theta>>]\<in>RED \<tau>"
+    by fact
+  have "a\<sharp>(\<Gamma>,\<tau>,\<theta>)" by fact
+  hence b1: "a\<sharp>\<Gamma>" and b2: "a\<sharp>\<tau>" and b3: "a\<sharp>\<theta>" by (simp_all add: fresh_prod)
+  from b1 have c1: "\<not>(\<exists>\<tau>. (a,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context) 
+  show ?case using b1 
+  proof (auto dest!: t3_elim simp only: psubst_Lam)
+    fix \<sigma>1::"ty" and \<sigma>2::"ty"
+    assume a1: "((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2"
+    and    a3: "\<forall>(\<sigma>\<Colon>ty) (c\<Colon>name). (c,\<sigma>) \<in> set \<Gamma> \<longrightarrow> c \<in> set (domain \<theta>) \<and>  \<theta> <c> \<in> RED \<sigma>"
+    have "\<forall>s\<in>RED \<sigma>1. (t[<\<theta>>])[a::=s]\<in>RED \<sigma>2" 
+    proof
+(* HERE *)
+
+      fix s::"lam"
+      assume a4: "s \<in> RED \<sigma>1"
+      from ih have "\<forall>\<sigma> c. (c,\<sigma>)\<in>set ((a,\<sigma>1)#\<Gamma>) \<longrightarrow> c\<in>set (domain ((c,s)#\<theta>)) \<and> (((c,s)#\<theta>)<c>)\<in>RED \<sigma>"
+	using c1 a4 proof (auto)
 apply(simp)
-(* HERE *)
+	apply(rule allI)+
+	apply(rule conjI)
+
+      proof (auto) *)
+      have "(((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2) \<longrightarrow> t[<((a,s)#\<theta>)>] \<in> RED \<sigma>2" using Lam a3 b3 
+	proof(blast dest: fresh_context)
+
+      show "(t[<\<theta>>])[a::=s] \<in> RED \<sigma>2"
+	
+    qed
+    thus "Lam [a].(t[<\<theta>>]) \<in> RED (\<sigma>1\<rightarrow>\<sigma>2)" by (simp only: abs_RED)
+  qed
+qed
+
+
+
+
+
+    have "(((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2) \<longrightarrow> t[<((a,u)#\<theta>)>] \<in> RED \<sigma>2" using Lam a3 sorry
+    hence "t[<((a,u)#\<theta>)>] \<in> RED \<sigma>2" using a1 by simp
+    hence "t[<\<theta>>][a::=u] \<in> RED \<sigma>2" using b3 by (simp add: psubs_subs)
+    show "Lam [a].(t[<\<theta>>]) \<in> RED (\<sigma>1\<rightarrow>\<sigma>2)" 
+    hence "Lam [a].(t[<\<theta>>]) \<in> RED (\<tau>\<rightarrow>\<sigma>)" using a2 abs_RED by force
+    show "App (Lam [a].(t[<\<theta>>])) u \<in> RED \<sigma>2"
+
+    
+
+  thus ?case using t2_elim 
+    proof(auto, blast)
+
+qed
+
+(* Variables *)
+apply(force dest: t1_elim)
+(* Applications *)
+apply(clarify)
+apply(drule t2_elim)
+apply(erule exE, erule conjE)
+apply(drule_tac x="a" in spec)
+apply(drule_tac x="a" in spec)
+apply(drule_tac x="\<tau>\<rightarrow>aa" in spec)
+apply(drule_tac x="\<tau>" in spec)
+apply(drule_tac x="b" in spec)
+apply(drule_tac x="b" in spec)
+apply(force)
+(* Abstractions *)
+apply(clarify)
+apply(drule t3_elim)
+apply(simp add: fresh_prod)
+apply(erule exE)+
+apply(erule conjE)
+apply(simp only: fresh_prod psubst_Lam)
+apply(rule abs_RED)
+apply(auto)
+apply(drule_tac x="(ab,\<tau>)#a" in spec)
+apply(drule_tac x="\<tau>'" in spec)
+apply(drule_tac x="(ab,s)#b" in spec)
+apply(simp)
+apply(auto)
+apply(drule fresh_context)
+apply(simp)
+apply(simp add: psubs_subs)
+done
+
 
 
 done