# HG changeset patch
# User urbanc
# Date 1191813827 -7200
# Node ID 7cbb842aa99eecd6642e0a81065079dba6e778e3
# Parent  163c82d039cfdd3b262e0530eaabed3c5292a8d6
added two new example files

diff -r 163c82d039cf -r 7cbb842aa99e src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Sun Oct 07 21:29:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Mon Oct 08 05:23:47 2007 +0200
@@ -18,4 +18,7 @@
   "Crary",
   "SOS",
   "LocalWeakening"
+  "Support"
 ];
+
+setmp quick_and_dirty true use_thy "VC-Compatible";
\ No newline at end of file
diff -r 163c82d039cf -r 7cbb842aa99e src/HOL/Nominal/Examples/Support.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/Support.thy	Mon Oct 08 05:23:47 2007 +0200
@@ -0,0 +1,124 @@
+(* $Id$ *)
+
+theory Support 
+imports "../Nominal" 
+begin
+
+text {* 
+  
+  An example showing that in general
+
+  x\<sharp>(A \<union> B) does not imply  x\<sharp>A and  x\<sharp>B
+
+  The example shows that with A set to the set of 
+  even atoms and B to the set of odd even atoms. 
+  Then A \<union> B, that is the set of all atoms, has 
+  empty support. The sets A, respectively B, have 
+  the set of all atoms as support. 
+
+*}
+
+atom_decl atom
+
+abbreviation
+  EVEN :: "atom set"
+where
+  "EVEN \<equiv> {atom n | n. \<exists>i. n=2*i}"
+
+abbreviation  
+  ODD :: "atom set"
+where
+  "ODD \<equiv> {atom n | n. \<exists>i. n=2*i+1}"
+
+lemma even_or_odd:
+  fixes n::"nat"
+  shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)"
+  by (induct n) (presburger)+
+
+lemma EVEN_union_ODD:
+  shows "EVEN \<union> ODD = UNIV"
+proof -
+  have "EVEN \<union> ODD = (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i} \<union> (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i+1}" by auto
+  also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i} \<union> {n. \<exists>i. n = 2*i+1})" by auto
+  also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i \<or> n = 2*i+1})" by auto
+  also have "\<dots> = (\<lambda>n. atom n) ` (UNIV::nat set)" using even_or_odd by auto
+  also have "\<dots> = (UNIV::atom set)" using atom.exhaust
+    by (rule_tac  surj_range) (auto simp add: surj_def)
+  finally show "EVEN \<union> ODD = UNIV" by simp
+qed
+
+lemma EVEN_intersect_ODD:
+  shows "EVEN \<inter> ODD = {}"
+  using even_or_odd
+  by (auto) (presburger)
+
+lemma UNIV_subtract:
+  shows "UNIV - EVEN = ODD"
+  and   "UNIV - ODD  = EVEN"
+  using EVEN_union_ODD EVEN_intersect_ODD
+  by (blast)+
+
+lemma EVEN_ODD_infinite:
+  shows "infinite EVEN"
+  and   "infinite ODD"
+apply(simp add: infinite_iff_countable_subset)
+apply(rule_tac x="\<lambda>n. atom (2*n)" in exI)
+apply(auto simp add: inj_on_def)[1]
+apply(simp add: infinite_iff_countable_subset)
+apply(rule_tac x="\<lambda>n. atom (2*n+1)" in exI)
+apply(auto simp add: inj_on_def)
+done
+
+(* A set S that is infinite and coinfinite has all atoms as its support *)
+lemma supp_infinite_coinfinite:
+  fixes S::"atom set"
+  assumes a: "infinite S"
+  and     b: "infinite (UNIV-S)"
+  shows "(supp S) = (UNIV::atom set)"
+proof -
+  have "\<forall>(x::atom). x\<in>(supp S)"
+  proof
+    fix x::"atom"
+    show "x\<in>(supp S)"
+    proof (cases "x\<in>S")
+      case True
+      have "x\<in>S" by fact
+      hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
+      with b have "infinite {b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
+      hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
+      then show "x\<in>(supp S)" by (simp add: supp_def)
+    next
+      case False
+      have "x\<notin>S" by fact
+      hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
+      with a have "infinite {b\<in>S. [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
+      hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
+      then show "x\<in>(supp S)" by (simp add: supp_def)
+    qed
+  qed
+  then show "(supp S) = (UNIV::atom set)" by auto
+qed
+
+lemma EVEN_ODD_supp:
+  shows "supp EVEN = (UNIV::atom set)"
+  and   "supp ODD  = (UNIV::atom set)"
+  using supp_infinite_coinfinite UNIV_subtract EVEN_ODD_infinite
+  by simp_all
+
+lemma UNIV_supp:
+  shows "supp (UNIV::atom set) = ({}::atom set)"
+proof -
+  have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)"
+    by (auto simp add: perm_set_def calc_atm)
+  then show "supp (UNIV::atom set) = ({}::atom set)"
+    by (simp add: supp_def)
+qed
+
+theorem EVEN_ODD_freshness:
+  fixes x::"atom"
+  shows "x\<sharp>(EVEN \<union> ODD)"
+  and   "\<not>x\<sharp>EVEN"
+  and   "\<not>x\<sharp>ODD"
+  by (auto simp only: fresh_def EVEN_union_ODD EVEN_ODD_supp UNIV_supp)
+
+end
\ No newline at end of file
diff -r 163c82d039cf -r 7cbb842aa99e src/HOL/Nominal/Examples/VC-Compatible.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/VC-Compatible.thy	Mon Oct 08 05:23:47 2007 +0200
@@ -0,0 +1,190 @@
+(* $Id$ *)
+
+theory VC_NonCompatible
+imports "../Nominal" 
+begin
+
+text {* 
+  We show here two examples where using the variable  
+  convention carelessly in rule inductions, we end 
+  up with faulty lemmas. The point is that the examples
+  are not variable-convention compatible and therefore
+  in the nominal package one is protected from such
+  bogus reasoning.
+*}
+
+text {* 
+  We define alpha-equated lambda-terms as usual. 
+*}
+atom_decl name 
+
+nominal_datatype lam = 
+    Var "name"
+  | App "lam" "lam"
+  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+
+text {*
+  The inductive relation "unbind" unbinds the top-most  
+  binders of a lambda-term; this relation is obviously  
+  not a function, since it does not respect alpha-      
+  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
+  u_var: "(Var a) \<mapsto> [],(Var a)"
+| u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)"
+| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'"
+
+text {* Unbind is equivariant ...*}
+equivariance unbind
+
+text {*
+  ... but it is not variable-convention compatible (see Urban, 
+  Berghofer, Norrish [2007] for more details). This condition 
+  requires for rule u_lam, that the binder x is not a free variable 
+  in the rule's conclusion. Beacuse this condition is not satisfied, 
+  Isabelle will not derive a strong induction principle for unbind 
+  - that means Isabelle does not allow us to use the variable 
+  convention in induction proofs involving unbind. We can, however,  
+  force Isabelle to derive the strengthening induction principle. 
+*}
+nominal_inductive unbind
+  sorry
+
+text {*
+  We can show that %x.%x. x unbinds to [x,x],x and 
+  also to [z,y],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)
+
+lemma unbind_lambda_lambda2: 
+  shows "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)"
+proof -
+  have "Lam [x].Lam [x].(Var x) = Lam [y].Lam [z].(Var z)" 
+    by (auto simp add: lam.inject alpha calc_atm abs_fresh fresh_atm)
+  moreover
+  have "Lam [y].Lam [z].(Var z) \<mapsto> [y,z],(Var z)"
+    by (auto intro: unbind.intros)
+  ultimately 
+  show "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" by simp
+qed
+
+text {*
+  The function 'bind' takes a list of names and abstracts 
+  away these names in a given lambda-term.                                     
+*}
+fun 
+  bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "bind [] t = t"
+| "bind (x#xs) t = Lam [x].(bind xs t)"
+
+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'"
+using a by (induct) (auto)
+
+text {*
+  The next lemma shows that if x is a free 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"
+  shows "\<not>(x\<sharp>bind xs t)"
+using a b
+by (induct xs)
+   (auto simp add: fresh_list_cons abs_fresh fresh_atm)
+
+text {*
+  Now comes the faulty lemma. It is derived using the     
+  variable convention, that means using the strong induction 
+  principle we 'proved' above by using sorry. This faulty    
+  lemma states that if t unbinds to x::xs and t', and x is a 
+  free variable in t', then it is also a free variable in    
+  bind xs t'. We show this lemma by assuming that the binder 
+  x is fresh w.r.t. to the xs unbound previously.            
+*}   
+lemma faulty1:
+  assumes a: "t\<mapsto>(x#xs),t'"
+  shows "\<not>(x\<sharp>t') \<Longrightarrow> \<not>(x\<sharp>bind xs t')"
+using a
+by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct)
+   (simp_all add: free_variable)
+
+text {*
+  Obviously the faulty lemma does not hold for the case 
+  Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x).             
+*}
+lemma false1:
+  shows "False"
+proof -
+  have "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" 
+  and  "\<not>(x\<sharp>Var x)" by (simp_all add: unbind_lambda_lambda1 fresh_atm)
+  then have "\<not>(x\<sharp>(bind [x] (Var x)))" by (rule faulty1)
+  moreover 
+  have "x\<sharp>(bind [x] (Var x))" by (simp add: abs_fresh)
+  ultimately
+  show "False" by simp
+qed
+   
+text {* 
+  The next example is slightly simpler, but looks more
+  contrived than unbind. This example just strips off
+  the top-most binders from lambdas. 
+*}
+
+inductive
+  strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60)
+where
+  s_var: "(Var a) \<rightarrow> (Var a)"
+| s_app: "(App t1 t2) \<rightarrow> (App t1 t2)"
+| s_lam: "t \<rightarrow> t' \<Longrightarrow> (Lam [x].t) \<rightarrow> t'"
+
+text {* 
+  The relation is equivariant but we have to use again 
+  sorry to derive a strong induction principle.
+*}
+equivariance strip
+
+nominal_inductive strip
+  sorry
+
+text {*
+  The faulty lemma shows that a variable that is fresh
+  for a term is also fresh for the term after striping.
+*}
+lemma faulty2:
+  fixes x::"name"
+  assumes a: "t \<rightarrow> t'"
+  shows "x\<sharp>t \<Longrightarrow> x\<sharp>t'"
+using a
+by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct)
+   (auto simp add: abs_fresh)
+
+text {*
+  Obviously %x.x is an counter example to this lemma.
+*}
+lemma false2:
+  shows "False"
+proof -
+  have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros)
+  moreover
+  have "x\<sharp>Lam [x].(Var x)" by (simp add: abs_fresh)
+  ultimately have "x\<sharp>(Var x)" by (simp only: faulty2)
+  then show "False" by (simp add: fresh_atm)
+qed 
+ 
+end
\ No newline at end of file