# HG changeset patch
# User urbanc
# Date 1202739557 -3600
# Node ID a7a537e0413a0868d6e584c648b37a742a9175e8
# Parent  345e495d3b92557e3ddf021754870a6ce93700d7
tuned proofs and comments

diff -r 345e495d3b92 -r a7a537e0413a src/HOL/Nominal/Examples/CR_Takahashi.thy
--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Sun Feb 10 20:49:48 2008 +0100
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Mon Feb 11 15:19:17 2008 +0100
@@ -45,13 +45,13 @@
 by (nominal_induct t avoiding: x s rule: lam.induct)
    (auto simp add: abs_fresh fresh_atm)
 
-lemma fresh_fact:
+lemma fresh_fact1:
   fixes z::"name"
   shows "z\<sharp>(t,s) \<Longrightarrow> z\<sharp>t[y::=s]"
 by (nominal_induct t avoiding: z y s rule: lam.induct)
    (auto simp add: abs_fresh fresh_prod fresh_atm)
 
-lemma fresh_fact': 
+lemma fresh_fact2: 
   fixes x::"name"
   shows "x\<sharp>s \<Longrightarrow> x\<sharp>t[x::=s]"
 by (nominal_induct t avoiding: x s rule: lam.induct)
@@ -61,7 +61,7 @@
   assumes a: "x\<noteq>y" "x\<sharp>u"
   shows "t[x::=s][y::=u] = t[y::=u][x::=s[y::=u]]"
 using a by (nominal_induct t avoiding: x y s u rule: lam.induct)
-           (auto simp add: fresh_fact forget)
+           (auto simp add: fresh_fact1 forget)
 
 lemma subst_rename: 
   assumes a: "y\<sharp>t"
@@ -100,7 +100,7 @@
 
 equivariance One
 nominal_inductive One 
-  by (simp_all add: abs_fresh fresh_fact')
+  by (simp_all add: abs_fresh fresh_fact2)
 
 lemma One_refl:
   shows "t \<longrightarrow>\<^isub>1 t"
@@ -110,7 +110,7 @@
   assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
   shows "t1[x::=s1] \<longrightarrow>\<^isub>1 t2[x::=s2]" 
 using a by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
-           (auto simp add: substitution_lemma fresh_atm fresh_fact)
+           (auto simp add: substitution_lemma fresh_atm fresh_fact1)
 
 lemma better_o4_intro:
   assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
@@ -127,27 +127,27 @@
 lemma One_Var:
   assumes a: "Var x \<longrightarrow>\<^isub>1 M"
   shows "M = Var x"
-using a by (erule_tac One.cases) (simp_all) 
+using a by (cases rule: One.cases) (simp_all) 
 
 lemma One_Lam: 
   assumes a: "Lam [x].t \<longrightarrow>\<^isub>1 s" "x\<sharp>s"
   shows "\<exists>t'. s = Lam [x].t' \<and> t \<longrightarrow>\<^isub>1 t'"
 using a
-by (cases rule: One.strong_cases[where x="x" and xa="x"])
+by (cases rule: One.strong_cases)
    (auto simp add: lam.inject abs_fresh alpha)
 
 lemma One_App: 
   assumes a: "App t s \<longrightarrow>\<^isub>1 r"
   shows "(\<exists>t' s'. r = App t' s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or> 
          (\<exists>x p p' s'. r = p'[x::=s'] \<and> t = Lam [x].p \<and> p \<longrightarrow>\<^isub>1 p' \<and> s \<longrightarrow>\<^isub>1 s' \<and> x\<sharp>(s,s'))" 
-using a by (erule_tac One.cases) (auto simp add: lam.inject)
+using a by (cases rule: One.cases) (auto simp add: lam.inject)
 
 lemma One_Redex: 
   assumes a: "App (Lam [x].t) s \<longrightarrow>\<^isub>1 r" "x\<sharp>(s,r)"
   shows "(\<exists>t' s'. r = App (Lam [x].t') s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or> 
          (\<exists>t' s'. r = t'[x::=s'] \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s')" 
 using a
-by (cases rule: One.strong_cases [where x="x" and xa="x"])
+by (cases rule: One.strong_cases)
    (auto dest: One_Lam simp add: lam.inject abs_fresh alpha fresh_prod)
 
 section {* Transitive Closure of One *}
@@ -171,7 +171,7 @@
 
 equivariance Dev
 nominal_inductive Dev 
-  by (simp_all add: abs_fresh fresh_fact')
+  by (simp_all add: abs_fresh fresh_fact2)
 
 lemma better_d4_intro:
   assumes a: "t1 \<longrightarrow>\<^isub>d t2" "s1 \<longrightarrow>\<^isub>d s2"
@@ -189,8 +189,8 @@
   fixes x::"name"
   assumes a: "M\<longrightarrow>\<^isub>d N"  
   shows "x\<sharp>M \<Longrightarrow> x\<sharp>N"
-using a 
-by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
+using a
+by (induct) (auto simp add: abs_fresh fresh_fact1 fresh_fact2)
 
 lemma Dev_Lam:
   assumes a: "Lam [x].M \<longrightarrow>\<^isub>d N" 
@@ -198,8 +198,8 @@
 proof -
   from a have "x\<sharp>Lam [x].M" by (simp add: abs_fresh)
   with a have "x\<sharp>N" by (simp add: Dev_preserves_fresh)
-  with a show ?thesis
-    by (cases rule: Dev.strong_cases [where x="x" and xa="x"])
+  with a show "\<exists>N'. N = Lam [x].N' \<and> M \<longrightarrow>\<^isub>d N'"
+    by (cases rule: Dev.strong_cases)
        (auto simp add: lam.inject abs_fresh alpha)
 qed
 
@@ -213,10 +213,8 @@
   shows "t2 \<longrightarrow>\<^isub>1 t1"
 using a 
 apply(nominal_induct avoiding: t2 rule: Dev.strong_induct)
-apply(auto dest!: One_Var)[1]
-apply(auto dest!: One_Lam)[1]
-apply(auto dest!: One_App)[1]
-apply(auto dest!: One_Redex intro: One_subst)[1]
+apply(auto dest!: One_Var One_Lam One_App)[3]
+apply(auto dest!: One_Redex intro: One_subst)
 done
 
 lemma Diamond_for_One:
@@ -245,20 +243,16 @@
   shows "Lam [x].t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam [x].t2"
 using a by (induct) (blast)+
 
-lemma Beta_App_congL: 
+lemma Beta_App_cong_aux: 
   assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" 
   shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
-using a by (induct) (blast)+
-
-lemma Beta_App_congR: 
-  assumes a: "s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* s2" 
-  shows "App t s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t s2"
+    and "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2"
 using a by (induct) (blast)+
 
 lemma Beta_App_cong: 
   assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" "s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* s2" 
   shows "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2"
-using a by (blast intro: Beta_App_congL Beta_App_congR)
+using a by (blast intro: Beta_App_cong_aux)
 
 lemmas Beta_congs = Beta_Lam_cong Beta_App_cong
 
@@ -272,17 +266,13 @@
   shows "Lam [x].t1 \<longrightarrow>\<^isub>1\<^sup>* Lam [x].t2"
 using a by (induct) (auto)
 
-lemma One_star_App_congL: 
+lemma One_star_App_cong: 
   assumes a: "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" 
-  shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s"
+  shows "App t1 s \<longrightarrow>\<^isub>1\<^sup>* App t2 s"
+  and   "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2"
 using a by (induct) (auto intro: One_refl)
 
-lemma One_star_App_congR: 
-  assumes a: "s1 \<longrightarrow>\<^isub>1\<^sup>* s2" 
-  shows "App t s1 \<longrightarrow>\<^isub>1\<^sup>* App t s2"
-using a by (induct) (auto intro: One_refl)
-
-lemmas One_congs = One_star_App_congL One_star_App_congR One_star_Lam_cong
+lemmas One_congs = One_star_App_cong One_star_Lam_cong
 
 lemma Beta_implies_One_star: 
   assumes a: "t1 \<longrightarrow>\<^isub>\<beta> t2" 
@@ -305,9 +295,9 @@
   assumes a: "t \<longrightarrow>\<^isub>\<beta>\<^sup>* t1" "t\<longrightarrow>\<^isub>\<beta>\<^sup>* t2" 
   shows "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3"
 proof -
-  from a have "t \<longrightarrow>\<^isub>1\<^sup>* t1" and "t\<longrightarrow>\<^isub>1\<^sup>* t2" by (simp_all only: Beta_star_equals_One_star)
-  then have "\<exists>t3. t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by (rule_tac CR_for_One_star) 
-  then show "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3" by (simp only: Beta_star_equals_One_star)
+  from a have "t \<longrightarrow>\<^isub>1\<^sup>* t1" and "t\<longrightarrow>\<^isub>1\<^sup>* t2" by (simp_all add: Beta_star_equals_One_star)
+  then have "\<exists>t3. t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by (simp add: CR_for_One_star) 
+  then show "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3" by (simp add: Beta_star_equals_One_star)
 qed
 
 end
diff -r 345e495d3b92 -r a7a537e0413a src/HOL/Nominal/Examples/Support.thy
--- a/src/HOL/Nominal/Examples/Support.thy	Sun Feb 10 20:49:48 2008 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy	Mon Feb 11 15:19:17 2008 +0100
@@ -9,10 +9,11 @@
 
   x\<sharp>(A \<union> B) does not imply  x\<sharp>A and  x\<sharp>B
 
-  For this we set A to the set of even atoms and B to the 
-  set of odd atoms. Then A \<union> B, that is the set of all atoms,
-  has empty support. The sets A, respectively B, however
-  have the set of all atoms as their support. 
+  with A and B being sets. For this we set A to the set of 
+  even atoms and B to the set of odd atoms. Then A \<union> B, that 
+  is the set of all atoms, has empty support. The sets A, 
+  respectively B, however have the set of all atoms as 
+  their support. 
 *}
 
 atom_decl atom
@@ -35,7 +36,9 @@
   shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)"
   by (induct n) (presburger)+
 
-text {* The union of even and odd atoms is the set of all atoms. *}
+text {* 
+  The union of even and odd atoms is the set of all atoms. 
+  Unfortunately I do not know a simpler proof of this fact. *}
 lemma EVEN_union_ODD:
   shows "EVEN \<union> ODD = UNIV"
   using even_or_odd
@@ -57,8 +60,8 @@
 
 text {* 
   The preceeding two lemmas help us to prove 
-  the following two useful equalities: 
-*}
+  the following two useful equalities: *}
+
 lemma UNIV_subtract:
   shows "UNIV - EVEN = ODD"
   and   "UNIV - ODD  = EVEN"
@@ -81,9 +84,10 @@
 qed
 
 text {* 
-  A general fact: a set S that is both infinite and coinfinite 
-  has all atoms as its support. 
-*}
+  A general fact about a set S of names that is both infinite and 
+  coinfinite. Then S has all atoms as its support. Steve Zdancewick 
+  helped with proving this fact. *}
+
 lemma supp_infinite_coinfinite:
   fixes S::"atom set"
   assumes asm1: "infinite S"
@@ -122,8 +126,8 @@
 
 text {* 
   The set of all atoms has empty support, since any swappings leaves 
-  this set unchanged. 
-*}
+  this set unchanged. *}
+
 lemma UNIV_supp:
   shows "supp (UNIV::atom set) = ({}::atom set)"
 proof -
@@ -140,4 +144,6 @@
   and   "\<not>x\<sharp>ODD"
   by (auto simp only: fresh_def EVEN_union_ODD EVEN_ODD_supp UNIV_supp)
 
+text {* Moral: support is a sublte notion. *}
+
 end
\ No newline at end of file
diff -r 345e495d3b92 -r a7a537e0413a src/HOL/Nominal/Examples/VC_Condition.thy
--- a/src/HOL/Nominal/Examples/VC_Condition.thy	Sun Feb 10 20:49:48 2008 +0100
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Mon Feb 11 15:19:17 2008 +0100
@@ -27,6 +27,7 @@
   equivalence. However as a relation 'unbind' is ok and     
   a similar relation has been used in our formalisation 
   of the algorithm W. *}
+
 inductive
   unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
 where
@@ -38,6 +39,7 @@
   We can show that Lam [x].Lam [x].Var x unbinds to [x,x],Var x 
   and also to [z,y],Var y (though the proof for the second is a 
   bit clumsy). *} 
+
 lemma unbind_lambda_lambda1: 
   shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
 by (auto intro: unbind.intros)
@@ -74,6 +76,7 @@
   To obtain a faulty lemma, we introduce the function 'bind'
   which takes a list of names and abstracts them away in 
   a given lambda-term. *}
+
 fun 
   bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
 where
@@ -83,6 +86,7 @@
 text {*
   Although not necessary for our main argument below, we can 
   easily prove that bind undoes the unbinding. *}
+
 lemma bind_unbind:
   assumes a: "t \<mapsto> xs,t'"
   shows "t = bind xs t'"
@@ -93,6 +97,7 @@
   variable in t, and x does not occur in xs, then x is a free 
   variable in bind xs t. In the nominal tradition we formulate    
   'is a free variable in' as 'is not fresh for'. *}
+
 lemma free_variable:
   fixes x::"name"
   assumes a: "\<not>(x\<sharp>t)" and b: "x\<sharp>xs"
