author urbanc Sun, 21 Oct 2007 19:32:19 +0200 changeset 25139 ffc5054a7274 parent 25138 e453c480d599 child 25140 273772abbea2
tuned
--- a/src/HOL/Nominal/Examples/Support.thy	Sun Oct 21 19:12:05 2007 +0200
+++ b/src/HOL/Nominal/Examples/Support.thy	Sun Oct 21 19:32:19 2007 +0200
@@ -5,17 +5,15 @@
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.
-
+  For this we set A 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
@@ -37,6 +35,7 @@

lemma EVEN_union_ODD:
shows "EVEN \<union> ODD = UNIV"
+  using even_or_odd
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
@@ -69,7 +68,9 @@
done

-(* A set S that is infinite and coinfinite has all atoms as its support *)
+text {*
+  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"
--- a/src/HOL/Nominal/Examples/VC_Compatible.thy	Sun Oct 21 19:12:05 2007 +0200
+++ b/src/HOL/Nominal/Examples/VC_Compatible.thy	Sun Oct 21 19:32:19 2007 +0200
@@ -5,17 +5,15 @@
begin

text {*
-  We show here two examples where using the variable
-  convention carelessly in rule inductions, we end
+  We give here two examples that show if we use the variable
+  convention carelessly in rule inductions, we might 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.
+  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.
-*}
+  We define alpha-equated lambda-terms as usual. *}
atom_decl name

nominal_datatype lam =
@@ -27,10 +25,9 @@
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
+  equivalence. However as a relation 'unbind' is ok and
a similar relation has been used in our formalisation
-  of the algorithm W.
-*}
+  of the algorithm W. *}
inductive
unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
where
@@ -39,10 +36,9 @@
| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'"

text {*
-  We can show that Lam [x]. Lam [x]. Var x unbinds to [x,x],Var x
+  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).
-*}
+  bit clumsy). *}
lemma unbind_lambda_lambda1:
shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
by (auto intro: unbind.intros)
@@ -65,21 +61,21 @@
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
+  requires for rule u_lam to have the binder x being not a free variable
in the rule's conclusion. Because this condition is not satisfied,
-  Isabelle will not derive a strong induction principle for unbind
-  - that means Isabelle does not allow you to use the variable
-  convention in induction proofs involving unbind. We can, however,
-  force Isabelle to derive the strengthening induction principle.
-*}
+  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 over 'unbind'. We can, however,
+  force Isabelle to derive the strengthening induction principle
+  and see what happens. *}
+
nominal_inductive unbind
sorry

text {*
-  To obtain our faulty lemma, we introduce the function 'bind'
+  To obtain a faulty lemma, we introduce the function 'bind'
which takes a list of names and abstracts away these names in
-  a given lambda-term.
-*}
+  a given lambda-term. *}
fun
bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
where
@@ -88,8 +84,7 @@

text {*
Although not necessary for our main argument below, we can
-  easily prove that bind undoes the unbinding.
-*}
+  easily prove that bind undoes the unbinding. *}
lemma bind_unbind:
assumes a: "t \<mapsto> xs,t'"
shows "t = bind xs t'"
@@ -99,8 +94,7 @@
The next lemma shows by induction on xs 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'.
-*}
+  '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"
@@ -111,13 +105,12 @@

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.
-*}
+  variable convention (i.e. our strong induction principle).
+  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')"
@@ -128,8 +121,8 @@
text {*
Obviously the faulty lemma does not hold, for example, in
case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). Therefore,
-  we can prove False.
-*}
+  we can prove False. *}
+
lemma false1:
shows "False"
proof -
@@ -145,8 +138,7 @@
text {*
The next example is slightly simpler, but looks more
contrived than 'unbind'. This example, caled 'strip' just
-  strips off the top-most binders from lambdas.
-*}
+  strips off the top-most binders from lambdas. *}

inductive
strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60)
@@ -157,8 +149,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
@@ -166,8 +158,8 @@

text {*
The faulty lemma shows that a variable that is fresh
-  for a term is also fresh for the term after striping.
-*}
+  for a term is also fresh for the term after striping. *}
+
lemma faulty2:
fixes x::"name"
assumes a: "t \<rightarrow> t'"
@@ -177,8 +169,8 @@