src/Pure/Proof/proof_syntax.ML
author wenzelm
Fri Oct 19 22:02:02 2001 +0200 (2001-10-19)
changeset 11839 3ef83c265aca
parent 11640 be1bc3b88480
child 12909 d3ad295a087a
permissions -rw-r--r--
latex output: bold lambda;
     1 (*  Title:      Pure/Proof/proof_syntax.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Function for parsing and printing proof terms.
     7 *)
     8 
     9 signature PROOF_SYNTAX =
    10 sig
    11   val proofT : typ
    12   val add_proof_syntax : Sign.sg -> Sign.sg
    13   val disambiguate_names : theory -> Proofterm.proof ->
    14     Proofterm.proof * Proofterm.proof Symtab.table
    15   val proof_of_term : theory -> Proofterm.proof Symtab.table ->
    16     bool -> term -> Proofterm.proof
    17   val term_of_proof : Proofterm.proof -> term
    18   val cterm_of_proof : theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
    19   val read_term : theory -> typ -> string -> term
    20   val read_proof : theory -> bool -> string -> Proofterm.proof
    21   val pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
    22   val pretty_proof_of : bool -> thm -> Pretty.T
    23   val print_proof_of : bool -> thm -> unit
    24 end;
    25 
    26 structure ProofSyntax : PROOF_SYNTAX =
    27 struct
    28 
    29 open Proofterm;
    30 
    31 (**** add special syntax for embedding proof terms ****)
    32 
    33 val proofT = Type ("proof", []);
    34 val paramT = Type ("param", []);
    35 val paramsT = Type ("params", []);
    36 val idtT = Type ("idt", []);
    37 val aT = TFree ("'a", ["logic"]);
    38 
    39 (** constants for theorems and axioms **)
    40 
    41 fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b);
    42 
    43 fun add_proof_atom_consts names sg = Sign.add_consts_i
    44   (map (fn name => (name, proofT, NoSyn)) names) (Sign.add_path "//" sg);
    45 
    46 (** constants for application and abstraction **)
    47 
    48 fun add_proof_syntax sg =
    49   sg
    50   |> Sign.copy
    51   |> Sign.add_path "/"
    52   |> Sign.add_defsort_i ["logic"]
    53   |> Sign.add_types [("proof", 0, NoSyn)]
    54   |> Sign.add_arities [("proof", [], "logic")]
    55   |> Sign.add_consts_i
    56       [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
    57        ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
    58        ("Abst", (aT --> proofT) --> proofT, NoSyn),
    59        ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn)]
    60   |> Sign.add_nonterminals ["param", "params"]
    61   |> Sign.add_syntax_i
    62       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
    63        ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    64        ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    65        ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
    66        ("", paramT --> paramT, Delimfix "'(_')"),
    67        ("", idtT --> paramsT, Delimfix "_"),
    68        ("", paramT --> paramsT, Delimfix "_")]
    69   |> Sign.add_modesyntax_i (("xsymbols", true),
    70       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
    71        ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
    72        ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))])
    73   |> Sign.add_modesyntax_i (("latex", false),
    74       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))])
    75   |> Sign.add_trrules_i (map Syntax.ParsePrintRule
    76       [(Syntax.mk_appl (Constant "_Lam")
    77           [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
    78         Syntax.mk_appl (Constant "_Lam")
    79           [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
    80        (Syntax.mk_appl (Constant "_Lam")
    81           [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
    82         Syntax.mk_appl (Constant "AbsP") [Variable "A",
    83           (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
    84        (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
    85         Syntax.mk_appl (Constant "Abst")
    86           [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
    87 
    88 
    89 (**** create unambiguous theorem names ****)
    90 
    91 fun disambiguate_names thy prf =
    92   let
    93     val thms = thms_of_proof Symtab.empty prf;
    94     val thms' = map (apsnd (#prop o rep_thm)) (flat
    95       (map PureThy.thms_of (thy :: Theory.ancestors_of thy)));
    96 
    97     val tab = Symtab.foldl (fn (tab, (key, ps)) =>
    98       let val prop = if_none (assoc (thms', key)) (Bound 0)
    99       in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
   100         if prop <> prop' then
   101           (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
   102         else x) (ps, (tab, 1)))
   103       end) (Symtab.empty, thms);
   104 
   105     fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)
   106       | rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf)
   107       | rename (prf1 %% prf2) = rename prf1 %% rename prf2
   108       | rename (prf % t) = rename prf % t
   109       | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
   110           let
   111             val prop' = if_none (assoc (thms', s)) (Bound 0);
   112             val ps = map fst (the (Symtab.lookup (thms, s))) \ prop'
   113           in if prop = prop' then prf' else
   114             PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
   115               prf, prop, Ts)
   116           end
   117       | rename prf = prf
   118 
   119   in (rename prf, tab) end;
   120 
   121 
   122 (**** translation between proof terms and pure terms ****)
   123 
   124 fun change_type T (PThm (name, prf, prop, _)) = PThm (name, prf, prop, T)
   125   | change_type T (PAxm (name, prop, _)) = PAxm (name, prop, T)
   126   | change_type _ _ = error "Not a proper theorem";
   127 
   128 fun proof_of_term thy tab ty =
   129   let
   130     val thys = thy :: Theory.ancestors_of thy;
   131     val thms = flat (map thms_of thys);
   132     val axms = flat (map (Symtab.dest o #axioms o rep_theory) thys);
   133 
   134     fun mk_term t = (if ty then I else map_term_types (K dummyT))
   135       (Term.no_dummy_patterns t);
   136 
   137     fun prf_of [] (Bound i) = PBound i
   138       | prf_of Ts (Const (s, Type ("proof", _))) =
   139           change_type (if ty then Some Ts else None)
   140             (case NameSpace.unpack s of
   141                "axm" :: xs =>
   142                  let
   143                    val name = NameSpace.pack xs;
   144                    val prop = (case assoc (axms, name) of
   145                        Some prop => prop
   146                      | None => error ("Unknown axiom " ^ quote name))
   147                  in PAxm (name, prop, None) end
   148              | "thm" :: xs =>
   149                  let val name = NameSpace.pack xs;
   150                  in (case assoc (thms, name) of
   151                      Some thm => fst (strip_combt (#2 (#der (rep_thm thm))))
   152                    | None => (case Symtab.lookup (tab, name) of
   153                          Some prf => prf
   154                        | None => error ("Unknown theorem " ^ quote name)))
   155                  end
   156              | _ => error ("Illegal proof constant name: " ^ quote s))
   157       | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
   158       | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
   159           Abst (s, if ty then Some T else None,
   160             incr_pboundvars (~1) 0 (prf_of [] prf))
   161       | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
   162           AbsP (s, case t of
   163                 Const ("dummy_pattern", _) => None
   164               | _ $ Const ("dummy_pattern", _) => None
   165               | _ => Some (mk_term t),
   166             incr_pboundvars 0 (~1) (prf_of [] prf))
   167       | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
   168           prf_of [] prf1 %% prf_of [] prf2
   169       | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
   170           prf_of (T::Ts) prf
   171       | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
   172           (case t of Const ("dummy_pattern", _) => None | _ => Some (mk_term t))
   173       | prf_of _ t = error ("Not a proof term:\n" ^
   174           Sign.string_of_term (sign_of thy) t)
   175 
   176   in prf_of [] end;
   177 
   178 
   179 val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);
   180 val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
   181 val Hypt = Free ("Hyp", propT --> proofT);
   182 val Oraclet = Free ("Oracle", propT --> proofT);
   183 val MinProoft = Free ("?", proofT);
   184 
   185 val mk_tyapp = foldl (fn (prf, T) => Const ("Appt",
   186   [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
   187 
   188 fun term_of _ (PThm ((name, _), _, _, None)) =
   189       Const (add_prefix "thm" name, proofT)
   190   | term_of _ (PThm ((name, _), _, _, Some Ts)) =
   191       mk_tyapp (Const (add_prefix "thm" name, proofT), Ts)
   192   | term_of _ (PAxm (name, _, None)) = Const (add_prefix "axm" name, proofT)
   193   | term_of _ (PAxm (name, _, Some Ts)) =
   194       mk_tyapp (Const (add_prefix "axm" name, proofT), Ts)
   195   | term_of _ (PBound i) = Bound i
   196   | term_of Ts (Abst (s, opT, prf)) = 
   197       let val T = if_none opT dummyT
   198       in Const ("Abst", (T --> proofT) --> proofT) $
   199         Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
   200       end
   201   | term_of Ts (AbsP (s, t, prf)) =
   202       AbsPt $ if_none t (Const ("dummy_pattern", propT)) $
   203         Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
   204   | term_of Ts (prf1 %% prf2) =
   205       AppPt $ term_of Ts prf1 $ term_of Ts prf2
   206   | term_of Ts (prf % opt) = 
   207       let val t = if_none opt (Const ("dummy_pattern", dummyT))
   208       in Const ("Appt",
   209         [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
   210           term_of Ts prf $ t
   211       end
   212   | term_of Ts (Hyp t) = Hypt $ t
   213   | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
   214   | term_of Ts (MinProof _) = MinProoft;
   215 
   216 val term_of_proof = term_of [];
   217 
   218 fun cterm_of_proof thy prf =
   219   let
   220     val (prf', tab) = disambiguate_names thy prf;
   221     val thys = thy :: Theory.ancestors_of thy;
   222     val thm_names = filter_out (equal "") (map fst (flat (map thms_of thys))) @
   223       map fst (Symtab.dest tab);
   224     val axm_names = map fst (flat (map (Symtab.dest o #axioms o rep_theory) thys));
   225     val sg = sign_of thy |>
   226       add_proof_syntax |>
   227       add_proof_atom_consts
   228         (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   229   in
   230     (cterm_of sg (term_of_proof prf'),
   231      proof_of_term thy tab true o Thm.term_of)
   232   end;
   233 
   234 fun read_term thy =
   235   let
   236     val thys = thy :: Theory.ancestors_of thy;
   237     val thm_names = filter_out (equal "") (map fst (flat (map thms_of thys)));
   238     val axm_names = map fst (flat (map (Symtab.dest o #axioms o rep_theory) thys));
   239     val sg = sign_of thy |>
   240       add_proof_syntax |>
   241       add_proof_atom_consts
   242         (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   243   in
   244     (fn T => fn s => Thm.term_of (read_cterm sg (s, T)))
   245   end;
   246 
   247 fun read_proof thy =
   248   let val rd = read_term thy proofT
   249   in
   250     (fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s)))
   251   end;
   252 
   253 fun pretty_proof sg prf =
   254   let
   255     val thm_names = map fst (Symtab.dest (thms_of_proof Symtab.empty prf)) \ "";
   256     val axm_names = map fst (Symtab.dest (axms_of_proof Symtab.empty prf));
   257     val sg' = sg |>
   258       add_proof_syntax |>
   259       add_proof_atom_consts
   260         (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   261   in
   262     Sign.pretty_term sg' (term_of_proof prf)
   263   end;
   264 
   265 fun pretty_proof_of full thm =
   266   let
   267     val {sign, der = (_, prf), prop, ...} = rep_thm thm;
   268     val prf' = (case strip_combt (fst (strip_combP prf)) of
   269         (PThm (_, prf', prop', _), _) => if prop=prop' then prf' else prf
   270       | _ => prf)
   271   in
   272     pretty_proof sign
   273       (if full then Reconstruct.reconstruct_proof sign prop prf' else prf')
   274   end;
   275 
   276 val print_proof_of = Pretty.writeln oo pretty_proof_of;
   277 
   278 end;