--- 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
--- /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
--- /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