--- a/src/FOL/IFOL.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/FOL/IFOL.thy Thu Jun 14 23:04:36 2007 +0200
@@ -319,27 +319,23 @@
***)
lemma ex1I:
- assumes "P(a)"
- and "!!x. P(x) ==> x=a"
- shows "EX! x. P(x)"
+ "P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)"
apply (unfold ex1_def)
- apply (assumption | rule assms exI conjI allI impI)+
+ apply (assumption | rule exI conjI allI impI)+
done
(*Sometimes easier to use: the premises have no shared variables. Safe!*)
lemma ex_ex1I:
- assumes ex: "EX x. P(x)"
- and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
- shows "EX! x. P(x)"
- apply (rule ex [THEN exE])
- apply (assumption | rule ex1I eq)+
+ "EX x. P(x) \<Longrightarrow> (!!x y. [| P(x); P(y) |] ==> x=y) \<Longrightarrow> EX! x. P(x)"
+ apply (erule exE)
+ apply (rule ex1I)
+ apply assumption
+ apply assumption
done
lemma ex1E:
- assumes ex1: "EX! x. P(x)"
- and r: "!!x. [| P(x); ALL y. P(y) --> y=x |] ==> R"
- shows R
- apply (insert ex1, unfold ex1_def)
+ "EX! x. P(x) \<Longrightarrow> (!!x. [| P(x); ALL y. P(y) --> y=x |] ==> R) \<Longrightarrow> R"
+ apply (unfold ex1_def)
apply (assumption | erule exE conjE)+
done
@@ -572,11 +568,11 @@
(*Simplifies the implication. Classical version is stronger.
Still UNSAFE since ~P must be provable -- backtracking needed. *)
lemma not_impE:
- assumes major: "~P --> S"
- and r1: "P ==> False"
- and r2: "S ==> R"
- shows R
- apply (assumption | rule notI impI major [THEN mp] r1 r2)+
+ "~P --> S \<Longrightarrow> (P ==> False) \<Longrightarrow> (S ==> R) \<Longrightarrow> R"
+ apply (drule mp)
+ apply (rule notI)
+ apply assumption
+ apply assumption
done
(*Simplifies the implication. UNSAFE. *)
@@ -595,7 +591,7 @@
and r1: "!!x. P(x)"
and r2: "S ==> R"
shows R
- apply (assumption | rule allI impI major [THEN mp] r1 r2)+
+ apply (rule allI impI major [THEN mp] r1 r2)+
done
(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *)
@@ -609,10 +605,8 @@
(*** Courtesy of Krzysztof Grabczewski ***)
lemma disj_imp_disj:
- assumes major: "P|Q"
- and "P==>R" and "Q==>S"
- shows "R|S"
- apply (rule disjE [OF major])
+ "P|Q \<Longrightarrow> (P==>R) \<Longrightarrow> (Q==>S) \<Longrightarrow> R|S"
+ apply (erule disjE)
apply (rule disjI1) apply assumption
apply (rule disjI2) apply assumption
done
--- a/src/HOL/Isar_examples/BasicLogic.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Thu Jun 14 23:04:36 2007 +0200
@@ -22,7 +22,7 @@
lemma I: "A --> A"
proof
assume A
- show A by assumption
+ show A by fact
qed
lemma K: "A --> B --> A"
@@ -30,7 +30,7 @@
assume A
show "B --> A"
proof
- show A by assumption
+ show A by fact
qed
qed
@@ -45,8 +45,8 @@
assume A
show C
proof (rule mp)
- show "B --> C" by (rule mp) assumption+
- show B by (rule mp) assumption+
+ show "B --> C" by (rule mp) fact+
+ show B by (rule mp) fact+
qed
qed
qed
@@ -65,7 +65,7 @@
lemma "A --> A"
proof
assume A
- show A by assumption
+ show A by fact+
qed
text {*
@@ -117,7 +117,7 @@
lemma "A --> B --> A"
proof (intro impI)
assume A
- show A by assumption
+ show A by fact
qed
text {*
@@ -162,8 +162,8 @@
assume "A & B"
show "B & A"
proof
- show B by (rule conjunct2) assumption
- show A by (rule conjunct1) assumption
+ show B by (rule conjunct2) fact
+ show A by (rule conjunct1) fact
qed
qed
@@ -294,9 +294,9 @@
proof -- {*
rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
*}
- assume P show P by assumption
+ assume P show P by fact
next
- assume P show P by assumption
+ assume P show P by fact
qed
qed
@@ -330,8 +330,8 @@
then show P
proof
assume P
- show P by assumption
- show P by assumption
+ show P by fact
+ show P by fact
qed
qed
@@ -439,8 +439,8 @@
assume r: "A ==> B ==> C"
show C
proof (rule r)
- show A by (rule conjunct1) assumption
- show B by (rule conjunct2) assumption
+ show A by (rule conjunct1) fact
+ show B by (rule conjunct2) fact
qed
qed
--- a/src/HOL/Lattice/Bounds.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Lattice/Bounds.thy Thu Jun 14 23:04:36 2007 +0200
@@ -193,8 +193,8 @@
show ?thesis
proof
show "x \<sqsubseteq> x" ..
- show "x \<sqsubseteq> y" by assumption
- fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by assumption
+ show "x \<sqsubseteq> y" by fact
+ fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact
qed
qed
@@ -203,10 +203,10 @@
assume "x \<sqsubseteq> y"
show ?thesis
proof
- show "x \<sqsubseteq> y" by assumption
+ show "x \<sqsubseteq> y" by fact
show "y \<sqsubseteq> y" ..
fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
- show "y \<sqsubseteq> z" by assumption
+ show "y \<sqsubseteq> z" by fact
qed
qed
--- a/src/HOL/Lattice/Lattice.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Lattice/Lattice.thy Thu Jun 14 23:04:36 2007 +0200
@@ -232,7 +232,7 @@
show "x \<sqsubseteq> x" ..
show "x \<sqsubseteq> x \<squnion> y" ..
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
- show "z \<sqsubseteq> x" by assumption
+ show "z \<sqsubseteq> x" by fact
qed
theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
--- a/src/HOL/Nominal/Examples/CR.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy Thu Jun 14 23:04:36 2007 +0200
@@ -24,7 +24,7 @@
ultimately show "(App M1 M2)[x::=P] = (App M1 M2)" by simp
next
case (Lam z M)
- have vc: "z\<sharp>x" "z\<sharp>P" by fact
+ have vc: "z\<sharp>x" "z\<sharp>P" by fact+
have ih: "x\<sharp>M \<Longrightarrow> M[x::=P] = M" by fact
have asm: "x\<sharp>Lam [z].M" by fact
then have "x\<sharp>M" using vc by (simp add: fresh_atm abs_fresh)
@@ -46,7 +46,7 @@
using asms
proof (nominal_induct N avoiding: z y L rule: lam.induct)
case (Var u)
- have "z\<sharp>(Var u)" "z\<sharp>L" by fact
+ have "z\<sharp>(Var u)" "z\<sharp>L" by fact+
thus "z\<sharp>((Var u)[y::=L])" by simp
next
case (App N1 N2)
@@ -54,11 +54,11 @@
moreover
have ih2: "\<lbrakk>z\<sharp>N2; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>N2[y::=L]" by fact
moreover
- have "z\<sharp>App N1 N2" "z\<sharp>L" by fact
+ have "z\<sharp>App N1 N2" "z\<sharp>L" by fact+
ultimately show "z\<sharp>((App N1 N2)[y::=L])" by simp
next
case (Lam u N1)
- have vc: "u\<sharp>z" "u\<sharp>y" "u\<sharp>L" by fact
+ have vc: "u\<sharp>z" "u\<sharp>y" "u\<sharp>L" by fact+
have "z\<sharp>Lam [u].N1" by fact
hence "z\<sharp>N1" using vc by (simp add: abs_fresh fresh_atm)
moreover
@@ -123,7 +123,7 @@
have ih: "\<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
have "x\<noteq>y" by fact
have "x\<sharp>L" by fact
- have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact
+ have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact+
hence "z\<sharp>N[y::=L]" by (simp add: fresh_fact)
show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS")
proof -
@@ -334,7 +334,7 @@
using a
proof (nominal_induct M avoiding: x N N' rule: lam.induct)
case (Var y)
- show "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y", auto)
+ thus "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y") auto
next
case (App P Q) (* application case - third line *)
thus "(App P Q)[x::=N] \<longrightarrow>\<^isub>1 (App P Q)[x::=N']" using o2 by simp
@@ -367,7 +367,7 @@
thus ?case by simp
next
case (o4 a N1 N2 M1 M2 N N' x)
- have vc: "a\<sharp>N" "a\<sharp>N'" "a\<sharp>x" "a\<sharp>N1" "a\<sharp>N2" by fact
+ have vc: "a\<sharp>N" "a\<sharp>N'" "a\<sharp>x" "a\<sharp>N1" "a\<sharp>N2" by fact+
have asm: "N\<longrightarrow>\<^isub>1N'" by fact
show ?case
proof -
@@ -401,7 +401,7 @@
thus "\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
next
case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*)
- have vc: "x\<sharp>Q" "x\<sharp>Q'" by fact
+ have vc: "x\<sharp>Q" "x\<sharp>Q'" by fact+
have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
have "App (Lam [x].P) Q \<longrightarrow>\<^isub>1 M2" by fact
@@ -559,8 +559,8 @@
case o3 thus ?case by (blast intro!: one_lam_cong)
next
case (o4 a s1 s2 t1 t2)
- have vc: "a\<sharp>s1" "a\<sharp>s2" by fact
- have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" by fact
+ have vc: "a\<sharp>s1" "a\<sharp>s2" by fact+
+ have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" by fact+
have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^isub>\<beta> (t2 [a::= s2])" using vc by (simp add: b4)
from a1 a2 have c2: "App (Lam [a].t1 ) s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App (Lam [a].t2 ) s2"
by (blast intro!: one_app_cong one_lam_cong)
--- a/src/HOL/Nominal/Examples/Class.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy Thu Jun 14 23:04:36 2007 +0200
@@ -5878,7 +5878,7 @@
qed
next
case (Cut b M z N x a y)
- have fs: "b\<sharp>x" "b\<sharp>a" "b\<sharp>y" "b\<sharp>N" "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "z\<sharp>M" by fact
+ have fs: "b\<sharp>x" "b\<sharp>a" "b\<sharp>y" "b\<sharp>N" "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "z\<sharp>M" by fact+
have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* N[x\<turnstile>n>y]" by fact
show "(Cut <b>.M (z).N){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (Cut <b>.M (z).N)[x\<turnstile>n>y]"
@@ -5900,14 +5900,14 @@
qed
next
case (NotR z M b x a y)
- have fs: "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "z\<sharp>b" by fact
+ have fs: "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "z\<sharp>b" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
have "(NotR (z).M b){x:=<a>.Ax y a} = NotR (z).(M{x:=<a>.Ax y a}) b" using fs by simp
also have "\<dots> \<longrightarrow>\<^isub>a* NotR (z).(M[x\<turnstile>n>y]) b" using ih by (auto intro: a_star_congs)
finally show "(NotR (z).M b){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (NotR (z).M b)[x\<turnstile>n>y]" using fs by simp
next
case (NotL b M z x a y)
- have fs: "b\<sharp>x" "b\<sharp>a" "b\<sharp>y" "b\<sharp>z" by fact
+ have fs: "b\<sharp>x" "b\<sharp>a" "b\<sharp>y" "b\<sharp>z" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
show "(NotL <b>.M z){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (NotL <b>.M z)[x\<turnstile>n>y]"
proof(cases "z=x")
@@ -5939,7 +5939,7 @@
qed
next
case (AndR c M d N e x a y)
- have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "d\<sharp>x" "d\<sharp>a" "d\<sharp>y" "d\<noteq>c" "c\<sharp>N" "c\<sharp>e" "d\<sharp>M" "d\<sharp>e" by fact
+ have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "d\<sharp>x" "d\<sharp>a" "d\<sharp>y" "d\<noteq>c" "c\<sharp>N" "c\<sharp>e" "d\<sharp>M" "d\<sharp>e" by fact+
have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* N[x\<turnstile>n>y]" by fact
have "(AndR <c>.M <d>.N e){x:=<a>.Ax y a} = AndR <c>.(M{x:=<a>.Ax y a}) <d>.(N{x:=<a>.Ax y a}) e"
@@ -5949,7 +5949,7 @@
using fs by simp
next
case (AndL1 u M v x a y)
- have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "u\<sharp>v" by fact
+ have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "u\<sharp>v" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
show "(AndL1 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (AndL1 (u).M v)[x\<turnstile>n>y]"
proof(cases "v=x")
@@ -5983,7 +5983,7 @@
qed
next
case (AndL2 u M v x a y)
- have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "u\<sharp>v" by fact
+ have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "u\<sharp>v" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
show "(AndL2 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (AndL2 (u).M v)[x\<turnstile>n>y]"
proof(cases "v=x")
@@ -6017,21 +6017,21 @@
qed
next
case (OrR1 c M d x a y)
- have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "c\<sharp>d" by fact
+ have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "c\<sharp>d" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
have "(OrR1 <c>.M d){x:=<a>.Ax y a} = OrR1 <c>.(M{x:=<a>.Ax y a}) d" using fs by (simp add: fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* OrR1 <c>.(M[x\<turnstile>n>y]) d" using ih by (auto intro: a_star_congs)
finally show "(OrR1 <c>.M d){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (OrR1 <c>.M d)[x\<turnstile>n>y]" using fs by simp
next
case (OrR2 c M d x a y)
- have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "c\<sharp>d" by fact
+ have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "c\<sharp>d" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
have "(OrR2 <c>.M d){x:=<a>.Ax y a} = OrR2 <c>.(M{x:=<a>.Ax y a}) d" using fs by (simp add: fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* OrR2 <c>.(M[x\<turnstile>n>y]) d" using ih by (auto intro: a_star_congs)
finally show "(OrR2 <c>.M d){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (OrR2 <c>.M d)[x\<turnstile>n>y]" using fs by simp
next
case (OrL u M v N z x a y)
- have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "v\<sharp>x" "v\<sharp>a" "v\<sharp>y" "v\<noteq>u" "u\<sharp>N" "u\<sharp>z" "v\<sharp>M" "v\<sharp>z" by fact
+ have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "v\<sharp>x" "v\<sharp>a" "v\<sharp>y" "v\<noteq>u" "u\<sharp>N" "u\<sharp>z" "v\<sharp>M" "v\<sharp>z" by fact+
have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* N[x\<turnstile>n>y]" by fact
show "(OrL (u).M (v).N z){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (OrL (u).M (v).N z)[x\<turnstile>n>y]"
@@ -6070,7 +6070,7 @@
qed
next
case (ImpR z c M d x a y)
- have fs: "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "z\<sharp>d" "c\<sharp>d" by fact
+ have fs: "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "z\<sharp>d" "c\<sharp>d" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
have "(ImpR (z).<c>.M d){x:=<a>.Ax y a} = ImpR (z).<c>.(M{x:=<a>.Ax y a}) d" using fs by simp
also have "\<dots> \<longrightarrow>\<^isub>a* ImpR (z).<c>.(M[x\<turnstile>n>y]) d" using ih by (auto intro: a_star_congs)
@@ -6135,7 +6135,7 @@
qed
next
case (Cut c M z N b a x)
- have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>N" "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "z\<sharp>M" by fact
+ have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>N" "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "z\<sharp>M" by fact+
have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* N[b\<turnstile>c>a]" by fact
show "(Cut <c>.M (z).N){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (Cut <c>.M (z).N)[b\<turnstile>c>a]"
@@ -6157,7 +6157,7 @@
qed
next
case (NotR z M c b a x)
- have fs: "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "z\<sharp>c" by fact
+ have fs: "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "z\<sharp>c" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
show "(NotR (z).M c){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (NotR (z).M c)[b\<turnstile>c>a]"
proof (cases "c=b")
@@ -6190,14 +6190,14 @@
qed
next
case (NotL c M z b a x)
- have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>z" by fact
+ have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>z" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
have "(NotL <c>.M z){b:=(x).Ax x a} = NotL <c>.(M{b:=(x).Ax x a}) z" using fs by simp
also have "\<dots> \<longrightarrow>\<^isub>a* NotL <c>.(M[b\<turnstile>c>a]) z" using ih by (auto intro: a_star_congs)
finally show "(NotL <c>.M z){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (NotL <c>.M z)[b\<turnstile>c>a]" using fs by simp
next
case (AndR c M d N e b a x)
- have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "d\<sharp>b" "d\<sharp>a" "d\<sharp>x" "d\<noteq>c" "c\<sharp>N" "c\<sharp>e" "d\<sharp>M" "d\<sharp>e" by fact
+ have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "d\<sharp>b" "d\<sharp>a" "d\<sharp>x" "d\<noteq>c" "c\<sharp>N" "c\<sharp>e" "d\<sharp>M" "d\<sharp>e" by fact+
have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* N[b\<turnstile>c>a]" by fact
show "(AndR <c>.M <d>.N e){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (AndR <c>.M <d>.N e)[b\<turnstile>c>a]"
@@ -6235,21 +6235,21 @@
qed
next
case (AndL1 u M v b a x)
- have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "u\<sharp>v" by fact
+ have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "u\<sharp>v" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
have "(AndL1 (u).M v){b:=(x).Ax x a} = AndL1 (u).(M{b:=(x).Ax x a}) v" using fs by simp
also have "\<dots> \<longrightarrow>\<^isub>a* AndL1 (u).(M[b\<turnstile>c>a]) v" using ih by (auto intro: a_star_congs)
finally show "(AndL1 (u).M v){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (AndL1 (u).M v)[b\<turnstile>c>a]" using fs by simp
next
case (AndL2 u M v b a x)
- have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "u\<sharp>v" by fact
+ have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "u\<sharp>v" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
have "(AndL2 (u).M v){b:=(x).Ax x a} = AndL2 (u).(M{b:=(x).Ax x a}) v" using fs by simp
also have "\<dots> \<longrightarrow>\<^isub>a* AndL2 (u).(M[b\<turnstile>c>a]) v" using ih by (auto intro: a_star_congs)
finally show "(AndL2 (u).M v){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (AndL2 (u).M v)[b\<turnstile>c>a]" using fs by simp
next
case (OrR1 c M d b a x)
- have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>d" by fact
+ have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>d" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
show "(OrR1 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (OrR1 <c>.M d)[b\<turnstile>c>a]"
proof(cases "d=b")
@@ -6283,7 +6283,7 @@
qed
next
case (OrR2 c M d b a x)
- have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>d" by fact
+ have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>d" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
show "(OrR2 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (OrR2 <c>.M d)[b\<turnstile>c>a]"
proof(cases "d=b")
@@ -6317,7 +6317,7 @@
qed
next
case (OrL u M v N z b a x)
- have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "v\<sharp>b" "v\<sharp>a" "v\<sharp>x" "v\<noteq>u" "u\<sharp>N" "u\<sharp>z" "v\<sharp>M" "v\<sharp>z" by fact
+ have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "v\<sharp>b" "v\<sharp>a" "v\<sharp>x" "v\<noteq>u" "u\<sharp>N" "u\<sharp>z" "v\<sharp>M" "v\<sharp>z" by fact+
have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* N[b\<turnstile>c>a]" by fact
have "(OrL (u).M (v).N z){b:=(x).Ax x a} = OrL (u).(M{b:=(x).Ax x a}) (v).(N{b:=(x).Ax x a}) z"
@@ -6326,7 +6326,7 @@
finally show "(OrL (u).M (v).N z){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (OrL (u).M (v).N z)[b\<turnstile>c>a]" using fs by simp
next
case (ImpR z c M d b a x)
- have fs: "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "z\<sharp>d" "c\<sharp>d" by fact
+ have fs: "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "z\<sharp>d" "c\<sharp>d" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
show "(ImpR (z).<c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (ImpR (z).<c>.M d)[b\<turnstile>c>a]"
proof(cases "b=d")
@@ -6360,7 +6360,7 @@
qed
next
case (ImpL c M u N v b a x)
- have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "c\<sharp>N" "c\<sharp>v" "u\<sharp>M" "u\<sharp>v" by fact
+ have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "c\<sharp>N" "c\<sharp>v" "u\<sharp>M" "u\<sharp>v" by fact+
have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* N[b\<turnstile>c>a]" by fact
have "(ImpL <c>.M (u).N v){b:=(x).Ax x a} = ImpL <c>.(M{b:=(x).Ax x a}) (u).(N{b:=(x).Ax x a}) v"
@@ -7124,7 +7124,7 @@
using a
proof(nominal_induct M avoiding: x a P b y Q rule: trm.induct)
case (Ax z c)
- have fs: "a\<sharp>(Q,b)" "x\<sharp>(y,P,Q)" "b\<sharp>Q" "y\<sharp>P" by fact
+ have fs: "a\<sharp>(Q,b)" "x\<sharp>(y,P,Q)" "b\<sharp>Q" "y\<sharp>P" by fact+
{ assume asm: "z=x \<and> c=b"
have "(Ax x b){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (x).Ax x b){b:=(y).Q}" using fs by simp
also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).Q"
@@ -10052,7 +10052,7 @@
proof (induct a rule: SNa.induct)
case (SNaI x)
note SNa' = this
- have "SNa b" .
+ have "SNa b" by fact
thus ?case
proof (induct b rule: SNa.induct)
case (SNaI y)
--- a/src/HOL/Nominal/Examples/Crary.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy Thu Jun 14 23:04:36 2007 +0200
@@ -168,7 +168,7 @@
using assms
proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct)
case (Lam y t x u)
- have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact
+ have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact+
moreover have "x\<sharp> Lam [y].t" by fact
ultimately have "x\<sharp>t" by (simp add: abs_fresh fresh_atm)
moreover have ih:"\<And>n T. n\<sharp>t \<Longrightarrow> ((n,T)#\<theta>)<t> = \<theta><t>" by fact
@@ -244,7 +244,7 @@
ultimately show ?case by auto
next
case (Lam n t x u \<theta>)
- have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact
+ have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact+
have ih:"\<And> y s \<theta>. y\<sharp>\<theta> \<Longrightarrow> ((\<theta><(t[y::=s])>) = ((\<theta><t>)[y::=(\<theta><s>)]))" by fact
have "\<theta> <(Lam [n].t)[x::=u]> = \<theta><Lam [n]. (t [x::=u])>" using fs by auto
then have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n]. \<theta><t [x::=u]>" using fs by auto
@@ -436,7 +436,7 @@
using assms
proof (induct arbitrary: b)
case (QAN_Reduce x t a b)
- have h:"x \<leadsto> t" "t \<Down> a" by fact
+ have h:"x \<leadsto> t" "t \<Down> a" by fact+
have ih:"\<And>b. t \<Down> b \<Longrightarrow> a = b" by fact
have "x \<Down> b" by fact
then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto
@@ -519,14 +519,14 @@
case (QAP_Var \<Gamma> x T u T')
have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact
then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto
- moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact
+ moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact+
ultimately show "T=T'" using type_unicity_in_context by auto
next
case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u T\<^isub>2')
- have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^isub>1\<rightarrow>T\<^isub>2 = T" by fact
+ have ih: "\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^isub>1\<rightarrow>T\<^isub>2 = T" by fact
have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2'" by fact
then obtain r t T\<^isub>1' where "u = App r t" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
- then have "T\<^isub>1\<rightarrow>T\<^isub>2 = T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
+ with ih have "T\<^isub>1\<rightarrow>T\<^isub>2 = T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
then show "T\<^isub>2=T\<^isub>2'" using ty.inject by auto
qed (auto)
@@ -559,7 +559,7 @@
case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2 u)
have ih:"(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2
\<Longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by fact
- have fs: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>u" by fact
+ have fs: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>u" by fact+
have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" using fs
by (simp add: Q_Arrow_strong_inversion)
@@ -592,7 +592,7 @@
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv.strong_inducts)
case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
- have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'"by fact
+ have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'"by fact+
have h2:"\<Gamma> \<subseteq> \<Gamma>'" by fact
have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^isub>1)#\<Gamma> \<subseteq> \<Gamma>'; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact
have "valid \<Gamma>'" by fact
@@ -640,8 +640,8 @@
next
case (3 \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
have "\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2"
- and "\<Gamma> \<subseteq> \<Gamma>'"
- and "valid \<Gamma>'" by fact
+ and "\<Gamma> \<subseteq> \<Gamma>'"
+ and "valid \<Gamma>'" by fact+
then show "\<Gamma>' \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by simp
qed (auto)
@@ -797,7 +797,7 @@
moreover
{
assume "(y,U) \<in> set [(x,T)]"
- then have "\<Gamma>' \<turnstile> (x,s)#\<theta><Var y> is (x,t)#\<theta>'<Var y> : U" by auto
+ with h2 have "\<Gamma>' \<turnstile> (x,s)#\<theta><Var y> is (x,t)#\<theta>'<Var y> : U" by auto
}
moreover
{
@@ -821,7 +821,7 @@
using h1 h2 h3
proof (nominal_induct \<Gamma> t T avoiding: \<Gamma>' \<theta> \<theta>' rule: typing.strong_induct)
case (t_Lam x \<Gamma> T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
- have fs:"x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact
+ have fs:"x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact+
have h:"\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
have ih:"\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
{
@@ -848,14 +848,14 @@
proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<theta> \<theta>' rule: def_equiv.strong_induct)
case (Q_Refl \<Gamma> t T \<Gamma>' \<theta> \<theta>')
have "\<Gamma> \<turnstile> t : T"
- and "valid \<Gamma>'" by fact
+ and "valid \<Gamma>'" by fact+
moreover
have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
ultimately show "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T" using fundamental_theorem_1 by blast
next
case (Q_Symm \<Gamma> t s T \<Gamma>' \<theta> \<theta>')
have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
- and "valid \<Gamma>'" by fact
+ and "valid \<Gamma>'" by fact+
moreover
have ih: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<s> : T" by fact
ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using logical_symmetry by blast
@@ -864,7 +864,7 @@
have ih1: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" by fact
have ih2: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<u> : T" by fact
have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
- and v: "valid \<Gamma>'" by fact
+ and v: "valid \<Gamma>'" by fact+
then have "\<Gamma>' \<turnstile> \<theta>' is \<theta>' over \<Gamma>" using logical_pseudo_reflexivity by auto
then have "\<Gamma>' \<turnstile> \<theta>'<t> is \<theta>'<u> : T" using ih2 v by auto
moreover have "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using ih1 h v by auto
@@ -872,9 +872,9 @@
next
case (Q_Abs x \<Gamma> T\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
have fs:"x\<sharp>\<Gamma>" by fact
- have fs2: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact
+ have fs2: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+
have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
- and h3: "valid \<Gamma>'" by fact
+ and h3: "valid \<Gamma>'" by fact+
have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
{
fix \<Gamma>'' s' t'
@@ -888,7 +888,7 @@
ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<theta><s\<^isub>2>) s' is App (Lam [x].\<theta>'<t\<^isub>2>) t' : T\<^isub>2"
using logical_weak_head_closure by auto
}
- moreover have "valid \<Gamma>'" using h2 by auto
+ moreover have "valid \<Gamma>'" using h3 by auto
ultimately have "\<Gamma>' \<turnstile> Lam [x].\<theta><s\<^isub>2> is Lam [x].\<theta>'<t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
then show "\<Gamma>' \<turnstile> \<theta><Lam [x].s\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs2 by auto
next
@@ -897,9 +897,9 @@
next
case (Q_Beta x \<Gamma> s\<^isub>2 t\<^isub>2 T\<^isub>1 s12 t12 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
- and h': "valid \<Gamma>'" by fact
+ and h': "valid \<Gamma>'" by fact+
have fs: "x\<sharp>\<Gamma>" by fact
- have fs2: " x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact
+ have fs2: " x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+
have ih1: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>1" by fact
have ih2: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s12> is \<theta>'<t12> : T\<^isub>2" by fact
have "\<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>1" using ih1 h' h by auto
@@ -914,8 +914,8 @@
next
case (Q_Ext x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
- and h2': "valid \<Gamma>'" by fact
- have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
+ and h2': "valid \<Gamma>'" by fact+
+ have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact+
have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk>
\<Longrightarrow> \<Gamma>' \<turnstile> \<theta><App s (Var x)> is \<theta>'<App t (Var x)> : T\<^isub>2" by fact
{
@@ -930,7 +930,7 @@
then have "\<Gamma>'' \<turnstile> App ((x,s')#\<theta><s>) s' is App ((x,t')#\<theta>'<t>) t' : T\<^isub>2" by auto
then have "\<Gamma>'' \<turnstile> App (\<theta><s>) s' is App (\<theta>'<t>) t' : T\<^isub>2" using fs fresh_psubst_simp by auto
}
- moreover have "valid \<Gamma>'" using h2 by auto
+ moreover have "valid \<Gamma>'" using h2' by auto
ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
next
case (Q_Unit \<Gamma> s t \<Gamma>' \<theta> \<theta>')
--- a/src/HOL/Nominal/Examples/Fsub.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Thu Jun 14 23:04:36 2007 +0200
@@ -599,7 +599,7 @@
hence rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
hence T_inst: "T = Top" by (simp add: S_TopE)
have "\<turnstile> \<Gamma> ok"
- and "S closed_in \<Gamma>" by fact
+ and "S closed_in \<Gamma>" by fact+
hence "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of.S_Top)
thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp
next
@@ -724,13 +724,13 @@
{ --{* The transitivity proof is now by the auxiliary lemma. *}
case 1
have "\<Gamma> \<turnstile> S <: Q"
- and "\<Gamma> \<turnstile> Q <: T" by fact
+ and "\<Gamma> \<turnstile> Q <: T" by fact+
thus "\<Gamma> \<turnstile> S <: T" by (rule transitivity_aux)
next
--{* The narrowing proof proceeds by an induction over @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N"}. *}
case 2
have "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N" --{* left-hand derivation *}
- and "\<Gamma> \<turnstile> P<:Q" by fact --{* right-hand derivation *}
+ and "\<Gamma> \<turnstile> P<:Q" by fact+ --{* right-hand derivation *}
thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> M <: N"
proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(X,Q)]@\<Gamma>" M N avoiding: \<Delta> \<Gamma> X rule: subtype_of.strong_induct)
case (S_Top _ S \<Delta> \<Gamma> X)
--- a/src/HOL/Nominal/Examples/Height.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy Thu Jun 14 23:04:36 2007 +0200
@@ -64,7 +64,7 @@
case (Lam y e1)
hence ih: "height (e1[x::=e']) \<le> (((height e1) - 1) + (height e'))" by simp
moreover
- have vc: "y\<sharp>x" "y\<sharp>e'" by fact (* usual variable convention *)
+ have vc: "y\<sharp>x" "y\<sharp>e'" by fact+ (* usual variable convention *)
ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp
next
case (App e1 e2)
@@ -74,4 +74,3 @@
qed
end
-
--- a/src/HOL/Nominal/Examples/SN.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy Thu Jun 14 23:04:36 2007 +0200
@@ -374,7 +374,7 @@
proof (induct a rule: acc.induct)
case (accI x)
note accI' = accI
- have "acc r b" .
+ have "acc r b" by fact
thus ?case
proof (induct b rule: acc.induct)
case (accI y)
@@ -501,7 +501,7 @@
case (t3 a \<Gamma> \<sigma> t \<tau> \<theta>) --"lambda case"
have ih: "\<And>\<theta>. \<theta> closes ((a,\<sigma>)#\<Gamma>) \<Longrightarrow> \<theta><t> \<in> RED \<tau>" by fact
have \<theta>_cond: "\<theta> closes \<Gamma>" by fact
- have fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" by fact
+ have fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" by fact+
from ih have "\<forall>s\<in>RED \<sigma>. ((a,s)#\<theta>)<t> \<in> RED \<tau>"
using fresh \<theta>_cond fresh_context by simp
then have "\<forall>s\<in>RED \<sigma>. \<theta><t>[a::=s] \<in> RED \<tau>"
--- a/src/HOL/Nominal/Examples/SOS.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy Thu Jun 14 23:04:36 2007 +0200
@@ -327,7 +327,7 @@
and "(x\<^isub>1, Data \<sigma>\<^isub>1)#\<Gamma> \<turnstile> e\<^isub>1 : T"
and "(x\<^isub>2, Data \<sigma>\<^isub>2)#\<Gamma> \<turnstile> e\<^isub>2 : T"
proof -
- have f:"x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" by fact
+ have f:"x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" by fact+
have "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T" by fact
then obtain \<sigma>\<^isub>1 \<sigma>\<^isub>2 x\<^isub>1' x\<^isub>2' e\<^isub>1' e\<^isub>2' where
h:"\<Gamma> \<turnstile> e : Data (DSum \<sigma>\<^isub>1 \<sigma>\<^isub>2)" and
@@ -382,8 +382,8 @@
then have ih\<^isub>1: "valid ((x\<^isub>1,Data S\<^isub>1)#\<Gamma>\<^isub>2) \<Longrightarrow> (x\<^isub>1,Data S\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>1 : T"
and ih\<^isub>2: "valid ((x\<^isub>2,Data S\<^isub>2)#\<Gamma>\<^isub>2) \<Longrightarrow> (x\<^isub>2,Data S\<^isub>2)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>2 : T"
and ih\<^isub>3: "\<Gamma>\<^isub>2 \<turnstile> e : Data (DSum S\<^isub>1 S\<^isub>2)" by auto
- have fs\<^isub>1: "x\<^isub>1\<sharp>\<Gamma>\<^isub>2" "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>e\<^isub>2" "x\<^isub>1\<sharp>x\<^isub>2" by fact
- have fs\<^isub>2: "x\<^isub>2\<sharp>\<Gamma>\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>e\<^isub>1" "x\<^isub>2\<sharp>x\<^isub>1" by fact
+ have fs\<^isub>1: "x\<^isub>1\<sharp>\<Gamma>\<^isub>2" "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>e\<^isub>2" "x\<^isub>1\<sharp>x\<^isub>2" by fact+
+ have fs\<^isub>2: "x\<^isub>2\<sharp>\<Gamma>\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>e\<^isub>1" "x\<^isub>2\<sharp>x\<^isub>1" by fact+
have "valid \<Gamma>\<^isub>2" by fact
then have "valid ((x\<^isub>1,Data S\<^isub>1)#\<Gamma>\<^isub>2)" and "valid ((x\<^isub>2,Data S\<^isub>2)#\<Gamma>\<^isub>2)" using fs\<^isub>1 fs\<^isub>2 by auto
then have "(x\<^isub>1, Data S\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>1 : T" and "(x\<^isub>2, Data S\<^isub>2)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>2 : T" using ih\<^isub>1 ih\<^isub>2 by simp_all
@@ -439,7 +439,7 @@
qed
next
case (Lam y t \<Gamma> e' x T)
- have vc: "y\<sharp>\<Gamma>" "y\<sharp>x" "y\<sharp>e'" by fact
+ have vc: "y\<sharp>\<Gamma>" "y\<sharp>x" "y\<sharp>e'" by fact+
have pr1: "\<Gamma> \<turnstile> e' : T'" by fact
have pr2: "(x,T')#\<Gamma> \<turnstile> Lam [y].t : T" by fact
then obtain T\<^isub>1 T\<^isub>2 where pr2': "(y,T\<^isub>1)#(x,T')#\<Gamma> \<turnstile> t : T\<^isub>2" and eq: "T = T\<^isub>1\<rightarrow>T\<^isub>2"
@@ -455,7 +455,7 @@
next
case (Case t\<^isub>1 x\<^isub>1 t\<^isub>2 x\<^isub>2 t3 \<Gamma> e' x T)
have vc: "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>1\<sharp>e'" "x\<^isub>1\<sharp>x""x\<^isub>1\<sharp>t\<^isub>1" "x\<^isub>1\<sharp>t3" "x\<^isub>2\<sharp>\<Gamma>"
- "x\<^isub>2\<sharp>e'" "x\<^isub>2\<sharp>x" "x\<^isub>2\<sharp>t\<^isub>1" "x\<^isub>2\<sharp>t\<^isub>2" "x\<^isub>2\<noteq>x\<^isub>1" by fact
+ "x\<^isub>2\<sharp>e'" "x\<^isub>2\<sharp>x" "x\<^isub>2\<sharp>t\<^isub>1" "x\<^isub>2\<sharp>t\<^isub>2" "x\<^isub>2\<noteq>x\<^isub>1" by fact+
have as1: "\<Gamma> \<turnstile> e' : T'" by fact
have as2: "(x,T')#\<Gamma> \<turnstile> Case t\<^isub>1 of inl x\<^isub>1 \<rightarrow> t\<^isub>2 | inr x\<^isub>2 \<rightarrow> t3 : T" by fact
then obtain S\<^isub>1 S\<^isub>2 where
@@ -463,10 +463,10 @@
h2:"(x\<^isub>1,Data S\<^isub>1)#(x,T')#\<Gamma> \<turnstile> t\<^isub>2 : T" and
h3:"(x\<^isub>2,Data S\<^isub>2)#(x,T')#\<Gamma> \<turnstile> t3 : T"
using vc by (auto simp add: fresh_list_cons)
- have ih1: "\<lbrakk>(x,T')#\<Gamma> \<turnstile> t\<^isub>1 : T; \<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1[x::=e'] : T"
+ have ih1: "\<lbrakk>(x,T')#\<Gamma> \<turnstile> t\<^isub>1 : Data (DSum S\<^isub>1 S\<^isub>2); \<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1[x::=e'] : Data (DSum S\<^isub>1 S\<^isub>2)"
and ih2: "\<lbrakk>(x,T')#(x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>2:T; (x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> e':T'\<rbrakk> \<Longrightarrow> (x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>2[x::=e']:T"
and ih3: "\<lbrakk>(x,T')#(x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t3:T; (x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> e':T'\<rbrakk> \<Longrightarrow> (x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t3[x::=e']:T"
- by fact
+ by fact+
from h2 have h2': "(x,T')#(x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>2 : T" by (rule context_exchange)
from h3 have h3': "(x,T')#(x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t3 : T" by (rule context_exchange)
have "\<Gamma> \<turnstile> t\<^isub>1[x::=e'] : Data (DSum S\<^isub>1 S\<^isub>2)" using h1 ih1 as1 by simp
@@ -663,7 +663,7 @@
thus "\<Gamma> \<turnstile> e' : T" using ih3 by simp
next
case (b_CaseL x\<^isub>1 e e\<^isub>2 e'' x\<^isub>2 e\<^isub>1 e' \<Gamma>)
- have vc: "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" by fact
+ have vc: "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" by fact+
have "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T" by fact
then obtain S\<^isub>1 S\<^isub>2 e\<^isub>1' e\<^isub>2' where
a1: "\<Gamma> \<turnstile> e : Data (DSum S\<^isub>1 S\<^isub>2)" and
@@ -694,7 +694,7 @@
have ih2:"\<And>t. e\<^isub>2 \<Down> t \<Longrightarrow> e\<^isub>2' = t" by fact
have ih3: "\<And>t. e\<^isub>1'[x::=e\<^isub>2'] \<Down> t \<Longrightarrow> e' = t" by fact
have app: "App e\<^isub>1 e\<^isub>2 \<Down> t\<^isub>2" by fact
- have vc: "x\<sharp>e\<^isub>1" "x\<sharp>e\<^isub>2" by fact
+ have vc: "x\<sharp>e\<^isub>1" "x\<sharp>e\<^isub>2" by fact+
then have "x \<sharp> App e\<^isub>1 e\<^isub>2" by auto
then have vc': "x\<sharp>t\<^isub>2" using fresh_preserved app by blast
from vc vc' obtain f\<^isub>1 f\<^isub>2 where x1: "e\<^isub>1 \<Down> Lam [x]. f\<^isub>1" and x2: "e\<^isub>2 \<Down> f\<^isub>2" and x3: "f\<^isub>1[x::=f\<^isub>2] \<Down> t\<^isub>2"
@@ -708,7 +708,7 @@
thus ?case using ih3 by simp
next
case (b_CaseL x\<^isub>1 e e\<^isub>2 e'' x\<^isub>2 e\<^isub>1 e' t\<^isub>2)
- have fs: "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>t\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>t\<^isub>2" by fact
+ have fs: "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>t\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>t\<^isub>2" by fact+
have ih1:"\<And>t. e \<Down> t \<Longrightarrow> InL e' = t" by fact
have ih2:"\<And>t. e\<^isub>1[x\<^isub>1::=e'] \<Down> t \<Longrightarrow> e'' = t" by fact
have ha: "\<not>(\<exists>t. e \<Down> InR t)" using ih1 by force
@@ -720,7 +720,7 @@
then show "e'' = t\<^isub>2" using ih2 by simp
next
case (b_CaseR x\<^isub>1 e e\<^isub>2 e'' x\<^isub>2 e\<^isub>1 e' t\<^isub>2 )
- have fs: "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>t\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>t\<^isub>2" by fact
+ have fs: "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>t\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>t\<^isub>2" by fact+
have ih1: "\<And>t. e \<Down> t \<Longrightarrow> InR e' = t" by fact
have ih2: "\<And>t. e\<^isub>2[x\<^isub>2::=e'] \<Down> t \<Longrightarrow> e'' = t" by fact
have ha: "\<not>(\<exists>t. e \<Down> InL t)" using ih1 by force
@@ -997,7 +997,7 @@
have ih:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e> \<Down> v \<and> v \<in> V T" by fact
have as\<^isub>1: "\<theta> Vcloses \<Gamma>" by fact
have as\<^isub>2: "\<Gamma> \<turnstile> Lam [x].e : T" by fact
- have fs: "x\<sharp>\<Gamma>" "x\<sharp>\<theta>" by fact
+ have fs: "x\<sharp>\<Gamma>" "x\<sharp>\<theta>" by fact+
from as\<^isub>2 fs obtain T\<^isub>1 T\<^isub>2
where "(i)": "(x,T\<^isub>1)#\<Gamma> \<turnstile> e:T\<^isub>2" and "(ii)": "T = T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
from "(i)" have "(iii)": "valid ((x,T\<^isub>1)#\<Gamma>)" by (simp add: typing_implies_valid)
@@ -1016,7 +1016,7 @@
next
case (Case t' n\<^isub>1 t\<^isub>1 n\<^isub>2 t\<^isub>2 \<Gamma> \<theta> T)
have f: "n\<^isub>1\<sharp>\<Gamma>" "n\<^isub>1\<sharp>\<theta>" "n\<^isub>2\<sharp>\<Gamma>" "n\<^isub>2\<sharp>\<theta>" "n\<^isub>2\<noteq>n\<^isub>1" "n\<^isub>1\<sharp>t'"
- "n\<^isub>1\<sharp>t\<^isub>2" "n\<^isub>2\<sharp>t'" "n\<^isub>2\<sharp>t\<^isub>1" by fact
+ "n\<^isub>1\<sharp>t\<^isub>2" "n\<^isub>2\<sharp>t'" "n\<^isub>2\<sharp>t\<^isub>1" by fact+
have h:"\<theta> Vcloses \<Gamma>" by fact
have th:"\<Gamma> \<turnstile> Case t' of inl n\<^isub>1 \<rightarrow> t\<^isub>1 | inr n\<^isub>2 \<rightarrow> t\<^isub>2 : T" by fact
then obtain S\<^isub>1 S\<^isub>2 where
--- a/src/HOL/Nominal/Nominal.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Thu Jun 14 23:04:36 2007 +0200
@@ -1715,7 +1715,7 @@
and at: "at TYPE('x)"
shows "pi2\<bullet>(pi1\<bullet>x) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>x)"
proof -
- have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
+ have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8 [OF at])
hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
thus ?thesis by (simp add: pt2[OF pt])
qed
@@ -2543,7 +2543,7 @@
proof -
have ptd: "pt TYPE('y) TYPE('y)" by (simp add: at_pt_inst[OF at'])
have ptc: "pt TYPE('y\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at])
- have cpc: "cp TYPE('y\<Rightarrow>'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb,OF cpa])
+ have cpc: "cp TYPE('y\<Rightarrow>'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb cpa ptb at])
have f2: "finite ((supp (pi\<bullet>h))::'y set)"
proof -
from f1 have "finite (pi\<bullet>((supp h)::'y set))"
@@ -3077,7 +3077,7 @@
and at: "at TYPE('x)"
shows "pi2\<bullet>(pi1\<bullet>x) = perm_aux (pi2\<bullet>pi1) (pi2\<bullet>x)"
proof -
- have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
+ have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8[OF at])
hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
thus ?thesis by (simp add: pt2[OF pt] perm_aux_def)
qed