# HG changeset patch
# User wenzelm
# Date 1564479699 -7200
# Node ID a21a96eda0332312e5b63cfe49791621efc779cc
# Parent  6410166400ea5a15e02eee28f47c00912d4a08fb
clarified modules;

diff -r 6410166400ea -r a21a96eda033 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Tue Jul 30 11:41:39 2019 +0200
@@ -13,7 +13,7 @@
 
 ML \<open>
   fun export_proof ctxt thm =
-    Proofterm.encode (Reconstruct.clean_proof_of ctxt true thm);
+    Proofterm.encode (Thm.clean_proof_of ctxt true thm);
 
   fun import_proof thy xml =
     let
diff -r 6410166400ea -r a21a96eda033 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -148,7 +148,7 @@
             | _ => AbsP ("H", SOME p, prf)))
           (rec_fns ~~ Thm.prems_of thm)
           (Proofterm.proof_combP
-            (Reconstruct.proof_of ctxt' thm', map PBound (length prems - 1 downto 0))));
+            (Thm.reconstruct_proof_of ctxt' thm', map PBound (length prems - 1 downto 0))));
 
     val r' =
       if null is then r
@@ -214,10 +214,10 @@
               (AbsP ("H", SOME (Logic.varify_global p), prf)))
           (prems ~~ rs)
           (Proofterm.proof_combP
-            (Reconstruct.proof_of ctxt' thm', map PBound (length prems - 1 downto 0))));
+            (Thm.reconstruct_proof_of ctxt' thm', map PBound (length prems - 1 downto 0))));
     val prf' =
       Extraction.abs_corr_shyps thy' exhaust []
-        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of ctxt' exhaust);
+        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Thm.reconstruct_proof_of ctxt' exhaust);
     val r' =
       Logic.varify_global (Abs ("y", T,
         (fold_rev (Term.abs o dest_Free) rs
diff -r 6410166400ea -r a21a96eda033 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -20,7 +20,7 @@
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
 
 fun prf_of ctxt thm =
-  Reconstruct.proof_of ctxt thm
+  Thm.reconstruct_proof_of ctxt thm
   |> Reconstruct.expand_proof ctxt [("", NONE)];  (* FIXME *)
 
 fun subsets [] = [[]]
diff -r 6410166400ea -r a21a96eda033 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -195,6 +195,6 @@
     (Proofterm.term_of_proof prf);
 
 fun pretty_clean_proof_of ctxt full thm =
-  pretty_proof ctxt (Reconstruct.clean_proof_of ctxt full thm);
+  pretty_proof ctxt (Thm.clean_proof_of ctxt full thm);
 
 end;
diff -r 6410166400ea -r a21a96eda033 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -6,14 +6,12 @@
 
 signature RECONSTRUCT =
 sig
-  val quiet_mode : bool Config.T
-  val reconstruct_proof : Proof.context -> term -> Proofterm.proof -> Proofterm.proof
-  val prop_of' : term list -> Proofterm.proof -> term
-  val prop_of : Proofterm.proof -> term
-  val proof_of : Proof.context -> thm -> Proofterm.proof
-  val expand_proof : Proof.context -> (string * term option) list ->
+  val quiet_mode: bool Config.T
+  val reconstruct_proof: Proof.context -> term -> Proofterm.proof -> Proofterm.proof
+  val prop_of': term list -> Proofterm.proof -> term
+  val prop_of: Proofterm.proof -> term
+  val expand_proof: Proof.context -> (string * term option) list ->
     Proofterm.proof -> Proofterm.proof
-  val clean_proof_of : Proof.context -> bool -> thm -> Proofterm.proof
 end;
 
 structure Reconstruct : RECONSTRUCT =
@@ -250,7 +248,7 @@
       let
         fun search env [] = error ("Unsolvable constraints:\n" ^
               Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
-                Thm.pretty_flexpair ctxt (apply2 (Envir.norm_term bigenv) p)) cs)))
+                Syntax.pretty_flexpair ctxt (apply2 (Envir.norm_term bigenv) p)) cs)))
           | search env ((u, p as (t1, t2), vs)::ps) =
               if u then
                 let
@@ -321,10 +319,6 @@
 val prop_of' = Envir.beta_eta_contract oo prop_of0;
 val prop_of = prop_of' [];
 
-fun proof_of ctxt raw_thm =
-  let val thm = Thm.transfer' ctxt raw_thm
-  in reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
-
 
 (* expand and reconstruct subproofs *)
 
@@ -374,21 +368,4 @@
 
   in #3 (expand (Proofterm.maxidx_proof prf ~1) [] prf) end;
 
