# HG changeset patch
# User wenzelm
# Date 1211053582 -7200
# Node ID c398a386608219a5db2b3a50463b5d24558bb116
# Parent  aa226d8405a88f9bc83204de3feb23aa3a5792fc
avoid undeclared variables within proofs;

diff -r aa226d8405a8 -r c398a3866082 src/HOL/Bali/AxCompl.thy
--- 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)"
diff -r aa226d8405a8 -r c398a3866082 src/HOL/Bali/Evaln.thy
--- 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
diff -r aa226d8405a8 -r c398a3866082 src/HOL/Complex/ex/MIR.thy
--- 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
diff -r aa226d8405a8 -r c398a3866082 src/HOL/Complex/ex/ReflectedFerrack.thy
--- 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"
diff -r aa226d8405a8 -r c398a3866082 src/HOL/Library/Heap.thy
--- 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)
diff -r aa226d8405a8 -r c398a3866082 src/HOL/Nominal/Examples/Class.thy
--- 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)
diff -r aa226d8405a8 -r c398a3866082 src/HOL/Nominal/Examples/SN.thy
--- 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)
diff -r aa226d8405a8 -r c398a3866082 src/HOL/Nominal/Examples/VC_Condition.thy
--- 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)"
diff -r aa226d8405a8 -r c398a3866082 src/HOL/ex/Records.thy
--- 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