@@ -119,8 +124,8 @@
 text {*
   Obviously this lemma is bogus. For example, in 
   case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). 
-  As a result, we can prove False. 
-*}
+  As a result, we can prove False. *}
+
 lemma false1:
   shows "False"
 proof -
@@ -147,8 +152,8 @@
 
 text {* 
   The relation is equivariant but we have to use again 
-  sorry to derive a strong induction principle. 
-*}
+  sorry to derive a strong induction principle. *}
+
 equivariance strip
 
 nominal_inductive strip
@@ -156,8 +161,8 @@
 
 text {*
   The second faulty lemma shows that a variable being fresh
-  for a term is also fresh for this term after striping. 
-*}
+  for a term is also fresh for this term after striping. *}
+
 lemma faulty2:
   fixes x::"name"
   assumes a: "t \<rightarrow> t'"
@@ -167,6 +172,7 @@
    (auto simp add: abs_fresh)
 
 text {* Obviously Lam [x].Var x is a counter example to this lemma. *}
+
 lemma false2:
   shows "False"
 proof -
@@ -176,5 +182,11 @@
   ultimately have "x\<sharp>(Var x)" by (simp only: faulty2)
   then show "False" by (simp add: fresh_atm)
 qed 
+
+text {*
+  Moral: Who would have thought that the variable convention 
+  is in general an unsound reasoning principle.
+  *}
+
  
 end
\ No newline at end of file
diff -r 345e495d3b92 -r a7a537e0413a src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Sun Feb 10 20:49:48 2008 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Mon Feb 11 15:19:17 2008 +0100
@@ -4,11 +4,15 @@
   imports "../Nominal" 
 begin
 
-section {* Weakening Property in the Simply-Typed Lambda-Calculus *}
+text {* 
+  A simple proof of the Weakening Property in the simply-typed 
+  lambda-calculus. The proof is simple, because we can make use
+  of the variable convention. *}
 
 atom_decl name 
 
 text {* Terms and Types *}
+
 nominal_datatype lam = 
     Var "name"
   | App "lam" "lam"
@@ -27,8 +31,8 @@
 
 text {* 
   Valid contexts (at the moment we have no type for finite 
-  sets yet; therefore typing-contexts are lists). 
-  *}
+  sets yet, therefore typing-contexts are lists). *}
+
 inductive
   valid :: "(name\<times>ty) list \<Rightarrow> bool"
 where
@@ -38,6 +42,7 @@
 equivariance valid
 
 text{* Typing judgements *}
+
 inductive
   typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
 where
@@ -48,13 +53,14 @@
 text {* 
   We derive the strong induction principle for the typing 
   relation (this induction principle has the variable convention 
-  already built-in). 
-  *}
+  already built-in). *}
+
 equivariance typing
 nominal_inductive typing
   by (simp_all add: abs_fresh ty_fresh)
 
 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
@@ -62,10 +68,10 @@
 
 text {* Now it comes: The Weakening Lemma *}
 
-text {* 
+text {*
   The first version is, after setting up the induction, 
-  completely automatic except for use of atomize. 
-  *}
+  completely automatic except for use of atomize. *}
+
 lemma weakening_version1: 
   fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T" 
@@ -77,9 +83,9 @@
    (auto | atomize)+
 
 text {* 
-  The second version gives all details for the variable
-  and lambda case. 
-  *}
+  The second version gives the details for the variable
+  and lambda case. *}
+
 lemma weakening_version2: 
   fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   and   t ::"lam"
@@ -113,8 +119,8 @@
 text{* 
   The original induction principle for the typing relation
   is not strong enough - even this simple lemma fails to be 
-  simple ;o) 
-  *}
+  simple ;o) *}
+
 lemma weakening_not_straigh_forward: 
   fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T"
@@ -143,7 +149,11 @@
   have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *) 
     oops
   
-text{* The complete proof without using the variable convention. *}
+text{* 
+  To show that the proof is not simple, here proof without using 
+  the variable convention. 
+
+*}
 
 lemma weakening_with_explicit_renaming: 
   fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
@@ -190,9 +200,8 @@
 qed (auto)
 
 text {*
-  Moral: compare the proof with explicit renamings to version1 and version2,
-  and imagine you are proving something more substantial than the weakening 
-  lemma. 
-  *}
+  Moral: compare the proof with explicit renamings to weakening_version1 
+  and weakening_version2, and imagine you are proving something more substantial 
+  than the weakening lemma. *}
 
 end
\ No newline at end of file