--- a/src/HOL/Bali/AxCompl.thy Sat May 17 15:31:42 2008 +0200
+++ b/src/HOL/Bali/AxCompl.thy Sat May 17 21:46:22 2008 +0200
@@ -970,7 +970,7 @@
fix l show "abrupt s2 \<noteq> Some (Jump (Break l)) \<and>
abrupt s2 \<noteq> Some (Jump (Cont l))"
proof -
- from clsD have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
+ fix accC from clsD have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
by auto
from eval_init wf
have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
--- a/src/HOL/Bali/Evaln.thy Sat May 17 15:31:42 2008 +0200
+++ b/src/HOL/Bali/Evaln.thy Sat May 17 21:46:22 2008 +0200
@@ -582,7 +582,7 @@
then show ?case ..
next
case (Jmp s j)
- have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
+ fix n have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
by (rule evaln.Jmp)
then show ?case ..
next
@@ -681,7 +681,7 @@
then show ?case ..
next
case (Lit s v)
- have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
+ fix n have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
by (rule evaln.Lit)
then show ?case ..
next
@@ -705,7 +705,7 @@
then show ?case ..
next
case (Super s )
- have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
+ fix n have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
by (rule evaln.Super)
then show ?case ..
next
@@ -830,5 +830,5 @@
by (blast intro!: evaln.Cons dest: evaln_max2)
then show ?case ..
qed
-
+
end
--- a/src/HOL/Complex/ex/MIR.thy Sat May 17 15:31:42 2008 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Sat May 17 21:46:22 2008 +0200
@@ -1519,7 +1519,7 @@
using partition_set[OF part] by auto
finally have "Ifm bs p = ((Ifm bs ?cyes) \<and> (Ifm bs ?cno))" using list_conj by simp}
hence "Ifm bs (E p) = (\<exists>x. (Ifm (x#bs) ?cyes) \<and> (Ifm (x#bs) ?cno))" by simp
- also have "\<dots> = (\<exists>x. (Ifm (y#bs) ?cyes) \<and> (Ifm (x#bs) ?cno))"
+ also fix y have "\<dots> = (\<exists>x. (Ifm (y#bs) ?cyes) \<and> (Ifm (x#bs) ?cno))"
using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
also have "\<dots> = (Ifm bs (decr ?cyes) \<and> Ifm bs (E ?cno))"
by (auto simp add: decr[OF yes_nb])
@@ -2170,6 +2170,7 @@
case (3 c e)
from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
from prems have nbe: "numbound0 e" by simp
+ fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Eq (CN 0 c e))) = ?I x (Eq (CN 0 c e))"
proof (simp add: less_floor_eq , rule allI, rule impI)
fix x
@@ -2186,6 +2187,7 @@
case (4 c e)
from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
from prems have nbe: "numbound0 e" by simp
+ fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (NEq (CN 0 c e))) = ?I x (NEq (CN 0 c e))"
proof (simp add: less_floor_eq , rule allI, rule impI)
fix x
@@ -2202,6 +2204,7 @@
case (5 c e)
from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
from prems have nbe: "numbound0 e" by simp
+ fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Lt (CN 0 c e))) = ?I x (Lt (CN 0 c e))"
proof (simp add: less_floor_eq , rule allI, rule impI)
fix x
@@ -2217,6 +2220,7 @@
case (6 c e)
from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
from prems have nbe: "numbound0 e" by simp
+ fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Le (CN 0 c e))) = ?I x (Le (CN 0 c e))"
proof (simp add: less_floor_eq , rule allI, rule impI)
fix x
@@ -2232,6 +2236,7 @@
case (7 c e)
from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
from prems have nbe: "numbound0 e" by simp
+ fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Gt (CN 0 c e))) = ?I x (Gt (CN 0 c e))"
proof (simp add: less_floor_eq , rule allI, rule impI)
fix x
@@ -2247,6 +2252,7 @@
case (8 c e)
from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
from prems have nbe: "numbound0 e" by simp
+ fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Ge (CN 0 c e))) = ?I x (Ge (CN 0 c e))"
proof (simp add: less_floor_eq , rule allI, rule impI)
fix x
@@ -2642,7 +2648,7 @@
by simp
hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)" by simp
also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: ring_simps)
- also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"
+ also fix k have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"
using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp
also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp
finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def be isint_Mul[OF ei] mult_strict_mono[OF ldcp jp ldcp ] by simp
@@ -2659,7 +2665,7 @@
by simp
hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)" by simp
also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: ring_simps)
- also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"
+ also fix k have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"
using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp
also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp
finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def be isint_Mul[OF ei] mult_strict_mono[OF ldcp jp ldcp ] by simp
@@ -4363,6 +4369,7 @@
case (3 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4379,6 +4386,7 @@
case (4 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4395,6 +4403,7 @@
case (5 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4410,6 +4419,7 @@
case (6 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4425,6 +4435,7 @@
case (7 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4440,6 +4451,7 @@
case (8 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4465,6 +4477,7 @@
case (3 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4481,6 +4494,7 @@
case (4 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4497,6 +4511,7 @@
case (5 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4512,6 +4527,7 @@
case (6 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4527,6 +4543,7 @@
case (7 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -4542,6 +4559,7 @@
case (8 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Sat May 17 15:31:42 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Sat May 17 21:46:22 2008 +0200
@@ -1119,6 +1119,7 @@
case (3 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1135,6 +1136,7 @@
case (4 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1151,6 +1153,7 @@
case (5 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1166,6 +1169,7 @@
case (6 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1181,6 +1185,7 @@
case (7 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1196,6 +1201,7 @@
case (8 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1221,6 +1227,7 @@
case (3 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1237,6 +1244,7 @@
case (4 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1253,6 +1261,7 @@
case (5 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1268,6 +1277,7 @@
case (6 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1283,6 +1293,7 @@
case (7 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1298,6 +1309,7 @@
case (8 c e)
from prems have nb: "numbound0 e" by simp
from prems have cp: "real c > 0" by simp
+ fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
{fix x
@@ -1892,6 +1904,7 @@
(is "_ \<and> (?rhs = ?lhs)")
proof-
let ?I = "\<lambda> x p. Ifm (x#bs) p"
+ fix x
let ?N = "\<lambda> t. Inum (x#bs) t"
let ?q = "rlfm (simpfm p)"
let ?U = "uset ?q"
--- a/src/HOL/Library/Heap.thy Sat May 17 15:31:42 2008 +0200
+++ b/src/HOL/Library/Heap.thy Sat May 17 21:46:22 2008 +0200
@@ -54,8 +54,9 @@
termination by (relation "measure (\<lambda>x. size x)")
(simp, simp only: in_measure rtype_size)
-instance proof (rule countable_classI)
- fix t t' :: rtype
+instance
+proof (rule countable_classI)
+ fix t t' :: rtype and ts
have "(\<forall>t'. to_nat_rtype t = to_nat_rtype t' \<longrightarrow> t = t')
\<and> (\<forall>ts'. map to_nat_rtype ts = map to_nat_rtype ts' \<longrightarrow> ts = ts')"
proof (induct rule: rtype.induct)
--- a/src/HOL/Nominal/Examples/Class.thy Sat May 17 15:31:42 2008 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy Sat May 17 21:46:22 2008 +0200
@@ -20786,9 +20786,9 @@
assumes a: "\<Gamma> \<turnstile> M \<turnstile> \<Delta>"
shows "SNa M"
proof -
- have "(idc \<Delta> x) ccloses \<Delta>" by (simp add: ccloses_id)
+ fix x have "(idc \<Delta> x) ccloses \<Delta>" by (simp add: ccloses_id)
moreover
- have "(idn \<Gamma> a) ncloses \<Gamma>" by (simp add: ncloses_id)
+ fix a have "(idn \<Gamma> a) ncloses \<Gamma>" by (simp add: ncloses_id)
ultimately have "SNa ((idn \<Gamma> a),(idc \<Delta> x)<M>)" using a by (simp add: all_CAND)
moreover
have "((idn \<Gamma> a),(idc \<Delta> x)<M>) \<longrightarrow>\<^isub>a* M" by (simp add: id_redu)
--- a/src/HOL/Nominal/Examples/SN.thy Sat May 17 15:31:42 2008 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy Sat May 17 21:46:22 2008 +0200
@@ -374,7 +374,7 @@
then have a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2" by simp
from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_implies_CR4)
moreover
- have "NEUT (Var a)" by (force simp add: NEUT_def)
+ fix a have "NEUT (Var a)" by (force simp add: NEUT_def)
moreover
have "NORMAL (Var a)" by (rule NORMAL_Var)
ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def)
--- a/src/HOL/Nominal/Examples/VC_Condition.thy Sat May 17 15:31:42 2008 +0200
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy Sat May 17 21:46:22 2008 +0200
@@ -129,6 +129,7 @@
lemma false1:
shows "False"
proof -
+ fix x
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)
@@ -176,6 +177,7 @@
lemma false2:
shows "False"
proof -
+ fix x
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)
@@ -189,6 +191,7 @@
lemma false3:
shows "False"
proof -
+ fix x
have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros)
moreover obtain y::"name" where fc: "y\<sharp>x" by (rule exists_fresh) (rule fin_supp)
then have "Lam [x].(Var x) = Lam [y].(Var y)"
--- a/src/HOL/ex/Records.thy Sat May 17 15:31:42 2008 +0200
+++ b/src/HOL/ex/Records.thy Sat May 17 21:46:22 2008 +0200
@@ -310,7 +310,7 @@
lemma True
proof -
{
- fix r
+ fix P r
assume pre: "P (xpos r)"
have "\<exists>x. P x"
using pre