-
-(* cleanup for output etc. *)
-
-fun clean_proof_of ctxt full thm =
-  let
-    val (_, prop) =
-      Logic.unconstrainT (Thm.shyps_of thm)
-        (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
-  in
-    Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
-    |> reconstruct_proof ctxt prop
-    |> expand_proof ctxt [("", NONE)]
-    |> Proofterm.rew_proof (Proof_Context.theory_of ctxt)
-    |> Proofterm.no_thm_proofs
-    |> not full ? Proofterm.shrink_proof
-  end;
-
 end;
diff -r 6410166400ea -r a21a96eda033 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/Pure/ROOT.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -169,10 +169,12 @@
 ML_file "unify.ML";
 ML_file "theory.ML";
 ML_file "proofterm.ML";
+ML_file "Proof/reconstruct.ML";
 ML_file "thm.ML";
 ML_file "more_pattern.ML";
 ML_file "more_unify.ML";
 ML_file "more_thm.ML";
+
 ML_file "facts.ML";
 ML_file "global_theory.ML";
 ML_file "pure_thy.ML";
@@ -283,7 +285,6 @@
 ML_file "Isar/toplevel.ML";
 
 (*proof term operations*)
-ML_file "Proof/reconstruct.ML";
 ML_file "Proof/proof_syntax.ML";
 ML_file "Proof/proof_rewrite_rules.ML";
 ML_file "Proof/proof_checker.ML";
diff -r 6410166400ea -r a21a96eda033 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -70,6 +70,7 @@
   val string_of_term_global: theory -> term -> string
   val string_of_typ_global: theory -> typ -> string
   val string_of_sort_global: theory -> sort -> string
+  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   type syntax
   val eq_syntax: syntax * syntax -> bool
   val force_syntax: syntax -> unit
@@ -344,6 +345,12 @@
 val string_of_sort_global = string_of_sort o init_pretty_global;
 
 
+(* derived operations *)
+
+fun pretty_flexpair ctxt (t, u) = Pretty.block
+  [pretty_term ctxt t, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, pretty_term ctxt u];
+
+
 
 (** tables of translation functions **)
 
@@ -678,4 +685,3 @@
 open Lexicon.Syntax;
 
 end;
-
diff -r 6410166400ea -r a21a96eda033 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/Pure/goal_display.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -93,7 +93,7 @@
       Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
     val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
 
-    val pretty_ffpairs = pretty_list "flex-flex pairs:" (Thm.pretty_flexpair ctxt);
+    val pretty_ffpairs = pretty_list "flex-flex pairs:" (Syntax.pretty_flexpair ctxt);
 
     val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
     val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
diff -r 6410166400ea -r a21a96eda033 src/Pure/more_pattern.ML
--- a/src/Pure/more_pattern.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/Pure/more_pattern.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -12,7 +12,6 @@
   val matchess: theory -> term list * term list -> bool
   val equiv: theory -> term * term -> bool
   val first_order: term -> bool
-  val pattern: term -> bool
   val match_rew: theory -> term -> term * term -> (term * term) option
   val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
   val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
@@ -36,14 +35,6 @@
   | first_order (t $ u) = first_order t andalso first_order u
   | first_order _ = true;
 
-fun pattern (Abs (_, _, t)) = pattern t
-  | pattern t =
-      let val (head, args) = strip_comb t in
-        if is_Var head then
-          forall is_Bound args andalso not (has_duplicates (op aconv) args)
-        else forall pattern args
-      end;
-
 
 (* rewriting -- simple but fast *)
 
diff -r 6410166400ea -r a21a96eda033 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -114,12 +114,13 @@
   val tag: string * string -> attribute
   val untag: string -> attribute
   val kind: string -> attribute
+  val reconstruct_proof_of: Proof.context -> thm -> Proofterm.proof
+  val clean_proof_of: Proof.context -> bool -> thm -> Proofterm.proof
   val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit
   val show_consts: bool Config.T
   val show_hyps: bool Config.T
   val show_tags: bool Config.T
-  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val pretty_thm_item: Proof.context -> thm -> Pretty.T
@@ -584,7 +585,7 @@
 
 
 
-(*** theorem tags ***)
+(** theorem tags **)
 
 (* add / delete tags *)
 
@@ -672,7 +673,29 @@
 fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k));
 
 
-(* forked proofs *)
+
+(** proof terms **)
+
+fun reconstruct_proof_of ctxt raw_thm =
+  let val thm = Thm.transfer' ctxt raw_thm
+  in Reconstruct.reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
+
+fun clean_proof_of ctxt full thm =
+  let
+    val (_, prop) =
+      Logic.unconstrainT (Thm.shyps_of thm)
+        (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
+  in
+    Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
+    |> Reconstruct.reconstruct_proof ctxt prop
+    |> Reconstruct.expand_proof ctxt [("", NONE)]
+    |> Proofterm.rew_proof (Proof_Context.theory_of ctxt)
+    |> Proofterm.no_thm_proofs
+    |> not full ? Proofterm.shrink_proof
+  end;
+
+
+(** forked proofs **)
 
 structure Proofs = Theory_Data
 (
@@ -706,9 +729,6 @@
 fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
 
-fun pretty_flexpair ctxt (t, u) = Pretty.block
-  [Syntax.pretty_term ctxt t, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, Syntax.pretty_term ctxt u];
-
 fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
   let
     val show_tags = Config.get ctxt show_tags;
@@ -732,7 +752,7 @@
       if hlen = 0 then []
       else if show_hyps orelse show_hyps' then
         [Pretty.brk 2, Pretty.list "[" "]"
-          (map (q o pretty_flexpair ctxt) tpairs @ map prt_term hyps @
+          (map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
            map (Syntax.pretty_sort ctxt) extra_shyps)]
       else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
     val tsymbs =
diff -r 6410166400ea -r a21a96eda033 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/Pure/pattern.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -21,6 +21,7 @@
   val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val first_order_match: theory -> term * term
     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
+  val pattern: term -> bool
 end;
 
 structure Pattern: PATTERN =
@@ -375,5 +376,12 @@
   val envir' = apfst (typ_match thy (pT, oT)) envir;
 in mtch [] po envir' handle Pattern => first_order_match thy po envir' end;
 
+
+fun pattern (Abs (_, _, t)) = pattern t
+  | pattern t =
+      let val (head, args) = strip_comb t in
+        if is_Var head then
+          forall is_Bound args andalso not (has_duplicates (op aconv) args)
+        else forall pattern args
+      end;
 end;
-