--- a/src/HOL/Finite_Set.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/HOL/Finite_Set.thy Tue Mar 13 14:44:27 2012 +0100
@@ -22,7 +22,8 @@
assumes "P {}"
and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
shows "P F"
-using `finite F` proof induct
+using `finite F`
+proof induct
show "P {}" by fact
fix x F assume F: "finite F" and P: "P F"
show "P (insert x F)"
@@ -68,7 +69,8 @@
lemma finite_imp_nat_seg_image_inj_on:
assumes "finite A"
shows "\<exists>(n::nat) f. A = f ` {i. i < n} \<and> inj_on f {i. i < n}"
-using assms proof induct
+using assms
+proof induct
case empty
show ?case
proof
@@ -248,7 +250,8 @@
lemma finite_imageD:
assumes "finite (f ` A)" and "inj_on f A"
shows "finite A"
-using assms proof (induct "f ` A" arbitrary: A)
+using assms
+proof (induct "f ` A" arbitrary: A)
case empty then show ?case by simp
next
case (insert x B)
@@ -272,7 +275,8 @@
lemma finite_subset_image:
assumes "finite B"
shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
-using assms proof induct
+using assms
+proof induct
case empty then show ?case by simp
next
case insert then show ?case
@@ -413,7 +417,8 @@
assumes "\<And>x. P {x}"
and "\<And>x F. finite F \<Longrightarrow> F \<noteq> {} \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
shows "P F"
-using assms proof induct
+using assms
+proof induct
case empty then show ?case by simp
next
case (insert x F) then show ?case by cases auto
@@ -424,7 +429,8 @@
assumes empty: "P {}"
and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)"
shows "P F"
-using `finite F` `F \<subseteq> A` proof induct
+using `finite F` `F \<subseteq> A`
+proof induct
show "P {}" by fact
next
fix x F
@@ -486,8 +492,8 @@
end
-instance prod :: (finite, finite) finite proof
-qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
+instance prod :: (finite, finite) finite
+ by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
lemma inj_graph: "inj (%f. {(x, y). y = f x})"
by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
@@ -506,24 +512,24 @@
qed
qed
-instance bool :: finite proof
-qed (simp add: UNIV_bool)
+instance bool :: finite
+ by default (simp add: UNIV_bool)
instance set :: (finite) finite
by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
-instance unit :: finite proof
-qed (simp add: UNIV_unit)
+instance unit :: finite
+ by default (simp add: UNIV_unit)
-instance sum :: (finite, finite) finite proof
-qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
+instance sum :: (finite, finite) finite
+ by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
lemma finite_option_UNIV [simp]:
"finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
-instance option :: (finite) finite proof
-qed (simp add: UNIV_option_conv)
+instance option :: (finite) finite
+ by default (simp add: UNIV_option_conv)
subsection {* A basic fold functional for finite sets *}
@@ -830,9 +836,9 @@
assumes "finite A" and "a \<notin> A"
shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
proof -
- interpret comp_fun_commute "%x y. (g x) * y" proof
- qed (simp add: fun_eq_iff mult_ac)
- show ?thesis using assms by (simp add: fold_image_def)
+ interpret comp_fun_commute "%x y. (g x) * y"
+ by default (simp add: fun_eq_iff mult_ac)
+ from assms show ?thesis by (simp add: fold_image_def)
qed
lemma fold_image_reindex:
@@ -1018,8 +1024,8 @@
context ab_semigroup_mult
begin
-lemma comp_fun_commute: "comp_fun_commute (op *)" proof
-qed (simp add: fun_eq_iff mult_ac)
+lemma comp_fun_commute: "comp_fun_commute (op *)"
+ by default (simp add: fun_eq_iff mult_ac)
lemma fold_graph_insert_swap:
assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
@@ -1104,8 +1110,8 @@
context ab_semigroup_idem_mult
begin
-lemma comp_fun_idem: "comp_fun_idem (op *)" proof
-qed (simp_all add: fun_eq_iff mult_left_commute)
+lemma comp_fun_idem: "comp_fun_idem (op *)"
+ by default (simp_all add: fun_eq_iff mult_left_commute)
lemma fold1_insert_idem [simp]:
assumes nonempty: "A \<noteq> {}" and A: "finite A"
@@ -1137,7 +1143,8 @@
lemma hom_fold1_commute:
assumes hom: "!!x y. h (x * y) = h x * h y"
and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
-using N proof (induct rule: finite_ne_induct)
+using N
+proof (induct rule: finite_ne_induct)
case singleton thus ?case by simp
next
case (insert n N)
@@ -1293,8 +1300,8 @@
assumes "finite A" and "x \<notin> A"
shows "F (insert x A) = F A \<circ> f x"
proof -
- interpret comp_fun_commute f proof
- qed (insert comp_fun_commute, simp add: fun_eq_iff)
+ interpret comp_fun_commute f
+ by default (insert comp_fun_commute, simp add: fun_eq_iff)
from fold_insert2 assms
have "\<And>s. fold f s (insert x A) = fold f (f x s) A" .
with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
@@ -1426,9 +1433,9 @@
assumes "finite A" and "x \<notin> A"
shows "F (insert x A) = g x * F A"
proof -
- interpret comp_fun_commute "%x y. (g x) * y" proof
- qed (simp add: ac_simps fun_eq_iff)
- with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
+ interpret comp_fun_commute "%x y. (g x) * y"
+ by default (simp add: ac_simps fun_eq_iff)
+ from assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
by (simp add: fold_image_def)
with `finite A` show ?thesis by (simp add: eq_fold_g)
qed
@@ -1650,8 +1657,8 @@
assumes "finite A" and "x \<notin> A"
shows "F (insert x A) = fold (op *) x A"
proof -
- interpret ab_semigroup_mult "op *" proof qed (simp_all add: ac_simps)
- with assms show ?thesis by (simp add: eq_fold fold1_eq_fold)
+ interpret ab_semigroup_mult "op *" by default (simp_all add: ac_simps)
+ from assms show ?thesis by (simp add: eq_fold fold1_eq_fold)
qed
lemma insert [simp]:
@@ -1756,8 +1763,8 @@
assumes "finite A"
shows "F (insert a A) = fold (op *) a A"
proof -
- interpret ab_semigroup_idem_mult "op *" proof qed (simp_all add: ac_simps)
- with assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem)
+ interpret ab_semigroup_idem_mult "op *" by default (simp_all add: ac_simps)
+ from assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem)
qed
lemma insert_idem [simp]:
--- a/src/HOL/HOLCF/Tools/fixrec.ML Tue Mar 13 12:04:07 2012 +0000
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Tue Mar 13 14:44:27 2012 +0100
@@ -253,7 +253,9 @@
^ ML_Syntax.print_term pat)
fun strip_alls t =
- if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t
+ (case try Logic.dest_all t of
+ SOME (_, u) => strip_alls u
+ | NONE => t)
fun compile_eq match_name eq =
let
@@ -293,9 +295,7 @@
let
val tab = FixrecUnfoldData.get (Context.Proof ctxt)
val ss = Simplifier.simpset_of ctxt
- fun concl t =
- if Logic.is_all t then concl (snd (Logic.dest_all t))
- else HOLogic.dest_Trueprop (Logic.strip_imp_concl t)
+ val concl = HOLogic.dest_Trueprop o Logic.strip_imp_concl o strip_alls
fun tac (t, i) =
let
val (c, _) =
--- a/src/HOL/List.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/HOL/List.thy Tue Mar 13 14:44:27 2012 +0100
@@ -4483,7 +4483,8 @@
shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
proof -
interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
- with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
+ from assms show ?thesis
+ by (simp add: sorted_list_of_set_def fold_insert_remove)
qed
lemma sorted_list_of_set [simp]:
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Mar 13 14:44:27 2012 +0100
@@ -1689,7 +1689,7 @@
proof
assume ?l guess f' using `?l`[unfolded differentiable_def] .. note f' = this
then interpret bounded_linear f' by auto
- thus ?r unfolding vector_derivative_def has_vector_derivative_def
+ show ?r unfolding vector_derivative_def has_vector_derivative_def
apply-apply(rule someI_ex,rule_tac x="f' 1" in exI)
using f' unfolding scaleR[THEN sym] by auto
next
--- a/src/HOL/Probability/Binary_Product_Measure.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Mar 13 14:44:27 2012 +0100
@@ -197,7 +197,7 @@
next
fix A assume "A \<in> sets (M2 \<Otimes>\<^isub>M M1)"
interpret Q: pair_sigma_algebra M2 M1 by default
- with Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets (M2 \<Otimes>\<^isub>M M1)`]
+ from Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets (M2 \<Otimes>\<^isub>M M1)`]
show "?f -` A \<inter> space ?P \<in> sets ?P" by simp
qed
@@ -221,7 +221,7 @@
assumes Q: "Q \<in> sets P" shows "(\<lambda>x. (x, y)) -` Q \<in> sets M1" (is "?cut Q \<in> sets M1")
proof -
interpret Q: pair_sigma_algebra M2 M1 by default
- with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]
+ from Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]
show ?thesis by (simp add: vimage_compose[symmetric] comp_def)
qed
--- a/src/HOL/Probability/Finite_Product_Measure.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Mar 13 14:44:27 2012 +0100
@@ -858,7 +858,7 @@
using assms proof induct
case empty
interpret finite_product_sigma_finite M "{}" by default auto
- then show ?case by simp
+ show ?case by simp
next
case (insert i I)
note `finite I`[intro, simp]
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Mar 13 14:44:27 2012 +0100
@@ -502,7 +502,7 @@
fix A assume "A \<in> sets ?G"
with generatorE guess J X . note JX = this
interpret JK: finite_product_prob_space M J by default fact+
- with JX show "\<mu>G A \<noteq> \<infinity>" by simp
+ from JX show "\<mu>G A \<noteq> \<infinity>" by simp
next
fix A assume A: "range A \<subseteq> sets ?G" "decseq A" "(\<Inter>i. A i) = {}"
then have "decseq (\<lambda>i. \<mu>G (A i))"
--- a/src/HOL/Probability/Probability_Measure.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/HOL/Probability/Probability_Measure.thy Tue Mar 13 14:44:27 2012 +0100
@@ -622,7 +622,7 @@
assumes "finite_random_variable M' X" shows "random_variable M' X"
proof -
interpret M': finite_sigma_algebra M' using assms by simp
- then show "random_variable M' X" using assms by simp default
+ show "random_variable M' X" using assms by simp default
qed
lemma (in prob_space) distribution_finite_prob_space:
--- a/src/Pure/General/binding.ML Tue Mar 13 12:04:07 2012 +0000
+++ b/src/Pure/General/binding.ML Tue Mar 13 14:44:27 2012 +0100
@@ -122,9 +122,11 @@
(* print *)
fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
- Pretty.markup (Position.markup pos Isabelle_Markup.binding)
- [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
- |> Pretty.quote;
+ if name = "" then Pretty.str "\"\""
+ else
+ Pretty.markup (Position.markup pos Isabelle_Markup.binding)
+ [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
+ |> Pretty.quote;
val print = Pretty.str_of o pretty;
--- a/src/Pure/General/pretty.ML Tue Mar 13 12:04:07 2012 +0000
+++ b/src/Pure/General/pretty.ML Tue Mar 13 14:44:27 2012 +0100
@@ -78,7 +78,10 @@
val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
in
fun add_mode name indent =
- Synchronized.change modes (Symtab.update_new (name, {indent = indent}));
+ Synchronized.change modes (fn tab =>
+ (if not (Symtab.defined tab name) then ()
+ else warning ("Redefining pretty mode " ^ quote name);
+ Symtab.update (name, {indent = indent}) tab));
fun get_mode () =
the_default default
(Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
--- a/src/Pure/Isar/element.ML Tue Mar 13 12:04:07 2012 +0000
+++ b/src/Pure/Isar/element.ML Tue Mar 13 14:44:27 2012 +0100
@@ -278,8 +278,9 @@
fun gen_witness_proof proof after_qed wit_propss eq_props =
let
- val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss
- @ [map (rpair []) eq_props];
+ val propss =
+ (map o map) (fn prop => (mark_witness prop, [])) wit_propss @
+ [map (rpair []) eq_props];
fun after_qed' thmss =
let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
@@ -287,8 +288,8 @@
fun proof_local cmd goal_ctxt int after_qed' propss =
Proof.map_context (K goal_ctxt) #>
- Proof.local_goal (Proof_Display.print_results Isabelle_Markup.state int) (K I)
- Proof_Context.bind_propp_i cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
+ Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp_i cmd NONE
+ after_qed' (map (pair Thm.empty_binding) propss);
in
--- a/src/Pure/Isar/expression.ML Tue Mar 13 12:04:07 2012 +0000
+++ b/src/Pure/Isar/expression.ML Tue Mar 13 14:44:27 2012 +0100
@@ -858,7 +858,8 @@
fun after_qed witss eqns =
(Proof.map_context o Context.proof_map)
- (note_eqns_register deps witss attrss eqns export export');
+ (note_eqns_register deps witss attrss eqns export export')
+ #> Proof.put_facts NONE;
in
state
|> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
--- a/src/Pure/PIDE/markup.ML Tue Mar 13 12:04:07 2012 +0000
+++ b/src/Pure/PIDE/markup.ML Tue Mar 13 14:44:27 2012 +0100
@@ -74,7 +74,10 @@
val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
in
fun add_mode name output =
- Synchronized.change modes (Symtab.update_new (name, {output = output}));
+ Synchronized.change modes (fn tab =>
+ (if not (Symtab.defined tab name) then ()
+ else warning ("Redefining markup mode " ^ quote name);
+ Symtab.update (name, {output = output}) tab));
fun get_mode () =
the_default default
(Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
--- a/src/ZF/Induct/Binary_Trees.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/ZF/Induct/Binary_Trees.thy Tue Mar 13 14:44:27 2012 +0100
@@ -123,10 +123,10 @@
*}
lemma n_leaves_reflect: "t \<in> bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"
- by (induct set: bt) (simp_all add: add_commute n_leaves_type)
+ by (induct set: bt) (simp_all add: add_commute)
lemma n_leaves_nodes: "t \<in> bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
- by (induct set: bt) (simp_all add: add_succ_right)
+ by (induct set: bt) simp_all
text {*
Theorems about @{term bt_reflect}.
--- a/src/ZF/Induct/Brouwer.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/ZF/Induct/Brouwer.thy Tue Mar 13 14:44:27 2012 +0100
@@ -71,7 +71,7 @@
-- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
-- {* for @{text Well} to prove this. *}
apply (rule Well_unfold [THEN trans])
- apply (simp add: Sigma_bool Pi_empty1 succ_def)
+ apply (simp add: Sigma_bool succ_def)
done
end
--- a/src/ZF/Induct/Comb.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/ZF/Induct/Comb.thy Tue Mar 13 14:44:27 2012 +0100
@@ -114,8 +114,6 @@
inductive_cases Ap_E [elim!]: "p\<bullet>q \<in> comb"
-declare comb.intros [intro!]
-
subsection {* Results about Contraction *}
@@ -189,13 +187,13 @@
text {* Counterexample to the diamond property for @{text "-1->"}. *}
lemma KIII_contract1: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> I"
- by (blast intro: comb.intros contract.K comb_I)
+ by (blast intro: comb_I)
lemma KIII_contract2: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I))"
- by (unfold I_def) (blast intro: comb.intros contract.intros)
+ by (unfold I_def) (blast intro: contract.intros)
lemma KIII_contract3: "K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I)) -1-> I"
- by (blast intro: comb.intros contract.K comb_I)
+ by (blast intro: comb_I)
lemma not_diamond_contract: "\<not> diamond(contract)"
apply (unfold diamond_def)
--- a/src/ZF/Induct/Term.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/ZF/Induct/Term.thy Tue Mar 13 14:44:27 2012 +0100
@@ -138,8 +138,7 @@
apply (subst term_rec)
apply (assumption | rule a)+
apply (erule list.induct)
- apply (simp add: term_rec)
- apply (auto simp add: term_rec)
+ apply auto
done
lemma def_term_rec: