--- a/src/HOL/Nominal/Examples/VC_Condition.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy Thu May 26 17:51:22 2016 +0200
@@ -2,15 +2,15 @@
imports "../Nominal"
begin
-text {*
+text \<open>
We give here two examples showing that 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 data package one is protected from such bogus reasoning.
-*}
+\<close>
-text {* We define alpha-equated lambda-terms as usual. *}
+text \<open>We define alpha-equated lambda-terms as usual.\<close>
atom_decl name
nominal_datatype lam =
@@ -18,13 +18,13 @@
| App "lam" "lam"
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
-text {*
+text \<open>
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. *}
+ of the algorithm W.\<close>
inductive
unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
@@ -33,10 +33,10 @@
| u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)"
| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'"
-text {*
+text \<open>
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).\<close>
lemma unbind_lambda_lambda1:
shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
@@ -54,10 +54,10 @@
show "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" by simp
qed
-text {* Unbind is equivariant ...*}
+text \<open>Unbind is equivariant ...\<close>
equivariance unbind
-text {*
+text \<open>
... but it is not variable-convention compatible (see Urban,
Berghofer, Norrish [2007]). This condition requires for rule u_lam to
have the binder x not being a free variable in this rule's conclusion.
@@ -65,15 +65,15 @@
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. *}
+ principle and see what happens.\<close>
nominal_inductive unbind
sorry
-text {*
+text \<open>
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. *}
+ a given lambda-term.\<close>
fun
bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
@@ -81,20 +81,20 @@
"bind [] t = t"
| "bind (x#xs) t = Lam [x].(bind xs t)"
-text {*
+text \<open>
Although not necessary for our main argument below, we can
- easily prove that bind undoes the unbinding. *}
+ easily prove that bind undoes the unbinding.\<close>
lemma bind_unbind:
assumes a: "t \<mapsto> xs,t'"
shows "t = bind xs t'"
using a by (induct) (auto)
-text {*
+text \<open>
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'.\<close>
lemma free_variable:
fixes x::"name"
@@ -104,13 +104,13 @@
by (induct xs)
(auto simp add: fresh_list_cons abs_fresh fresh_atm)
-text {*
+text \<open>
Now comes the first faulty lemma. It is derived using the
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. *}
+ the binder x is fresh w.r.t. to the xs unbound previously.\<close>
lemma faulty1:
assumes a: "t\<mapsto>(x#xs),t'"
@@ -119,10 +119,10 @@
by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct)
(simp_all add: free_variable)
-text {*
+text \<open>
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.\<close>
lemma false1:
shows "False"
@@ -137,10 +137,10 @@
show "False" by simp
qed
-text {*
+text \<open>
The next example is slightly simpler, but looks more
contrived than 'unbind'. This example, called 'strip' just
- strips off the top-most binders from lambdas. *}
+ strips off the top-most binders from lambdas.\<close>
inductive
strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60)
@@ -149,18 +149,18 @@
| s_app: "(App t1 t2) \<rightarrow> (App t1 t2)"
| s_lam: "t \<rightarrow> t' \<Longrightarrow> (Lam [x].t) \<rightarrow> t'"
-text {*
+text \<open>
The relation is equivariant but we have to use again
- sorry to derive a strong induction principle. *}
+ sorry to derive a strong induction principle.\<close>
equivariance strip
nominal_inductive strip
sorry
-text {*
+text \<open>
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.\<close>
lemma faulty2:
fixes x::"name"
@@ -170,7 +170,7 @@
by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct)
(auto simp add: abs_fresh)
-text {* Obviously Lam [x].Var x is a counter example to this lemma. *}
+text \<open>Obviously Lam [x].Var x is a counter example to this lemma.\<close>
lemma false2:
shows "False"
@@ -183,8 +183,8 @@
then show "False" by (simp add: fresh_atm)
qed
-text {* A similar effect can be achieved by using naive inversion
- on rules. *}
+text \<open>A similar effect can be achieved by using naive inversion
+ on rules.\<close>
lemma false3:
shows "False"
@@ -202,9 +202,9 @@
by (cases) (simp_all add: lam.inject fresh_atm)
qed
-text {*
+text \<open>
Moral: Who would have thought that the variable convention
is in general an unsound reasoning principle.
- *}
+\<close>
end