src/Pure/Proof/proof_syntax.ML
author wenzelm
Fri, 08 Nov 2019 20:12:57 +0100
changeset 71288 06c6495fb1d0
parent 71286 4b45d592ce29
child 71993 3875815f5967
permissions -rw-r--r--
retain type information from reconstruct_proof, notably for Export_Theory.export_thm;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     1
(*  Title:      Pure/Proof/proof_syntax.ML
11539
0f17da240450 tuned headers;
wenzelm
parents: 11522
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     3
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     4
Function for parsing and printing proof terms.
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     5
*)
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     6
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     7
signature PROOF_SYNTAX =
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     8
sig
17078
db9d24c8b439 export proof_syntax, proof_of;
wenzelm
parents: 17019
diff changeset
     9
  val add_proof_syntax: theory -> theory
71176
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    10
  val term_of_proof: proof -> term
28807
9f3ecb4aaac2 proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28375
diff changeset
    11
  val proof_of_term: theory -> bool -> term -> Proofterm.proof
37227
bdd8dd217b1f - Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents: 36610
diff changeset
    12
  val read_term: theory -> bool -> typ -> string -> term
bdd8dd217b1f - Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents: 36610
diff changeset
    13
  val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
17078
db9d24c8b439 export proof_syntax, proof_of;
wenzelm
parents: 17019
diff changeset
    14
  val proof_syntax: Proofterm.proof -> theory -> theory
70635
6e34025981be clarified global theory context;
wenzelm
parents: 70633
diff changeset
    15
  val proof_of: bool -> thm -> Proofterm.proof
27260
17d617c6b026 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents: 26939
diff changeset
    16
  val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
71206
be689b7d81fd clarified signature -- more options;
wenzelm
parents: 71176
diff changeset
    17
  val pretty_proof_boxes_of: Proof.context ->
be689b7d81fd clarified signature -- more options;
wenzelm
parents: 71176
diff changeset
    18
    {full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T
71286
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
    19
  val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
    20
    thm -> Proofterm.proof
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
    21
  val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    22
end;
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    23
33388
d64545e6cba5 modernized structure Proof_Syntax;
wenzelm
parents: 31943
diff changeset
    24
structure Proof_Syntax : PROOF_SYNTAX =
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    25
struct
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    26
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    27
(**** add special syntax for embedding proof terms ****)
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    28
71176
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    29
val proofT = Type ("Pure.proof", []);
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    30
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    31
local
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    32
11614
3131fa12d425 - Tuned syntax
berghofe
parents: 11539
diff changeset
    33
val paramT = Type ("param", []);
3131fa12d425 - Tuned syntax
berghofe
parents: 11539
diff changeset
    34
val paramsT = Type ("params", []);
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    35
val idtT = Type ("idt", []);
70572
wenzelm
parents: 67649
diff changeset
    36
val aT = Term.aT [];
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    37
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    38
fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    39
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    40
in
62752
d09d71223e7a more position information for type mixfix;
wenzelm
parents: 61957
diff changeset
    41
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16350
diff changeset
    42
fun add_proof_syntax thy =
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16350
diff changeset
    43
  thy
22796
34c316d7b630 renamed some old names Theory.xxx to Sign.xxx;
wenzelm
parents: 22675
diff changeset
    44
  |> Sign.root_path
36449
78721f3adb13 modernized/simplified Sign.set_defsort;
wenzelm
parents: 35845
diff changeset
    45
  |> Sign.set_defsort []
56436
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    46
  |> Sign.add_nonterminals_global
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62958
diff changeset
    47
    [Binding.make ("param", \<^here>),
851ae0e7b09c more symbols;
wenzelm
parents: 62958
diff changeset
    48
     Binding.make ("params", \<^here>)]
56240
938c6c7e10eb tuned signature;
wenzelm
parents: 56239
diff changeset
    49
  |> Sign.add_syntax Syntax.mode_default
62752
d09d71223e7a more position information for type mixfix;
wenzelm
parents: 61957
diff changeset
    50
    [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
d09d71223e7a more position information for type mixfix;
wenzelm
parents: 61957
diff changeset
    51
     ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
d09d71223e7a more position information for type mixfix;
wenzelm
parents: 61957
diff changeset
    52
     ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
d09d71223e7a more position information for type mixfix;
wenzelm
parents: 61957
diff changeset
    53
     ("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)),
62761
5c672b22dcc2 clarified simple mixfix;
wenzelm
parents: 62752
diff changeset
    54
     ("", paramT --> paramT, Mixfix.mixfix "'(_')"),
5c672b22dcc2 clarified simple mixfix;
wenzelm
parents: 62752
diff changeset
    55
     ("", idtT --> paramsT, Mixfix.mixfix "_"),
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    56
     ("", paramT --> paramsT, Mixfix.mixfix "_"),
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    57
     (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    58
     (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
70592
e8558735961a clarified syntax;
wenzelm
parents: 70575
diff changeset
    59
     (Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "\<^bold>?")]
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 39557
diff changeset
    60
  |> Sign.add_trrules (map Syntax.Parse_Print_Rule
56436
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    61
    [(Ast.mk_appl (Ast.Constant "_Lam")
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    62
        [Ast.mk_appl (Ast.Constant "_Lam0")
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    63
          [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"],
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    64
      Ast.mk_appl (Ast.Constant "_Lam")
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    65
        [Ast.Variable "l",
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    66
          Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]),
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    67
     (Ast.mk_appl (Ast.Constant "_Lam")
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    68
        [Ast.mk_appl (Ast.Constant "_Lam1")
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    69
          [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    70
      Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.AbsP")) [Ast.Variable "A",
56436
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    71
        (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    72
     (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    73
      Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.Abst"))
56436
30ccec1e82fb more source positions;
wenzelm
parents: 56243
diff changeset
    74
        [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    75
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    76
end;
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    77
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    78
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    79
(** constants for theorems and axioms **)
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    80
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    81
fun add_proof_atom_consts names thy =
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    82
  thy
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    83
  |> Sign.root_path
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    84
  |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
    85
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    86
71176
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    87
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    88
(** proof terms as pure terms **)
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    89
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    90
(* term_of_proof *)
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    91
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    92
local
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    93
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    94
val AbsPt = Const ("Pure.AbsP", propT --> (proofT --> proofT) --> proofT);
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    95
val AppPt = Const ("Pure.AppP", proofT --> proofT --> proofT);
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    96
val Hypt = Const ("Pure.Hyp", propT --> proofT);
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    97
val Oraclet = Const ("Pure.Oracle", propT --> proofT);
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    98
val MinProoft = Const ("Pure.MinProof", proofT);
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
    99
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   100
fun AppT T prf =
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   101
  Const ("Pure.Appt", proofT --> Term.itselfT T --> proofT) $ prf $ Logic.mk_type T;
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   102
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   103
fun OfClasst (T, c) =
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   104
  let val U = Term.itselfT T --> propT
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   105
  in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   106
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   107
fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) =
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   108
      fold AppT (these Ts)
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   109
        (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT))
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   110
  | term_of _ (PAxm (name, _, Ts)) =
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   111
      fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   112
  | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   113
  | term_of _ (PBound i) = Bound i
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   114
  | term_of Ts (Abst (s, opT, prf)) =
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   115
      let val T = the_default dummyT opT in
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   116
        Const ("Pure.Abst", (T --> proofT) --> proofT) $
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   117
          Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf))
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   118
      end
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   119
  | term_of Ts (AbsP (s, t, prf)) =
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   120
      AbsPt $ the_default Term.dummy_prop t $
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   121
        Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf))
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   122
  | term_of Ts (prf1 %% prf2) =
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   123
      AppPt $ term_of Ts prf1 $ term_of Ts prf2
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   124
  | term_of Ts (prf % opt) =
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   125
      let
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   126
        val t = the_default Term.dummy opt;
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   127
        val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   128
      in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   129
  | term_of _ (Hyp t) = Hypt $ t
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   130
  | term_of _ (Oracle (_, t, _)) = Oraclet $ t
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   131
  | term_of _ MinProof = MinProoft;
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   132
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   133
in
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   134
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   135
val term_of_proof = term_of [];
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   136
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   137
end;
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   138
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   139
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   140
(* proof_of_term *)
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   141
28807
9f3ecb4aaac2 proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28375
diff changeset
   142
fun proof_of_term thy ty =
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   143
  let
56161
300f613060b0 tuned signature;
wenzelm
parents: 55725
diff changeset
   144
    val thms = Global_Theory.all_thms_of thy true;
16350
caa9b780ad91 Theory.all_axioms_of, PureThy.all_thms_of;
wenzelm
parents: 16195
diff changeset
   145
    val axms = Theory.all_axioms_of thy;
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   146
20548
8ef25fe585a8 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents: 19618
diff changeset
   147
    fun mk_term t = (if ty then I else map_types (K dummyT))
11614
3131fa12d425 - Tuned syntax
berghofe
parents: 11539
diff changeset
   148
      (Term.no_dummy_patterns t);
3131fa12d425 - Tuned syntax
berghofe
parents: 11539
diff changeset
   149
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   150
    fun prf_of [] (Bound i) = PBound i
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
   151
      | prf_of Ts (Const (s, Type ("Pure.proof", _))) =
70602
eb6ff14767cd tuned signature;
wenzelm
parents: 70597
diff changeset
   152
          Proofterm.change_types (if ty then SOME Ts else NONE)
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30344
diff changeset
   153
            (case Long_Name.explode s of
11614
3131fa12d425 - Tuned syntax
berghofe
parents: 11539
diff changeset
   154
               "axm" :: xs =>
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   155
                 let
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30344
diff changeset
   156
                   val name = Long_Name.implode xs;
17223
430edc6b7826 curried_lookup/update;
wenzelm
parents: 17078
diff changeset
   157
                   val prop = (case AList.lookup (op =) axms name of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   158
                       SOME prop => prop
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   159
                     | NONE => error ("Unknown axiom " ^ quote name))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   160
                 in PAxm (name, prop, NONE) end
11614
3131fa12d425 - Tuned syntax
berghofe
parents: 11539
diff changeset
   161
             | "thm" :: xs =>
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30344
diff changeset
   162
                 let val name = Long_Name.implode xs;
17223
430edc6b7826 curried_lookup/update;
wenzelm
parents: 17078
diff changeset
   163
                 in (case AList.lookup (op =) thms name of
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37236
diff changeset
   164
                     SOME thm =>
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37236
diff changeset
   165
                      fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of thm))))
28807
9f3ecb4aaac2 proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28375
diff changeset
   166
                   | NONE => error ("Unknown theorem " ^ quote name))
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   167
                 end
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   168
             | _ => error ("Illegal proof constant name: " ^ quote s))
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
   169
      | prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) =
31903
c5221dbc40f6 added pro-forma proof constructor Inclass;
wenzelm
parents: 30435
diff changeset
   170
          (case try Logic.class_of_const c_class of
c5221dbc40f6 added pro-forma proof constructor Inclass;
wenzelm
parents: 30435
diff changeset
   171
            SOME c =>
70602
eb6ff14767cd tuned signature;
wenzelm
parents: 70597
diff changeset
   172
              Proofterm.change_types (if ty then SOME Ts else NONE)
31943
5e960a0780a2 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents: 31903
diff changeset
   173
                (OfClass (TVar ((Name.aT, 0), []), c))
31903
c5221dbc40f6 added pro-forma proof constructor Inclass;
wenzelm
parents: 30435
diff changeset
   174
          | NONE => error ("Bad class constant: " ^ quote c_class))
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
   175
      | prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
   176
      | prf_of Ts (v as Var ((_, Type ("Pure.proof", _)))) = Hyp v
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
   177
      | prf_of [] (Const ("Pure.Abst", _) $ Abs (s, T, prf)) =
25245
1fcfcdcba53c Added well-formedness check to Abst case in function prf_of.
berghofe
parents: 24848
diff changeset
   178
          if T = proofT then
1fcfcdcba53c Added well-formedness check to Abst case in function prf_of.
berghofe
parents: 24848
diff changeset
   179
            error ("Term variable abstraction may not bind proof variable " ^ quote s)
1fcfcdcba53c Added well-formedness check to Abst case in function prf_of.
berghofe
parents: 24848
diff changeset
   180
          else Abst (s, if ty then SOME T else NONE,
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37236
diff changeset
   181
            Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf))
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
   182
      | prf_of [] (Const ("Pure.AbsP", _) $ t $ Abs (s, _, prf)) =
11614
3131fa12d425 - Tuned syntax
berghofe
parents: 11539
diff changeset
   183
          AbsP (s, case t of
56241
029246729dc0 more qualified names;
wenzelm
parents: 56240
diff changeset
   184
                Const ("Pure.dummy_pattern", _) => NONE
029246729dc0 more qualified names;
wenzelm
parents: 56240
diff changeset
   185
              | _ $ Const ("Pure.dummy_pattern", _) => NONE
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   186
              | _ => SOME (mk_term t),
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37236
diff changeset
   187
            Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
   188
      | prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) =
11614
3131fa12d425 - Tuned syntax
berghofe
parents: 11539
diff changeset
   189
          prf_of [] prf1 %% prf_of [] prf2
70603
d23cfb85438a proper argument type (amending 42fbb6abed5a);
wenzelm
parents: 70602
diff changeset
   190
      | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type ("itself", [T]))) =
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   191
          prf_of (T::Ts) prf
70573
e31271559de8 global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents: 70572
diff changeset
   192
      | prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf %
56241
029246729dc0 more qualified names;
wenzelm
parents: 56240
diff changeset
   193
          (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   194
      | prf_of _ t = error ("Not a proof term:\n" ^
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26626
diff changeset
   195
          Syntax.string_of_term_global thy t)
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   196
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   197
  in prf_of [] end;
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   198
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   199
37227
bdd8dd217b1f - Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents: 36610
diff changeset
   200
fun read_term thy topsort =
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   201
  let
56161
300f613060b0 tuned signature;
wenzelm
parents: 55725
diff changeset
   202
    val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true));
16350
caa9b780ad91 Theory.all_axioms_of, PureThy.all_thms_of;
wenzelm
parents: 16195
diff changeset
   203
    val axm_names = map fst (Theory.all_axioms_of thy);
27260
17d617c6b026 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents: 26939
diff changeset
   204
    val ctxt = thy
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16350
diff changeset
   205
      |> add_proof_syntax
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16350
diff changeset
   206
      |> add_proof_atom_consts
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30344
diff changeset
   207
        (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42290
diff changeset
   208
      |> Proof_Context.init_global
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42290
diff changeset
   209
      |> Proof_Context.allow_dummies
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42290
diff changeset
   210
      |> Proof_Context.set_mode Proof_Context.mode_schematic
62958
b41c1cb5e251 Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents: 62922
diff changeset
   211
      |> topsort ?
b41c1cb5e251 Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents: 62922
diff changeset
   212
        (Proof_Context.set_defsort [] #>
b41c1cb5e251 Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents: 62922
diff changeset
   213
         Config.put Type_Infer.object_logic false #>
b41c1cb5e251 Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents: 62922
diff changeset
   214
         Config.put Type_Infer_Context.const_sorts false);
27260
17d617c6b026 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents: 26939
diff changeset
   215
  in
17d617c6b026 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents: 26939
diff changeset
   216
    fn ty => fn s =>
17d617c6b026 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents: 26939
diff changeset
   217
      (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
39288
f1ae2493d93f eliminated aliases of Type.constraint;
wenzelm
parents: 37310
diff changeset
   218
      |> Type.constraint ty |> Syntax.check_term ctxt
27260
17d617c6b026 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents: 26939
diff changeset
   219
  end;
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   220
37227
bdd8dd217b1f - Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents: 36610
diff changeset
   221
fun read_proof thy topsort =
bdd8dd217b1f - Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents: 36610
diff changeset
   222
  let val rd = read_term thy topsort proofT
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35262
diff changeset
   223
  in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end;
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   224
17078
db9d24c8b439 export proof_syntax, proof_of;
wenzelm
parents: 17019
diff changeset
   225
fun proof_syntax prf =
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   226
  let
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37236
diff changeset
   227
    val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true
70679
a9053fa30909 clarified ML types;
wenzelm
parents: 70635
diff changeset
   228
      (fn PThm ({name, ...}, _) => if name <> "" then Symtab.update (name, ()) else I
28807
9f3ecb4aaac2 proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28375
diff changeset
   229
        | _ => I) [prf] Symtab.empty);
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37236
diff changeset
   230
    val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true
28807
9f3ecb4aaac2 proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28375
diff changeset
   231
      (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty);
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   232
  in
17078
db9d24c8b439 export proof_syntax, proof_of;
wenzelm
parents: 17019
diff changeset
   233
    add_proof_syntax #>
db9d24c8b439 export proof_syntax, proof_of;
wenzelm
parents: 17019
diff changeset
   234
    add_proof_atom_consts
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30344
diff changeset
   235
      (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   236
  end;
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   237
70635
6e34025981be clarified global theory context;
wenzelm
parents: 70633
diff changeset
   238
fun proof_of full thm =
17078
db9d24c8b439 export proof_syntax, proof_of;
wenzelm
parents: 17019
diff changeset
   239
  let
70635
6e34025981be clarified global theory context;
wenzelm
parents: 70633
diff changeset
   240
    val thy = Thm.theory_of_thm thm;
17078
db9d24c8b439 export proof_syntax, proof_of;
wenzelm
parents: 17019
diff changeset
   241
    val prop = Thm.full_prop_of thm;
28814
463c9e9111ae clarified Thm.proof_body_of vs. Thm.proof_of;
wenzelm
parents: 28807
diff changeset
   242
    val prf = Thm.proof_of thm;
71003
wenzelm
parents: 70679
diff changeset
   243
  in
wenzelm
parents: 70679
diff changeset
   244
    (case fst (Proofterm.strip_combt (fst (Proofterm.strip_combP prf))) of
wenzelm
parents: 70679
diff changeset
   245
      PThm ({prop = prop', ...}, thm_body) =>
wenzelm
parents: 70679
diff changeset
   246
        if prop = prop' then Proofterm.thm_body_proof_raw thm_body else prf
wenzelm
parents: 70679
diff changeset
   247
    | _ => prf)
wenzelm
parents: 70679
diff changeset
   248
    |> full ? Proofterm.reconstruct_proof thy prop
wenzelm
parents: 70679
diff changeset
   249
  end;
17078
db9d24c8b439 export proof_syntax, proof_of;
wenzelm
parents: 17019
diff changeset
   250
27260
17d617c6b026 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents: 26939
diff changeset
   251
fun pretty_proof ctxt prf =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42290
diff changeset
   252
  Proof_Context.pretty_term_abbrev
55725
9d605a21d7ec prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
wenzelm
parents: 52788
diff changeset
   253
    (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
71176
9dab828cbbc1 clarified modules (again);
wenzelm
parents: 71175
diff changeset
   254
    (term_of_proof prf);
17078
db9d24c8b439 export proof_syntax, proof_of;
wenzelm
parents: 17019
diff changeset
   255
71206
be689b7d81fd clarified signature -- more options;
wenzelm
parents: 71176
diff changeset
   256
fun pretty_proof_boxes_of ctxt {full, preproc} thm =
71175
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   257
  let
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   258
    val thy = Proof_Context.theory_of ctxt;
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   259
    val selection =
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   260
      {included = Proofterm.this_id (Thm.derivation_id thm),
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   261
       excluded = is_some o Global_Theory.lookup_thm_id thy}
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   262
  in
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   263
    Proofterm.proof_boxes selection [Thm.proof_of thm]
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   264
    |> map (fn ({serial = i, pos, prop, ...}, proof) =>
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   265
        let
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   266
          val proof' = proof
71206
be689b7d81fd clarified signature -- more options;
wenzelm
parents: 71176
diff changeset
   267
            |> Proofterm.reconstruct_proof thy prop
be689b7d81fd clarified signature -- more options;
wenzelm
parents: 71176
diff changeset
   268
            |> preproc thy
be689b7d81fd clarified signature -- more options;
wenzelm
parents: 71176
diff changeset
   269
            |> not full ? Proofterm.shrink_proof
71175
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   270
            |> Proofterm.forall_intr_variables prop;
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   271
          val prop' = prop
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   272
            |> Proofterm.forall_intr_variables_term;
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   273
          val name = Long_Name.append "thm" (string_of_int i);
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   274
        in
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   275
          Pretty.item
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   276
           [Pretty.str (name ^ Position.here_list pos ^ ":"), Pretty.brk 1,
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   277
            Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof']
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   278
        end)
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   279
    |> Pretty.chunks
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   280
  end;
7abe5abb4c05 more detailed proof term output;
wenzelm
parents: 71105
diff changeset
   281
71286
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   282
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   283
(* standardized proofs *)
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   284
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   285
fun standard_proof_of {full, expand_name} thm =
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   286
  let val thy = Thm.theory_of_thm thm in
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   287
    Thm.reconstruct_proof_of thm
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   288
    |> Proofterm.expand_proof thy expand_name
71288
06c6495fb1d0 retain type information from reconstruct_proof, notably for Export_Theory.export_thm;
wenzelm
parents: 71286
diff changeset
   289
    |> Proofterm.rewrite_proof thy ([], Proof_Rewrite_Rules.rprocs true)
71286
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   290
    |> Proofterm.no_thm_proofs
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   291
    |> not full ? Proofterm.shrink_proof
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   292
  end;
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   293
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   294
fun pretty_standard_proof_of ctxt full thm =
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   295
  pretty_proof ctxt (standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
4b45d592ce29 clarified modules;
wenzelm
parents: 71206
diff changeset
   296
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   297
end;