# HG changeset patch # User wenzelm # Date 1573241330 -3600 # Node ID fd82d53c176132a7de0bf9f7baa9c091702412c8 # Parent c4458eb355c0e74ca94b68396395a56fccb938b0# Parent 06c6495fb1d08c63e9dfa6622f95432163d71e8e merged diff -r c4458eb355c0 -r fd82d53c1761 src/HOL/Proofs/ex/XML_Data.thy --- 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 \ 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 = diff -r c4458eb355c0 -r fd82d53c1761 src/Pure/Proof/proof_rewrite_rules.ML --- 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 []; diff -r c4458eb355c0 -r fd82d53c1761 src/Pure/Proof/proof_syntax.ML --- 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; diff -r c4458eb355c0 -r fd82d53c1761 src/Pure/ROOT.ML --- 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"; diff -r c4458eb355c0 -r fd82d53c1761 src/Pure/Thy/export_theory.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) = diff -r c4458eb355c0 -r fd82d53c1761 src/Pure/more_thm.ML --- 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 diff -r c4458eb355c0 -r fd82d53c1761 src/Pure/thm.ML --- 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 = diff -r c4458eb355c0 -r fd82d53c1761 src/ZF/List.thy --- 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 \ nat; j \ nat; k \ nat |] ==> i #+ k < j \ nth(k, upt(i,j)) = i #+ k" +lemma nth_upt [simp]: + "[| i \ nat; j \ nat; k \ 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 \ nat; n \ nat |] ==> diff -r c4458eb355c0 -r fd82d53c1761 src/ZF/Nat.thy --- 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 \ nat; m \ nat; - !!x. [| x \ nat; m \ x; P(x) |] ==> P(succ(x)) |] - ==> m \ n \ P(m) \ 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 \ nat \ (\x. x \ nat \ (\y. y \ x \ P(y)) \ P(x)) \ P(i)" + using complete_induct [of i P] by simp (*Induction starting from m rather than 0*) lemma nat_induct_from: - "[| m \ n; m \ nat; n \ nat; - P(m); - !!x. [| x \ nat; m \ x; P(x) |] ==> P(succ(x)) |] - ==> P(n)" -apply (blast intro: nat_induct_from_lemma) -done + assumes "m \ n" "m \ nat" "n \ nat" + and "P(m)" + and "!!x. [| x \ nat; m \ x; P(x) |] ==> P(succ(x))" + shows "P(n)" +proof - + from assms(3) have "m \ n \ P(m) \ P(n)" + by (rule nat_induct) (use assms(5) in \simp_all add: distrib_simps le_succ_iff\) + 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]: diff -r c4458eb355c0 -r fd82d53c1761 src/ZF/Ordinal.thy --- 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 \ k \ Ord(k) \ (\x. x \ k \ (\y. y \ x \ P(y)) \ P(x)) \ 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); \y\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) \ (\x. Ord(x) \ (\y. y \ 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 section\Fundamental properties of the epsilon ordering (< on ordinals)\ @@ -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) \ P(0) \ (\x. Ord(x) \ P(x) \ P(succ(x))) \ (\x. Limit(x) \ (\y. y \ x \ P(y)) \ P(x)) \ P(i)" + using trans_induct3_raw [of i P] by simp text\A set of ordinals is either empty, contains its own union, or its union is a limit ordinal.\ @@ -756,7 +757,7 @@ lemma Ord_Union_eq_succD: "[|\x\X. Ord(x); \X = succ(j)|] ==> succ(j) \ X" by (drule Ord_set_cases, auto) -lemma Limit_Union [rule_format]: "[| I \ 0; \i\I. Limit(i) |] ==> Limit(\I)" +lemma Limit_Union [rule_format]: "[| I \ 0; (\i. i\I \ Limit(i)) |] ==> Limit(\I)" apply (simp add: Limit_def lt_def) apply (blast intro!: equalityI) done diff -r c4458eb355c0 -r fd82d53c1761 src/ZF/WF.thy --- 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) \ a \ A \ (\x. x \ A \ (\y. y \ A \ \y, x\ \ r \ P(y)) \ P(x)) \ P(a)" + using wf_on_induct_raw [of A r a P] by simp text\If \<^term>\r\ allows well-founded induction then we have \<^term>\wf(r)\.\ @@ -169,8 +169,9 @@ lemma wf_on_not_refl: "[| wf[A](r); a \ A |] ==> \ r" by (erule_tac a=a in wf_on_induct, assumption, blast) -lemma wf_on_not_sym [rule_format]: - "[| wf[A](r); a \ A |] ==> \b\A. :r \ \r" +lemma wf_on_not_sym: + "[| wf[A](r); a \ A |] ==> (\b. b\A \ :r \ \r)" +apply (atomize (full), intro impI) apply (erule_tac a=a in wf_on_induct, assumption, blast) done diff -r c4458eb355c0 -r fd82d53c1761 src/ZF/equalities.thy --- 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\C then B-C else cons(a,B-C))" by auto -lemma equal_singleton [rule_format]: "[| a: C; \y\C. y=b |] ==> C = {b}" +lemma equal_singleton: "[| a: C; \y. y \C \ y=b |] ==> C = {b}" by blast lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)" diff -r c4458eb355c0 -r fd82d53c1761 src/ZF/func.thy --- 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]: - "\f\F. relation(f) \ relation(\(F))" +lemma gen_relation_Union: + "(\f. f\F \ relation(f)) \ relation(\(F))" by (simp add: relation_def)