--- a/src/HOL/Proofs/ex/XML_Data.thy Fri Nov 08 16:07:31 2019 +0000
+++ b/src/HOL/Proofs/ex/XML_Data.thy Fri Nov 08 20:28:50 2019 +0100
@@ -13,7 +13,7 @@
ML \<open>
fun export_proof thy thm = thm
- |> Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
+ |> Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
|> Proofterm.encode (Sign.consts_of thy);
fun import_proof thy xml =
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Nov 08 16:07:31 2019 +0000
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Nov 08 20:28:50 2019 +0100
@@ -29,9 +29,11 @@
fun ?? x = if b then SOME x else NONE;
fun ax (prf as PAxm (s, prop, _)) Ts =
if b then PAxm (s, prop, SOME Ts) else prf;
- fun ty T = if b then
- let val Type (_, [Type (_, [U, _]), _]) = T
- in SOME U end
+ fun ty T =
+ if b then
+ (case T of
+ Type (_, [Type (_, [U, _]), _]) => SOME U
+ | _ => NONE)
else NONE;
val equal_intr_axm = ax Proofterm.equal_intr_axm [];
val equal_elim_axm = ax Proofterm.equal_elim_axm [];
--- a/src/Pure/Proof/proof_syntax.ML Fri Nov 08 16:07:31 2019 +0000
+++ b/src/Pure/Proof/proof_syntax.ML Fri Nov 08 20:28:50 2019 +0100
@@ -14,9 +14,11 @@
val proof_syntax: Proofterm.proof -> theory -> theory
val proof_of: bool -> thm -> Proofterm.proof
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
- val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
val pretty_proof_boxes_of: Proof.context ->
{full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T
+ val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
+ thm -> Proofterm.proof
+ val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
structure Proof_Syntax : PROOF_SYNTAX =
@@ -251,9 +253,6 @@
(Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
(term_of_proof prf);
-fun pretty_standard_proof_of ctxt full thm =
- pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
-
fun pretty_proof_boxes_of ctxt {full, preproc} thm =
let
val thy = Proof_Context.theory_of ctxt;
@@ -280,4 +279,19 @@
|> Pretty.chunks
end;
+
+(* standardized proofs *)
+
+fun standard_proof_of {full, expand_name} thm =
+ let val thy = Thm.theory_of_thm thm in
+ Thm.reconstruct_proof_of thm
+ |> Proofterm.expand_proof thy expand_name
+ |> Proofterm.rewrite_proof thy ([], Proof_Rewrite_Rules.rprocs true)
+ |> Proofterm.no_thm_proofs
+ |> not full ? Proofterm.shrink_proof
+ end;
+
+fun pretty_standard_proof_of ctxt full thm =
+ pretty_proof ctxt (standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
+
end;
--- a/src/Pure/ROOT.ML Fri Nov 08 16:07:31 2019 +0000
+++ b/src/Pure/ROOT.ML Fri Nov 08 20:28:50 2019 +0100
@@ -111,6 +111,7 @@
subsection "Concurrency within the ML runtime";
ML_file "ML/exn_properties.ML";
+ML_file_no_debug "ML/exn_debugger.ML";
ML_file "ML/ml_statistics.ML";
@@ -199,7 +200,6 @@
ML_file "ML/ml_env.ML";
ML_file "ML/ml_options.ML";
ML_file "ML/ml_print_depth.ML";
-ML_file_no_debug "ML/exn_debugger.ML";
ML_file_no_debug "Isar/runtime.ML";
ML_file "PIDE/execution.ML";
ML_file "ML/ml_compiler.ML";
@@ -287,8 +287,8 @@
ML_file "Isar/toplevel.ML";
(*proof term operations*)
+ML_file "Proof/proof_rewrite_rules.ML";
ML_file "Proof/proof_syntax.ML";
-ML_file "Proof/proof_rewrite_rules.ML";
ML_file "Proof/proof_checker.ML";
ML_file "Proof/extraction.ML";
--- a/src/Pure/Thy/export_theory.ML Fri Nov 08 16:07:31 2019 +0000
+++ b/src/Pure/Thy/export_theory.ML Fri Nov 08 20:28:50 2019 +0100
@@ -270,7 +270,8 @@
val proof0 =
if Proofterm.export_standard_enabled () then
- Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm
+ Proof_Syntax.standard_proof_of
+ {full = true, expand_name = SOME o expand_name thm_id} thm
else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm
else MinProof;
val (prop, SOME proof) =
--- a/src/Pure/more_thm.ML Fri Nov 08 16:07:31 2019 +0000
+++ b/src/Pure/more_thm.ML Fri Nov 08 20:28:50 2019 +0100
@@ -113,9 +113,6 @@
val tag: string * string -> attribute
val untag: string -> attribute
val kind: string -> attribute
- val reconstruct_proof_of: thm -> Proofterm.proof
- val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
- thm -> Proofterm.proof
val register_proofs: thm list lazy -> theory -> theory
val consolidate_theory: theory -> unit
val expose_theory: theory -> unit
@@ -653,22 +650,6 @@
-(** proof terms **)
-
-fun reconstruct_proof_of thm =
- Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-
-fun standard_proof_of {full, expand_name} thm =
- let val thy = Thm.theory_of_thm thm in
- reconstruct_proof_of thm
- |> Proofterm.expand_proof thy expand_name
- |> Proofterm.rew_proof thy
- |> Proofterm.no_thm_proofs
- |> not full ? Proofterm.shrink_proof
- end;
-
-
-
(** forked proofs **)
structure Proofs = Theory_Data
--- a/src/Pure/thm.ML Fri Nov 08 16:07:31 2019 +0000
+++ b/src/Pure/thm.ML Fri Nov 08 20:28:50 2019 +0100
@@ -101,6 +101,7 @@
val proof_bodies_of: thm list -> proof_body list
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
+ val reconstruct_proof_of: thm -> Proofterm.proof
val consolidate: thm list -> unit
val expose_proofs: theory -> thm list -> unit
val expose_proof: theory -> thm -> unit
@@ -760,6 +761,9 @@
val proof_body_of = singleton proof_bodies_of;
val proof_of = Proofterm.proof_of o proof_body_of;
+fun reconstruct_proof_of thm =
+ Proofterm.reconstruct_proof (theory_of_thm thm) (prop_of thm) (proof_of thm);
+
val consolidate = ignore o proof_bodies_of;
fun expose_proofs thy thms =
--- a/src/ZF/List.thy Fri Nov 08 16:07:31 2019 +0000
+++ b/src/ZF/List.thy Fri Nov 08 20:28:50 2019 +0100
@@ -1123,14 +1123,13 @@
apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff)
done
-lemma nth_upt [rule_format]:
- "[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i #+ k < j \<longrightarrow> nth(k, upt(i,j)) = i #+ k"
+lemma nth_upt [simp]:
+ "[| i \<in> nat; j \<in> nat; k \<in> nat; i #+ k < j |] ==> nth(k, upt(i,j)) = i #+ k"
+apply (rotate_tac -1, erule rev_mp)
apply (induct_tac "j", simp)
-apply (simp add: nth_append le_iff)
apply (auto dest!: not_lt_imp_le
- simp add: nth_append less_diff_conv add_commute)
+ simp add: nth_append le_iff less_diff_conv add_commute)
done
-declare nth_upt [simp]
lemma take_upt [rule_format]:
"[| m \<in> nat; n \<in> nat |] ==>
--- a/src/ZF/Nat.thy Fri Nov 08 16:07:31 2019 +0000
+++ b/src/ZF/Nat.thy Fri Nov 08 20:28:50 2019 +0100
@@ -155,26 +155,21 @@
lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1]
-lemmas complete_induct_rule =
- complete_induct [rule_format, case_names less, consumes 1]
-
-
-lemma nat_induct_from_lemma [rule_format]:
- "[| n \<in> nat; m \<in> nat;
- !!x. [| x \<in> nat; m \<le> x; P(x) |] ==> P(succ(x)) |]
- ==> m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
-apply (erule nat_induct)
-apply (simp_all add: distrib_simps le0_iff le_succ_iff)
-done
+lemma complete_induct_rule [case_names less, consumes 1]:
+ "i \<in> nat \<Longrightarrow> (\<And>x. x \<in> nat \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+ using complete_induct [of i P] by simp
(*Induction starting from m rather than 0*)
lemma nat_induct_from:
- "[| m \<le> n; m \<in> nat; n \<in> nat;
- P(m);
- !!x. [| x \<in> nat; m \<le> x; P(x) |] ==> P(succ(x)) |]
- ==> P(n)"
-apply (blast intro: nat_induct_from_lemma)
-done
+ assumes "m \<le> n" "m \<in> nat" "n \<in> nat"
+ and "P(m)"
+ and "!!x. [| x \<in> nat; m \<le> x; P(x) |] ==> P(succ(x))"
+ shows "P(n)"
+proof -
+ from assms(3) have "m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
+ by (rule nat_induct) (use assms(5) in \<open>simp_all add: distrib_simps le_succ_iff\<close>)
+ with assms(1,2,4) show ?thesis by blast
+qed
(*Induction suitable for subtraction and less-than*)
lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
--- a/src/ZF/Ordinal.thy Fri Nov 08 16:07:31 2019 +0000
+++ b/src/ZF/Ordinal.thy Fri Nov 08 20:28:50 2019 +0100
@@ -329,17 +329,16 @@
done
(*Induction over an ordinal*)
-lemmas Ord_induct [consumes 2] = Transset_induct [rule_format, OF _ Ord_is_Transset]
+lemma Ord_induct [consumes 2]:
+ "i \<in> k \<Longrightarrow> Ord(k) \<Longrightarrow> (\<And>x. x \<in> k \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+ using Transset_induct [OF _ Ord_is_Transset, of i k P] by simp
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
-
-lemma trans_induct [rule_format, consumes 1, case_names step]:
- "[| Ord(i);
- !!x.[| Ord(x); \<forall>y\<in>x. P(y) |] ==> P(x) |]
- ==> P(i)"
-apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption)
-apply (blast intro: Ord_succ [THEN Ord_in_Ord])
-done
+lemma trans_induct [consumes 1, case_names step]:
+ "Ord(i) \<Longrightarrow> (\<And>x. Ord(x) \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+ apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption)
+ apply (blast intro: Ord_succ [THEN Ord_in_Ord])
+ done
section\<open>Fundamental properties of the epsilon ordering (< on ordinals)\<close>
@@ -716,7 +715,9 @@
apply (erule Ord_cases, blast+)
done
-lemmas trans_induct3 = trans_induct3_raw [rule_format, case_names 0 succ limit, consumes 1]
+lemma trans_induct3 [case_names 0 succ limit, consumes 1]:
+ "Ord(i) \<Longrightarrow> P(0) \<Longrightarrow> (\<And>x. Ord(x) \<Longrightarrow> P(x) \<Longrightarrow> P(succ(x))) \<Longrightarrow> (\<And>x. Limit(x) \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+ using trans_induct3_raw [of i P] by simp
text\<open>A set of ordinals is either empty, contains its own union, or its
union is a limit ordinal.\<close>
@@ -756,7 +757,7 @@
lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)|] ==> succ(j) \<in> X"
by (drule Ord_set_cases, auto)
-lemma Limit_Union [rule_format]: "[| I \<noteq> 0; \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)"
+lemma Limit_Union [rule_format]: "[| I \<noteq> 0; (\<And>i. i\<in>I \<Longrightarrow> Limit(i)) |] ==> Limit(\<Union>I)"
apply (simp add: Limit_def lt_def)
apply (blast intro!: equalityI)
done
--- a/src/ZF/WF.thy Fri Nov 08 16:07:31 2019 +0000
+++ b/src/ZF/WF.thy Fri Nov 08 20:28:50 2019 +0100
@@ -137,9 +137,9 @@
apply (rule field_Int_square, blast)
done
-lemmas wf_on_induct =
- wf_on_induct_raw [rule_format, consumes 2, case_names step, induct set: wf_on]
-
+lemma wf_on_induct [consumes 2, case_names step, induct set: wf_on]:
+ "wf[A](r) \<Longrightarrow> a \<in> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> \<langle>y, x\<rangle> \<in> r \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(a)"
+ using wf_on_induct_raw [of A r a P] by simp
text\<open>If \<^term>\<open>r\<close> allows well-founded induction
then we have \<^term>\<open>wf(r)\<close>.\<close>
@@ -169,8 +169,9 @@
lemma wf_on_not_refl: "[| wf[A](r); a \<in> A |] ==> <a,a> \<notin> r"
by (erule_tac a=a in wf_on_induct, assumption, blast)
-lemma wf_on_not_sym [rule_format]:
- "[| wf[A](r); a \<in> A |] ==> \<forall>b\<in>A. <a,b>:r \<longrightarrow> <b,a>\<notin>r"
+lemma wf_on_not_sym:
+ "[| wf[A](r); a \<in> A |] ==> (\<And>b. b\<in>A \<Longrightarrow> <a,b>:r \<Longrightarrow> <b,a>\<notin>r)"
+apply (atomize (full), intro impI)
apply (erule_tac a=a in wf_on_induct, assumption, blast)
done
--- a/src/ZF/equalities.thy Fri Nov 08 16:07:31 2019 +0000
+++ b/src/ZF/equalities.thy Fri Nov 08 20:28:50 2019 +0100
@@ -105,7 +105,7 @@
lemma Diff_cons_eq: "cons(a,B) - C = (if a\<in>C then B-C else cons(a,B-C))"
by auto
-lemma equal_singleton [rule_format]: "[| a: C; \<forall>y\<in>C. y=b |] ==> C = {b}"
+lemma equal_singleton: "[| a: C; \<And>y. y \<in>C \<Longrightarrow> y=b |] ==> C = {b}"
by blast
lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
--- a/src/ZF/func.thy Fri Nov 08 16:07:31 2019 +0000
+++ b/src/ZF/func.thy Fri Nov 08 20:28:50 2019 +0100
@@ -356,8 +356,8 @@
apply (blast intro!: rel_Union function_Union)
done
-lemma gen_relation_Union [rule_format]:
- "\<forall>f\<in>F. relation(f) \<Longrightarrow> relation(\<Union>(F))"
+lemma gen_relation_Union:
+ "(\<And>f. f\<in>F \<Longrightarrow> relation(f)) \<Longrightarrow> relation(\<Union>(F))"
by (simp add: relation_def)