# HG changeset patch
# User urbanc
# Date 1192986293 -7200
# Node ID 0835ac64834a93556d7189c7d545fedc2e33a21d
# Parent  3cfa2a60837fca6635d016a7e54d4ea6c746988b
polished the proofs and added a version of the weakening lemma that does not use the variable convention

diff -r 3cfa2a60837f -r 0835ac64834a src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Sun Oct 21 17:48:11 2007 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Sun Oct 21 19:04:53 2007 +0200
@@ -9,57 +9,64 @@
 
 atom_decl name 
 
+text {* Terms and types *}
 nominal_datatype lam = 
     Var "name"
   | App "lam" "lam"
   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
 nominal_datatype ty =
-    TVar "nat"
-  | TArr "ty" "ty" (infix "\<rightarrow>" 200)
+    TVar "string"
+  | TArr "ty" "ty" ("_ \<rightarrow> _" [100,100] 100)
 
 lemma ty_fresh:
   fixes x::"name"
   and   T::"ty"
   shows "x\<sharp>T"
 by (nominal_induct T rule: ty.induct)
-   (auto simp add: fresh_nat)
+   (auto simp add: fresh_string)
 
-text {* valid contexts *}
-
+text {* 
+  Valid contexts (at the moment we have no type for finite 
+  sets yet; therefore typing-contexts are lists). *}
 inductive
   valid :: "(name\<times>ty) list \<Rightarrow> bool"
 where
     v1[intro]: "valid []"
-  | v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
+  | v2[intro]: "\<lbrakk>valid \<Gamma>;x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,T)#\<Gamma>)"
 
 equivariance valid
 
-text{* typing judgements *}
+text{* Typing judgements *}
 inductive
   typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
 where
     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
-  | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,T1)#\<Gamma>) \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2"
+  | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2"
 
+text {* 
+  We automatically derive the strong induction principle 
+  for the typing relation (this induction principle has the 
+  variable convention already built in). *}
 equivariance typing
-
-(* automatically deriving the strong induction principle *)
 nominal_inductive typing
   by (simp_all add: abs_fresh ty_fresh)
 
-text {* definition of a subcontext *}
-
+text {* Abbreviation for the notion of subcontexts. *}
 abbreviation
   "sub_context" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 
 where
   "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2"
 
 text {* Now it comes: The Weakening Lemma *}
+(*========================================*)
 
+text {* 
+  The first version is, after setting up the induction, 
+  quite automatic except for use of atomize. *}
 lemma weakening_version1: 
-  fixes \<Gamma>1 \<Gamma>2 :: "(name\<times>ty) list"
+  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T" 
   and     b: "valid \<Gamma>2" 
   and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
@@ -68,8 +75,11 @@
 by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
    (auto | atomize)+
 
+text {* 
+  The second version gives all details for the variable
+  and lambda case. *}
 lemma weakening_version2: 
-  fixes \<Gamma>1::"(name\<times>ty) list"
+  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   and   t ::"lam"
   and   \<tau> ::"ty"
   assumes a: "\<Gamma>1 \<turnstile> t : T"
@@ -88,7 +98,7 @@
 next
   case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
   have vc: "x\<sharp>\<Gamma>2" by fact   (* variable convention *)
-  have ih: "\<lbrakk>valid ((x,T1)#\<Gamma>2); (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2\<rbrakk> \<Longrightarrow>  (x,T1)#\<Gamma>2 \<turnstile> t:T2" by fact
+  have ih: "\<lbrakk>valid ((x,T1)#\<Gamma>2); (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2\<rbrakk> \<Longrightarrow> (x,T1)#\<Gamma>2 \<turnstile> t:T2" by fact
   have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
   then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp
   moreover
@@ -98,38 +108,19 @@
   with vc show "\<Gamma>2 \<turnstile> Lam [x].t : T1\<rightarrow>T2" by auto
 qed (auto) (* app case *)
 
-lemma weakening_version3:
-  fixes \<Gamma>1 \<Gamma>2 :: "(name\<times>ty) list"
-  assumes a: "\<Gamma>1 \<turnstile> t : T"
-  and     b: "valid \<Gamma>2" 
-  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
-  shows "\<Gamma>2 \<turnstile> t : T"
-using a b c
-proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
-  case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
-  have vc: "x\<sharp>\<Gamma>2" by fact (* variable convention *)
-  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow>  \<Gamma>3 \<turnstile> t : T2" by fact
-  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
-  then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp
-  moreover
-  have "valid \<Gamma>2" by fact
-  then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2)
-  ultimately have "(x,T1)#\<Gamma>2 \<turnstile> t : T2" using ih by simp
-  with vc show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by auto
-qed (auto) (* app and var case *)
-
-text{* The original induction principle for the typing relation
-       is not strong enough - even this simple lemma fails to be simple ;o) *}
-
-lemma weakening_too_weak: 
-  fixes \<Gamma>1 \<Gamma>2 :: "(name\<times>ty) list"
+text{* 
+  The original induction principle for the typing relation
+  is not strong enough - even this simple lemma fails to be 
+  simple ;o) *}
+lemma weakening_not_straigh_forward: 
+  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T"
   and     b: "valid \<Gamma>2" 
   and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
   shows "\<Gamma>2 \<turnstile> t : T"
 using a b c
 proof (induct arbitrary: \<Gamma>2)
-  case (t_Var \<Gamma>1 x T) (* variable case works *)
+  case (t_Var \<Gamma>1 x T) (* variable case still works *)
   have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
   moreover
   have "valid \<Gamma>2" by fact
@@ -138,15 +129,61 @@
   ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto
 next
   case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
-  (* all assumptions available in this case*)
+  (* These are all assumptions available in this case*)
   have a0: "x\<sharp>\<Gamma>1" by fact
   have a1: "(x,T1)#\<Gamma>1 \<turnstile> t : T2" by fact
   have a2: "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
   have a3: "valid \<Gamma>2" by fact
-  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk>  \<Longrightarrow>  \<Gamma>3 \<turnstile> t : T2" by fact
+  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact
   have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" using a2 by simp
   moreover
   have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *) 
     oops
+  
+text{* 
+  The complete proof without using the variable convention. *}
+lemma weakening_with_explicit_renaming: 
+  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
+  assumes a: "\<Gamma>1 \<turnstile> t : T"
+  and     b: "valid \<Gamma>2" 
+  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
+  shows "\<Gamma>2 \<turnstile> t : T"
+using a b c
+proof (induct arbitrary: \<Gamma>2)
+  case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
+  have fc0: "x\<sharp>\<Gamma>1" by fact
+  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact
+  obtain c::"name" where fc1: "c\<sharp>(x,t,\<Gamma>1,\<Gamma>2)"  (* we obtain a fresh name *)
+    by (rule exists_fresh) (auto simp add: fs_name1)
+  have "Lam [c].([(c,x)]\<bullet>t) = Lam [x].t" using fc1 (* we alpha-rename the lambda-abstraction *)
+    by (auto simp add: lam.inject alpha fresh_prod fresh_atm)
+  moreover
+  have "\<Gamma>2 \<turnstile> Lam [c].([(c,x)]\<bullet>t) : T1 \<rightarrow> T2" (* we can then alpha-rename our original goal *)
+  proof - 
+    (* we establish (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2) and valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2)) *)
+    have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2)" 
+    proof -
+      have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
+      then have "[(c,x)]\<bullet>((x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2))" using fc0 fc1 
+	by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
+      then show "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2)" by (rule perm_boolE)
+    qed
+    moreover 
+    have "valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2))" 
+    proof -
+      have "valid \<Gamma>2" by fact
+      then show "valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2))" using fc1
+	by (auto intro!: v2 simp add: fresh_left calc_atm eqvts)
+    qed
+    (* these two facts give us by induction hypothesis the following *)
+    ultimately have "(x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2" using ih by simp 
+    (* we now apply renamings to get our goal *)
+    then have "[(c,x)]\<bullet>((x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2)" by (rule perm_boolI)
+    then have "(c,T1)#\<Gamma>2 \<turnstile> ([(c,x)]\<bullet>t) : T2" using fc1 
+      by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
+    then show "\<Gamma>2 \<turnstile> Lam [c].([(c,x)]\<bullet>t) : T1 \<rightarrow> T2" using fc1 by auto
+  qed
+  ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp
+qed (auto)
 
 end
\ No newline at end of file