src/Pure/Proof/proof_syntax.ML
author wenzelm
Fri Oct 07 21:16:48 2016 +0200 (2016-10-07)
changeset 64092 95469c544b82
parent 62958 b41c1cb5e251
child 64556 851ae0e7b09c
permissions -rw-r--r--
accept obscure timezone used in 2011;
     1 (*  Title:      Pure/Proof/proof_syntax.ML
     2     Author:     Stefan Berghofer, TU Muenchen
     3 
     4 Function for parsing and printing proof terms.
     5 *)
     6 
     7 signature PROOF_SYNTAX =
     8 sig
     9   val proofT: typ
    10   val add_proof_syntax: theory -> theory
    11   val proof_of_term: theory -> bool -> term -> Proofterm.proof
    12   val term_of_proof: Proofterm.proof -> term
    13   val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
    14   val read_term: theory -> bool -> typ -> string -> term
    15   val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
    16   val proof_syntax: Proofterm.proof -> theory -> theory
    17   val proof_of: Proof.context -> bool -> thm -> Proofterm.proof
    18   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
    19   val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
    20 end;
    21 
    22 structure Proof_Syntax : PROOF_SYNTAX =
    23 struct
    24 
    25 (**** add special syntax for embedding proof terms ****)
    26 
    27 val proofT = Type ("proof", []);
    28 val paramT = Type ("param", []);
    29 val paramsT = Type ("params", []);
    30 val idtT = Type ("idt", []);
    31 val aT = TFree (Name.aT, []);
    32 
    33 
    34 (** constants for theorems and axioms **)
    35 
    36 fun add_proof_atom_consts names thy =
    37   thy
    38   |> Sign.root_path
    39   |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
    40 
    41 
    42 (** constants for application and abstraction **)
    43 
    44 fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
    45 
    46 fun add_proof_syntax thy =
    47   thy
    48   |> Sign.root_path
    49   |> Sign.set_defsort []
    50   |> Sign.add_types_global
    51     [(Binding.make ("proof", @{here}), 0, NoSyn)]
    52   |> fold (snd oo Sign.declare_const_global)
    53     [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
    54      ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
    55      ((Binding.make ("Abst", @{here}), (aT --> proofT) --> proofT), NoSyn),
    56      ((Binding.make ("AbsP", @{here}), [propT, proofT --> proofT] ---> proofT), NoSyn),
    57      ((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn),
    58      ((Binding.make ("Oracle", @{here}), propT --> proofT), NoSyn),
    59      ((Binding.make ("OfClass", @{here}), (Term.a_itselfT --> propT) --> proofT), NoSyn),
    60      ((Binding.make ("MinProof", @{here}), proofT), Mixfix.mixfix "?")]
    61   |> Sign.add_nonterminals_global
    62     [Binding.make ("param", @{here}),
    63      Binding.make ("params", @{here})]
    64   |> Sign.add_syntax Syntax.mode_default
    65     [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
    66      ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
    67      ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
    68      ("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)),
    69      ("", paramT --> paramT, Mixfix.mixfix "'(_')"),
    70      ("", idtT --> paramsT, Mixfix.mixfix "_"),
    71      ("", paramT --> paramsT, Mixfix.mixfix "_")]
    72   |> Sign.add_syntax (Print_Mode.ASCII, true)
    73     [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)),
    74      (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)),
    75      (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))]
    76   |> Sign.add_trrules (map Syntax.Parse_Print_Rule
    77     [(Ast.mk_appl (Ast.Constant "_Lam")
    78         [Ast.mk_appl (Ast.Constant "_Lam0")
    79           [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"],
    80       Ast.mk_appl (Ast.Constant "_Lam")
    81         [Ast.Variable "l",
    82           Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]),
    83      (Ast.mk_appl (Ast.Constant "_Lam")
    84         [Ast.mk_appl (Ast.Constant "_Lam1")
    85           [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
    86       Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A",
    87         (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
    88      (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
    89       Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst"))
    90         [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
    91 
    92 
    93 (**** translation between proof terms and pure terms ****)
    94 
    95 fun proof_of_term thy ty =
    96   let
    97     val thms = Global_Theory.all_thms_of thy true;
    98     val axms = Theory.all_axioms_of thy;
    99 
   100     fun mk_term t = (if ty then I else map_types (K dummyT))
   101       (Term.no_dummy_patterns t);
   102 
   103     fun prf_of [] (Bound i) = PBound i
   104       | prf_of Ts (Const (s, Type ("proof", _))) =
   105           Proofterm.change_type (if ty then SOME Ts else NONE)
   106             (case Long_Name.explode s of
   107                "axm" :: xs =>
   108                  let
   109                    val name = Long_Name.implode xs;
   110                    val prop = (case AList.lookup (op =) axms name of
   111                        SOME prop => prop
   112                      | NONE => error ("Unknown axiom " ^ quote name))
   113                  in PAxm (name, prop, NONE) end
   114              | "thm" :: xs =>
   115                  let val name = Long_Name.implode xs;
   116                  in (case AList.lookup (op =) thms name of
   117                      SOME thm =>
   118                       fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of thm))))
   119                    | NONE => error ("Unknown theorem " ^ quote name))
   120                  end
   121              | _ => error ("Illegal proof constant name: " ^ quote s))
   122       | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) =
   123           (case try Logic.class_of_const c_class of
   124             SOME c =>
   125               Proofterm.change_type (if ty then SOME Ts else NONE)
   126                 (OfClass (TVar ((Name.aT, 0), []), c))
   127           | NONE => error ("Bad class constant: " ^ quote c_class))
   128       | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
   129       | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
   130       | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
   131           if T = proofT then
   132             error ("Term variable abstraction may not bind proof variable " ^ quote s)
   133           else Abst (s, if ty then SOME T else NONE,
   134             Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf))
   135       | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
   136           AbsP (s, case t of
   137                 Const ("Pure.dummy_pattern", _) => NONE
   138               | _ $ Const ("Pure.dummy_pattern", _) => NONE
   139               | _ => SOME (mk_term t),
   140             Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
   141       | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
   142           prf_of [] prf1 %% prf_of [] prf2
   143       | prf_of Ts (Const ("Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
   144           prf_of (T::Ts) prf
   145       | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
   146           (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
   147       | prf_of _ t = error ("Not a proof term:\n" ^
   148           Syntax.string_of_term_global thy t)
   149 
   150   in prf_of [] end;
   151 
   152 
   153 val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);
   154 val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
   155 val Hypt = Const ("Hyp", propT --> proofT);
   156 val Oraclet = Const ("Oracle", propT --> proofT);
   157 val OfClasst = Const ("OfClass", (Term.itselfT dummyT --> propT) --> proofT);
   158 val MinProoft = Const ("MinProof", proofT);
   159 
   160 val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
   161   [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
   162 
   163 fun term_of _ (PThm (_, ((name, _, NONE), _))) =
   164       Const (Long_Name.append "thm" name, proofT)
   165   | term_of _ (PThm (_, ((name, _, SOME Ts), _))) =
   166       mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT))
   167   | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
   168   | term_of _ (PAxm (name, _, SOME Ts)) =
   169       mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
   170   | term_of _ (OfClass (T, c)) =
   171       mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
   172   | term_of _ (PBound i) = Bound i
   173   | term_of Ts (Abst (s, opT, prf)) =
   174       let val T = the_default dummyT opT
   175       in Const ("Abst", (T --> proofT) --> proofT) $
   176         Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf))
   177       end
   178   | term_of Ts (AbsP (s, t, prf)) =
   179       AbsPt $ the_default Term.dummy_prop t $
   180         Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf))
   181   | term_of Ts (prf1 %% prf2) =
   182       AppPt $ term_of Ts prf1 $ term_of Ts prf2
   183   | term_of Ts (prf % opt) =
   184       let val t = the_default Term.dummy opt
   185       in Const ("Appt",
   186         [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
   187           term_of Ts prf $ t
   188       end
   189   | term_of Ts (Hyp t) = Hypt $ t
   190   | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
   191   | term_of Ts MinProof = MinProoft;
   192 
   193 val term_of_proof = term_of [];
   194 
   195 fun cterm_of_proof thy prf =
   196   let
   197     val thm_names = map fst (Global_Theory.all_thms_of thy true);
   198     val axm_names = map fst (Theory.all_axioms_of thy);
   199     val thy' = thy
   200       |> add_proof_syntax
   201       |> add_proof_atom_consts
   202         (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);
   203   in
   204     (Thm.global_cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
   205   end;
   206 
   207 fun read_term thy topsort =
   208   let
   209     val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true));
   210     val axm_names = map fst (Theory.all_axioms_of thy);
   211     val ctxt = thy
   212       |> add_proof_syntax
   213       |> add_proof_atom_consts
   214         (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
   215       |> Proof_Context.init_global
   216       |> Proof_Context.allow_dummies
   217       |> Proof_Context.set_mode Proof_Context.mode_schematic
   218       |> topsort ?
   219         (Proof_Context.set_defsort [] #>
   220          Config.put Type_Infer.object_logic false #>
   221          Config.put Type_Infer_Context.const_sorts false);
   222   in
   223     fn ty => fn s =>
   224       (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
   225       |> Type.constraint ty |> Syntax.check_term ctxt
   226   end;
   227 
   228 fun read_proof thy topsort =
   229   let val rd = read_term thy topsort proofT
   230   in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end;
   231 
   232 fun proof_syntax prf =
   233   let
   234     val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true
   235       (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I
   236         | _ => I) [prf] Symtab.empty);
   237     val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true
   238       (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty);
   239   in
   240     add_proof_syntax #>
   241     add_proof_atom_consts
   242       (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
   243   end;
   244 
   245 fun proof_of ctxt full raw_thm =
   246   let
   247     val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm;
   248     val prop = Thm.full_prop_of thm;
   249     val prf = Thm.proof_of thm;
   250     val prf' =
   251       (case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of
   252         (PThm (_, ((_, prop', _), body)), _) =>
   253           if prop = prop' then Proofterm.join_proof body else prf
   254       | _ => prf)
   255   in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end;
   256 
   257 fun pretty_proof ctxt prf =
   258   Proof_Context.pretty_term_abbrev
   259     (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
   260     (term_of_proof prf);
   261 
   262 fun pretty_proof_of ctxt full th =
   263   pretty_proof ctxt (proof_of ctxt full th);
   264 
   265 end;