--- a/NEWS Tue Mar 13 17:11:49 2012 +0000
+++ b/NEWS Tue Mar 13 17:17:52 2012 +0000
@@ -43,6 +43,11 @@
*** Pure ***
+* Attribute "abs_def" turns an equation of the form "f x y == t" into
+"f == %x y. t", which ensures that "simp" or "unfold" steps always
+expand it. This also works for object-logic equality. (Formerly
+undocumented feature.)
+
* Discontinued old "prems" fact, which used to refer to the accidental
collection of foundational premises in the context (marked as legacy
since Isabelle2011).
--- a/src/HOL/Big_Operators.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Big_Operators.thy Tue Mar 13 17:17:52 2012 +0000
@@ -1537,11 +1537,11 @@
lemma dual_max:
"ord.max (op \<ge>) = min"
- by (auto simp add: ord.max_def_raw min_def fun_eq_iff)
+ by (auto simp add: ord.max_def min_def fun_eq_iff)
lemma dual_min:
"ord.min (op \<ge>) = max"
- by (auto simp add: ord.min_def_raw max_def fun_eq_iff)
+ by (auto simp add: ord.min_def max_def fun_eq_iff)
lemma strict_below_fold1_iff:
assumes "finite A" and "A \<noteq> {}"
--- a/src/HOL/Finite_Set.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Finite_Set.thy Tue Mar 13 17:17:52 2012 +0000
@@ -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 17:11:49 2012 +0000
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Tue Mar 13 17:17:52 2012 +0000
@@ -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/Import/HOL_Light/Compatibility.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Import/HOL_Light/Compatibility.thy Tue Mar 13 17:17:52 2012 +0000
@@ -272,7 +272,7 @@
lemma DEF_DISJOINT:
"DISJOINT = (%u ua. u \<inter> ua = {})"
- by (auto simp add: DISJOINT_def_raw)
+ by (auto simp add: DISJOINT_def [abs_def])
lemma DEF_DIFF:
"op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
@@ -282,7 +282,7 @@
lemma DEF_DELETE:
"DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
- by (auto simp add: DELETE_def_raw)
+ by (auto simp add: DELETE_def [abs_def])
lemma COND_DEF:
"(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> x = f))"
@@ -344,7 +344,7 @@
definition [import_rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
- by (simp add: INFINITE_def_raw)
+ by (simp add: INFINITE_def [abs_def])
end
--- a/src/HOL/Import/HOL_Light/HOLLightInt.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy Tue Mar 13 17:17:52 2012 +0000
@@ -90,7 +90,7 @@
lemma int_mod_def':
"int_mod = (\<lambda>u ua ub. (u dvd (ua - ub)))"
- by (simp add: int_mod_def_raw)
+ by (simp add: int_mod_def [abs_def])
lemma int_congruent:
"\<forall>x xa xb. int_mod xb x xa = (\<exists>d. x - xa = xb * d)"
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Mar 13 17:17:52 2012 +0000
@@ -7,9 +7,9 @@
declare HOL.if_bool_eq_disj[code_pred_inline]
declare bool_diff_def[code_pred_inline]
-declare inf_bool_def_raw[code_pred_inline]
-declare less_bool_def_raw[code_pred_inline]
-declare le_bool_def_raw[code_pred_inline]
+declare inf_bool_def[abs_def, code_pred_inline]
+declare less_bool_def[abs_def, code_pred_inline]
+declare le_bool_def[abs_def, code_pred_inline]
lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
by (rule eq_reflection) (auto simp add: fun_eq_iff min_def)
--- a/src/HOL/List.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/List.thy Tue Mar 13 17:17:52 2012 +0000
@@ -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 17:11:49 2012 +0000
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Mar 13 17:17:52 2012 +0000
@@ -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/Multivariate_Analysis/Integration.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Mar 13 17:17:52 2012 +0000
@@ -2762,12 +2762,24 @@
lemma negligible: "negligible s \<longleftrightarrow> (\<forall>t::('a::ordered_euclidean_space) set. ((indicator s::'a\<Rightarrow>real) has_integral 0) t)"
apply safe defer apply(subst negligible_def)
-proof- fix t::"'a set" assume as:"negligible s"
- have *:"(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)" by(rule ext,auto)
- show "((indicator s::'a\<Rightarrow>real) has_integral 0) t" apply(subst has_integral_alt)
- apply(cases,subst if_P,assumption) unfolding if_not_P apply(safe,rule as[unfolded negligible_def,rule_format])
- apply(rule_tac x=1 in exI) apply(safe,rule zero_less_one) apply(rule_tac x=0 in exI)
- using negligible_subset[OF as,of "s \<inter> t"] unfolding negligible_def indicator_def_raw unfolding * by auto qed auto
+proof -
+ fix t::"'a set" assume as:"negligible s"
+ have *:"(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)"
+ by auto
+ show "((indicator s::'a\<Rightarrow>real) has_integral 0) t"
+ apply(subst has_integral_alt)
+ apply(cases,subst if_P,assumption)
+ unfolding if_not_P
+ apply(safe,rule as[unfolded negligible_def,rule_format])
+ apply(rule_tac x=1 in exI)
+ apply(safe,rule zero_less_one)
+ apply(rule_tac x=0 in exI)
+ using negligible_subset[OF as,of "s \<inter> t"]
+ unfolding negligible_def indicator_def [abs_def]
+ unfolding *
+ apply auto
+ done
+qed auto
subsection {* Finite case of the spike theorem is quite commonly needed. *}
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Mar 13 17:17:52 2012 +0000
@@ -149,7 +149,7 @@
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
nitpick [expect = none]
-by (rule Zero_nat_def_raw)
+by (rule Zero_nat_def [abs_def])
lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
nitpick [expect = none]
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Tue Mar 13 17:17:52 2012 +0000
@@ -32,7 +32,7 @@
lemma [code_pred_def]:
"cardsp [] g k = False"
"cardsp (e # s) g k = (let C = cardsp s g in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
-unfolding cardsp_def_raw cards.simps by (auto simp add: Let_def split: event.split)
+unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split)
definition
"isinp evs r g = (g \<in> isin evs r)"
@@ -44,7 +44,7 @@
in case e of Check_in g' r c => G g
| Enter g' r' c => if r' = r then g = g' \<or> G g else G g
| Exit g' r' => if r' = r then ((g \<noteq> g') \<and> G g) else G g)"
-unfolding isinp_def_raw isin.simps by (auto simp add: Let_def split: event.split)
+unfolding isinp_def [abs_def] isin.simps by (auto simp add: Let_def split: event.split)
declare hotel.simps(1)[code_pred_def]
lemma [code_pred_def]:
--- a/src/HOL/Probability/Binary_Product_Measure.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Mar 13 17:17:52 2012 +0000
@@ -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/Borel_Space.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Probability/Borel_Space.thy Tue Mar 13 17:17:52 2012 +0000
@@ -90,7 +90,7 @@
lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]:
assumes A: "A \<in> sets M"
shows "indicator A \<in> borel_measurable M"
- unfolding indicator_def_raw using A
+ unfolding indicator_def [abs_def] using A
by (auto intro!: measurable_If_set borel_measurable_const)
lemma (in sigma_algebra) borel_measurable_indicator_iff:
@@ -101,7 +101,7 @@
then have "?I -` {1} \<inter> space M \<in> sets M"
unfolding measurable_def by auto
also have "?I -` {1} \<inter> space M = A \<inter> space M"
- unfolding indicator_def_raw by auto
+ unfolding indicator_def [abs_def] by auto
finally show "A \<inter> space M \<in> sets M" .
next
assume "A \<inter> space M \<in> sets M"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Mar 13 17:17:52 2012 +0000
@@ -706,7 +706,7 @@
have "\<And>A. measure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
using assms by (subst measure_times) auto
then show ?thesis
- unfolding positive_integral_def simple_function_def simple_integral_def_raw
+ unfolding positive_integral_def simple_function_def simple_integral_def [abs_def]
proof (simp add: P_empty, intro antisym)
show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
@@ -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 17:11:49 2012 +0000
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Mar 13 17:17:52 2012 +0000
@@ -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))"
@@ -874,7 +874,7 @@
by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
also have "\<dots> = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
using J M.sets_into_space
- by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast
+ by (auto simp: emb_def [abs_def] intro!: sigma_sets_vimage[symmetric]) blast
also have "\<dots> \<subseteq> sigma_sets (space (Pi\<^isub>M I M)) ?M"
using J by (intro sigma_sets_mono') auto
finally show "emb I J ` sets (Pi\<^isub>M J M) \<subseteq> sigma_sets ?O ?M"
--- a/src/HOL/Probability/Information.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Probability/Information.thy Tue Mar 13 17:17:52 2012 +0000
@@ -823,7 +823,7 @@
interpret S: prob_space "S\<lparr> measure := ereal\<circ>distribution X \<rparr>"
using distribution_prob_space[OF X] .
from A show "S.\<mu>' A = distribution X A"
- unfolding S.\<mu>'_def by (simp add: distribution_def_raw \<mu>'_def)
+ unfolding S.\<mu>'_def by (simp add: distribution_def [abs_def] \<mu>'_def)
qed
lemma (in information_space) entropy_uniform_max:
--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 13 17:17:52 2012 +0000
@@ -247,7 +247,7 @@
hence "finite ?S" by (rule finite_subset) simp
moreover have "- A \<inter> space M = space M - A" by auto
ultimately show ?thesis unfolding simple_function_def
- using assms by (auto simp: indicator_def_raw)
+ using assms by (auto simp: indicator_def [abs_def])
qed
lemma (in sigma_algebra) simple_function_Pair[intro, simp]:
@@ -821,7 +821,7 @@
lemma (in measure_space) simple_integral_subalgebra:
assumes N: "measure_space N" and [simp]: "space N = space M" "measure N = measure M"
shows "integral\<^isup>S N = integral\<^isup>S M"
- unfolding simple_integral_def_raw by simp
+ unfolding simple_integral_def [abs_def] by simp
lemma (in measure_space) simple_integral_vimage:
assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
@@ -1482,7 +1482,7 @@
have borel[simp]:
"borel_measurable M' = borel_measurable M"
"simple_function M' = simple_function M"
- unfolding measurable_def simple_function_def_raw by (auto simp: M')
+ unfolding measurable_def simple_function_def [abs_def] by (auto simp: M')
from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess G . note G = this
note G' = borel_measurable_simple_function[OF this(1)] simple_functionD[OF G(1)]
note G'(2)[simp]
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Mar 13 17:17:52 2012 +0000
@@ -48,7 +48,7 @@
qed
lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
- unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
+ unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
subsection {* Lebesgue measure *}
@@ -95,7 +95,7 @@
using A by (auto intro!: integrable_sub dest: lebesgueD simp: cube_def)
next
fix n show "(indicator {} :: _\<Rightarrow>real) integrable_on cube n"
- by (auto simp: cube_def indicator_def_raw)
+ by (auto simp: cube_def indicator_def [abs_def])
next
fix A :: "nat \<Rightarrow> 'a set" and n ::nat assume "range A \<subseteq> sets lebesgue"
then have A: "\<And>i. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
@@ -193,7 +193,7 @@
have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
- unfolding indicator_def_raw has_integral_restrict_univ ..
+ unfolding indicator_def [abs_def] has_integral_restrict_univ ..
finally show ?thesis
using has_integral_const[of "1::real" "?N" "?P"] by simp
qed
@@ -437,9 +437,9 @@
shows lmeasure_atLeastAtMost[simp]: "lebesgue.\<mu> {a..b} = ereal (content {a..b})"
proof -
have "(indicator (UNIV \<inter> {a..b})::_\<Rightarrow>real) integrable_on UNIV"
- unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def_raw)
+ unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def [abs_def])
from lmeasure_eq_integral[OF this] show ?thesis unfolding integral_indicator_UNIV
- by (simp add: indicator_def_raw)
+ by (simp add: indicator_def [abs_def])
qed
lemma atLeastAtMost_singleton_euclidean[simp]:
@@ -504,7 +504,7 @@
and sets_lborel[simp]: "sets lborel = sets borel"
and measure_lborel[simp]: "measure lborel = lebesgue.\<mu>"
and measurable_lborel[simp]: "measurable lborel = measurable borel"
- by (simp_all add: measurable_def_raw lborel_def)
+ by (simp_all add: measurable_def [abs_def] lborel_def)
interpretation lborel: measure_space "lborel :: ('a::ordered_euclidean_space) measure_space"
where "space lborel = UNIV"
@@ -871,7 +871,7 @@
let ?E = "\<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
show "Int_stable ?E" using Int_stable_cuboids .
- show "range cube \<subseteq> sets ?E" unfolding cube_def_raw by auto
+ show "range cube \<subseteq> sets ?E" unfolding cube_def [abs_def] by auto
show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
{ fix x have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
then show "(\<Union>i. cube i) = space ?E" by auto
@@ -1001,7 +1001,7 @@
then show "(\<Union>i. cube i) = space ?E" by auto
show "incseq cube" by (intro incseq_SucI cube_subset_Suc)
show "range cube \<subseteq> sets ?E"
- unfolding cube_def_raw by auto
+ unfolding cube_def [abs_def] by auto
show "\<And>i. measure lebesgue (cube i) \<noteq> \<infinity>"
by (simp add: cube_def)
show "measure_space lborel" by default
--- a/src/HOL/Probability/Probability_Measure.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Probability/Probability_Measure.thy Tue Mar 13 17:17:52 2012 +0000
@@ -260,7 +260,7 @@
proof (rule prob_space_vimage)
show "X \<in> measure_preserving M ?S"
using X
- unfolding measure_preserving_def distribution_def_raw
+ unfolding measure_preserving_def distribution_def [abs_def]
by (auto simp: finite_measure_eq measurable_sets)
show "sigma_algebra ?S" using X by simp
qed
@@ -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/HOL/Probability/ex/Dining_Cryptographers.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Tue Mar 13 17:17:52 2012 +0000
@@ -132,7 +132,7 @@
have *: "{xs. length xs = n} \<noteq> {}"
by (auto intro!: exI[of _ "replicate n undefined"])
show ?thesis
- unfolding payer_def_raw dc_crypto fst_image_times if_not_P[OF *] ..
+ unfolding payer_def [abs_def] dc_crypto fst_image_times if_not_P[OF *] ..
qed
lemma card_payer_and_inversion:
@@ -310,7 +310,7 @@
let ?sets = "{?set i | i. i < n}"
have [simp]: "length xs = n" using assms
- by (auto simp: dc_crypto inversion_def_raw)
+ by (auto simp: dc_crypto inversion_def [abs_def])
have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> i < n. ?set i)"
unfolding dc_crypto payer_def by auto
@@ -462,7 +462,7 @@
{dc \<in> dc_crypto. payer dc = Some (the z) \<and> inversion dc = x}"
by (auto simp add: payer_def)
moreover from x z obtain i where "z = Some i" and "i < n" by auto
- moreover from x have "length x = n" by (auto simp: inversion_def_raw dc_crypto)
+ moreover from x have "length x = n" by (auto simp: inversion_def [abs_def] dc_crypto)
ultimately
have "?dIP {(x, z)} = 2 / (real n * 2^n)" using x
by (auto simp add: card_dc_crypto card_payer_and_inversion distribution_def)
@@ -490,7 +490,7 @@
unfolding neg_equal_iff_equal
proof (rule setsum_cong[OF refl])
fix x assume x_inv: "x \<in> inversion ` dc_crypto"
- hence "length x = n" by (auto simp: inversion_def_raw dc_crypto)
+ hence "length x = n" by (auto simp: inversion_def [abs_def] dc_crypto)
moreover have "inversion -` {x} \<inter> dc_crypto = {dc \<in> dc_crypto. inversion dc = x}" by auto
ultimately have "?dI {x} = 2 / 2^n" using `0 < n`
by (auto simp: card_inversion[OF x_inv] card_dc_crypto distribution_def)
--- a/src/HOL/Series.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Series.thy Tue Mar 13 17:17:52 2012 +0000
@@ -87,10 +87,13 @@
by (simp add: sums_def summable_def, blast)
lemma summable_sums:
- fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}" assumes "summable f" shows "f sums (suminf f)"
+ fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}"
+ assumes "summable f"
+ shows "f sums (suminf f)"
proof -
- from assms guess s unfolding summable_def sums_def_raw .. note s = this
- then show ?thesis unfolding sums_def_raw suminf_def
+ from assms obtain s where s: "(\<lambda>n. setsum f {0..<n}) ----> s"
+ unfolding summable_def sums_def [abs_def] ..
+ then show ?thesis unfolding sums_def [abs_def] suminf_def
by (rule theI, auto intro!: tendsto_unique[OF trivial_limit_sequentially])
qed
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Mar 13 17:17:52 2012 +0000
@@ -476,11 +476,11 @@
pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u)
val combinator_table =
- [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
- (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
- (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
- (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
- (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
+ [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
+ (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
+ (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
+ (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
+ (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
fun uncombine_term thy =
let
--- a/src/HOL/Tools/Meson/meson.ML Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Tools/Meson/meson.ML Tue Mar 13 17:17:52 2012 +0000
@@ -560,7 +560,7 @@
val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
(* FIXME: "let_simp" is probably redundant now that we also rewrite with
- "Let_def_raw". *)
+ "Let_def [abs_def]". *)
val nnf_ss =
HOL_basic_ss addsimps nnf_extra_simps
addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
@@ -574,7 +574,7 @@
val presimplify =
rewrite_rule (map safe_mk_meta_eq nnf_simps)
#> simplify nnf_ss
- #> Raw_Simplifier.rewrite_rule @{thms Let_def_raw}
+ #> Raw_Simplifier.rewrite_rule @{thms Let_def [abs_def]}
fun make_nnf ctxt th = case prems_of th of
[] => th |> presimplify |> make_nnf1 ctxt
--- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Mar 13 17:17:52 2012 +0000
@@ -188,8 +188,6 @@
in c_variant_abs_multi (ct, cv::vars) end
handle CTERM _ => (ct0, rev vars);
-val skolem_def_raw = @{thms skolem_def_raw}
-
(* Given the definition of a Skolem function, return a theorem to replace
an existential formula by a use of that function.
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
@@ -210,8 +208,8 @@
Drule.list_comb (rhs, frees)
|> Drule.beta_conv cabs |> Thm.apply cTrueprop
fun tacf [prem] =
- rewrite_goals_tac skolem_def_raw
- THEN rtac ((prem |> rewrite_rule skolem_def_raw)
+ rewrite_goals_tac @{thms skolem_def [abs_def]}
+ THEN rtac ((prem |> rewrite_rule @{thms skolem_def [abs_def]})
RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
in
Goal.prove_internal [ex_tm] conc tacf
--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Mar 13 17:17:52 2012 +0000
@@ -62,7 +62,7 @@
fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth =
let
val thy = Proof_Context.theory_of ctxt
- val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
+ val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
val ct = cterm_of thy (HOLogic.mk_Trueprop t)
in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
--- a/src/HOL/ex/Dedekind_Real.thy Tue Mar 13 17:11:49 2012 +0000
+++ b/src/HOL/ex/Dedekind_Real.thy Tue Mar 13 17:17:52 2012 +0000
@@ -115,7 +115,7 @@
by (simp add: preal_def cut_of_rat)
lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
- unfolding preal_def cut_def_raw by blast
+ unfolding preal_def cut_def [abs_def] by blast
lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
apply (drule preal_nonempty)
@@ -131,10 +131,10 @@
done
lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
- unfolding preal_def cut_def_raw by blast
+ unfolding preal_def cut_def [abs_def] by blast
lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
- unfolding preal_def cut_def_raw by blast
+ unfolding preal_def cut_def [abs_def] by blast
text{*Relaxing the final premise*}
lemma preal_downwards_closed':
@@ -966,7 +966,7 @@
lemma mem_diff_set:
"R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
-apply (unfold preal_def cut_def_raw)
+apply (unfold preal_def cut_def [abs_def])
apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
diff_set_lemma3 diff_set_lemma4)
done
@@ -1135,7 +1135,7 @@
lemma preal_sup:
"[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
-apply (unfold preal_def cut_def_raw)
+apply (unfold preal_def cut_def [abs_def])
apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
preal_sup_set_lemma3 preal_sup_set_lemma4)
done
--- a/src/Pure/General/binding.ML Tue Mar 13 17:11:49 2012 +0000
+++ b/src/Pure/General/binding.ML Tue Mar 13 17:17:52 2012 +0000
@@ -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 17:11:49 2012 +0000
+++ b/src/Pure/General/pretty.ML Tue Mar 13 17:17:52 2012 +0000
@@ -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/attrib.ML Tue Mar 13 17:11:49 2012 +0000
+++ b/src/Pure/Isar/attrib.ML Tue Mar 13 17:17:52 2012 +0000
@@ -283,7 +283,8 @@
else if null decls' then [((b, []), fact')]
else [(empty_binding, decls'), ((b, []), fact')];
in (facts', context') end)
- |> fst |> flat |> map (apsnd (map (apfst single)));
+ |> fst |> flat |> map (apsnd (map (apfst single)))
+ |> filter_out (fn (b, fact) => is_empty_binding b andalso forall (null o #2) fact);
end;
@@ -399,8 +400,10 @@
setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
"declaration of definitional transformations" #>
- setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
- "abstract over free variables of a definition"));
+ setup (Binding.name "abs_def")
+ (Scan.succeed (Thm.rule_attribute (fn context =>
+ Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
+ "abstract over free variables of definitionial theorem"));
--- a/src/Pure/Isar/element.ML Tue Mar 13 17:11:49 2012 +0000
+++ b/src/Pure/Isar/element.ML Tue Mar 13 17:17:52 2012 +0000
@@ -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 17:11:49 2012 +0000
+++ b/src/Pure/Isar/expression.ML Tue Mar 13 17:17:52 2012 +0000
@@ -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/Isar/locale.ML Tue Mar 13 17:11:49 2012 +0000
+++ b/src/Pure/Isar/locale.ML Tue Mar 13 17:17:52 2012 +0000
@@ -533,21 +533,22 @@
(* Theorems *)
-fun add_thmss loc kind facts ctxt =
- ctxt
- |> Proof_Context.note_thmss kind
- (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
- |> snd
- |> Proof_Context.background_theory
- ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
- (* Registrations *)
- (fn thy => fold_rev (fn (_, morph) =>
- let
- val facts' = facts
- |> Element.transform_facts morph
- |> Attrib.map_facts (map (Attrib.attribute_i thy));
- in snd o Global_Theory.note_thmss kind facts' end)
- (registrations_of (Context.Theory thy) loc) thy));
+fun add_thmss _ _ [] ctxt = ctxt
+ | add_thmss loc kind facts ctxt =
+ ctxt
+ |> Proof_Context.note_thmss kind
+ (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
+ |> snd
+ |> Proof_Context.background_theory
+ ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
+ (* Registrations *)
+ (fn thy => fold_rev (fn (_, morph) =>
+ let
+ val facts' = facts
+ |> Element.transform_facts morph
+ |> Attrib.map_facts (map (Attrib.attribute_i thy));
+ in snd o Global_Theory.note_thmss kind facts' end)
+ (registrations_of (Context.Theory thy) loc) thy));
(* Declarations *)
--- a/src/Pure/PIDE/markup.ML Tue Mar 13 17:11:49 2012 +0000
+++ b/src/Pure/PIDE/markup.ML Tue Mar 13 17:17:52 2012 +0000
@@ -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 17:11:49 2012 +0000
+++ b/src/ZF/Induct/Binary_Trees.thy Tue Mar 13 17:17:52 2012 +0000
@@ -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 17:11:49 2012 +0000
+++ b/src/ZF/Induct/Brouwer.thy Tue Mar 13 17:17:52 2012 +0000
@@ -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 17:11:49 2012 +0000
+++ b/src/ZF/Induct/Comb.thy Tue Mar 13 17:17:52 2012 +0000
@@ -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 17:11:49 2012 +0000
+++ b/src/ZF/Induct/Term.thy Tue Mar 13 17:17:52 2012 +0000
@@ -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: