# 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 \ Some (Jump (Break l)) \ abrupt s2 \ Some (Jump (Cont l))" proof - - from clsD have wt_init: "\prg=G, cls=accC, lcl=L\\(Init D)\\" + fix accC from clsD have wt_init: "\prg=G, cls=accC, lcl=L\\(Init D)\\" by auto from eval_init wf have s1_no_jmp: "\ j. abrupt s1 \ 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\Norm s \Jmp j\n\ (Some (Jump j), s)" + fix n have "G\Norm s \Jmp j\n\ (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\Norm s \Lit v-\v\n\ Norm s" + fix n have "G\Norm s \Lit v-\v\n\ Norm s" by (rule evaln.Lit) then show ?case .. next @@ -705,7 +705,7 @@ then show ?case .. next case (Super s ) - have "G\Norm s \Super-\val_this s\n\ Norm s" + fix n have "G\Norm s \Super-\val_this s\n\ 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) \ (Ifm bs ?cno))" using list_conj by simp} hence "Ifm bs (E p) = (\x. (Ifm (x#bs) ?cyes) \ (Ifm (x#bs) ?cno))" by simp - also have "\ = (\x. (Ifm (y#bs) ?cyes) \ (Ifm (x#bs) ?cno))" + also fix y have "\ = (\x. (Ifm (y#bs) ?cyes) \ (Ifm (x#bs) ?cno))" using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast also have "\ = (Ifm bs (decr ?cyes) \ 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 "\ 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 "\ 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 "\ 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 "\ 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 "\ 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 "\ 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 "(\ (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\ (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 "\ = (\ (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 "\ = (\ (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)" + also fix k have "\ = (\ (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 "\ = (\ (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 "(\ (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\ (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 "\ = (\ (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 "\ = (\ (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)" + also fix k have "\ = (\ (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 "\ = (\ (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 "_ \ (?rhs = ?lhs)") proof- let ?I = "\ x p. Ifm (x#bs) p" + fix x let ?N = "\ 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 (\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 "(\t'. to_nat_rtype t = to_nat_rtype t' \ t = t') \ (\ts'. map to_nat_rtype ts = map to_nat_rtype ts' \ 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: "\ \ M \ \" shows "SNa M" proof - - have "(idc \ x) ccloses \" by (simp add: ccloses_id) + fix x have "(idc \ x) ccloses \" by (simp add: ccloses_id) moreover - have "(idn \ a) ncloses \" by (simp add: ncloses_id) + fix a have "(idn \ a) ncloses \" by (simp add: ncloses_id) ultimately have "SNa ((idn \ a),(idc \ x))" using a by (simp add: all_CAND) moreover have "((idn \ a),(idc \ x)) \\<^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: "\u. u \ RED \1 \ App t u \ RED \2" by simp from ih_CR3_\1 have "CR4 \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)\ RED \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)\[x,x],(Var x)" and "\(x\Var x)" by (simp_all add: unbind_lambda_lambda1 fresh_atm) then have "\(x\(bind [x] (Var x)))" by (rule faulty1) @@ -176,6 +177,7 @@ lemma false2: shows "False" proof - + fix x have "Lam [x].(Var x) \ (Var x)" by (auto intro: strip.intros) moreover have "x\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) \ (Var x)" by (auto intro: strip.intros) moreover obtain y::"name" where fc: "y\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 "\x. P x" using pre