src/Pure/Proof/proof_syntax.ML
author berghofe
Fri Sep 28 11:07:40 2001 +0200 (2001-09-28)
changeset 11614 3131fa12d425
parent 11539 0f17da240450
child 11640 be1bc3b88480
permissions -rw-r--r--
- Tuned syntax
- proof_of_term: fixed problems with dummy patterns and typing information
     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 ("(3Lam _./ _)", [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 ("(3\\<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_trrules_i (map Syntax.ParsePrintRule
    74       [(Syntax.mk_appl (Constant "_Lam")
    75           [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
    76         Syntax.mk_appl (Constant "_Lam")
    77           [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
    78        (Syntax.mk_appl (Constant "_Lam")
    79           [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
    80         Syntax.mk_appl (Constant "AbsP") [Variable "A",
    81           (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
    82        (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
    83         Syntax.mk_appl (Constant "Abst")
    84           [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
    85 
    86 
    87 (**** create unambiguous theorem names ****)
    88 
    89 fun disambiguate_names thy prf =
    90   let
    91     val thms = thms_of_proof Symtab.empty prf;
    92     val thms' = map (apsnd (#prop o rep_thm)) (flat
    93       (map PureThy.thms_of (thy :: Theory.ancestors_of thy)));
    94 
    95     val tab = Symtab.foldl (fn (tab, (key, ps)) =>
    96       let val prop = if_none (assoc (thms', key)) (Bound 0)
    97       in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
    98         if prop <> prop' then
    99           (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
   100         else x) (ps, (tab, 1)))
   101       end) (Symtab.empty, thms);
   102 
   103     fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)
   104       | rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf)
   105       | rename (prf1 %% prf2) = rename prf1 %% rename prf2
   106       | rename (prf % t) = rename prf % t
   107       | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
   108           let
   109             val prop' = if_none (assoc (thms', s)) (Bound 0);
   110             val ps = map fst (the (Symtab.lookup (thms, s))) \ prop'
   111           in if prop = prop' then prf' else
   112             PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
   113               prf, prop, Ts)
   114           end
   115       | rename prf = prf
   116 
   117   in (rename prf, tab) end;
   118 
   119 
   120 (**** translation between proof terms and pure terms ****)
   121 
   122 fun change_type T (PThm (name, prf, prop, _)) = PThm (name, prf, prop, T)
   123   | change_type T (PAxm (name, prop, _)) = PAxm (name, prop, T)
   124   | change_type _ _ = error "Not a proper theorem";
   125 
   126 fun proof_of_term thy tab ty =
   127   let
   128     val thys = thy :: Theory.ancestors_of thy;
   129     val thms = flat (map thms_of thys);
   130     val axms = flat (map (Symtab.dest o #axioms o rep_theory) thys);
   131 
   132     fun mk_term t = (if ty then I else map_term_types (K dummyT))
   133       (Term.no_dummy_patterns t);
   134 
   135     fun prf_of [] (Bound i) = PBound i
   136       | prf_of Ts (Const (s, Type ("proof", _))) =
   137           change_type (if ty then Some Ts else None)
   138             (case NameSpace.unpack s of
   139                "axm" :: xs =>
   140                  let
   141                    val name = NameSpace.pack xs;
   142                    val prop = (case assoc (axms, name) of
   143                        Some prop => prop
   144                      | None => error ("Unknown axiom " ^ quote name))
   145                  in PAxm (name, prop, None) end
   146              | "thm" :: xs =>
   147                  let val name = NameSpace.pack xs;
   148                  in (case assoc (thms, name) of
   149                      Some thm => fst (strip_combt (#2 (#der (rep_thm thm))))
   150                    | None => (case Symtab.lookup (tab, name) of
   151                          Some prf => prf
   152                        | None => error ("Unknown theorem " ^ quote name)))
   153                  end
   154              | _ => error ("Illegal proof constant name: " ^ quote s))
   155       | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
   156       | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
   157           Abst (s, if ty then Some T else None,
   158             incr_pboundvars (~1) 0 (prf_of [] prf))
   159       | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
   160           AbsP (s, case t of
   161                 Const ("dummy_pattern", _) => None
   162               | _ $ Const ("dummy_pattern", _) => None
   163               | _ => Some (mk_term t),
   164             incr_pboundvars 0 (~1) (prf_of [] prf))
   165       | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
   166           prf_of [] prf1 %% prf_of [] prf2
   167       | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
   168           prf_of (T::Ts) prf
   169       | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
   170           (case t of Const ("dummy_pattern", _) => None | _ => Some (mk_term t))
   171       | prf_of _ t = error ("Not a proof term:\n" ^
   172           Sign.string_of_term (sign_of thy) t)
   173 
   174   in prf_of [] end;
   175 
   176 
   177 val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);
   178 val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
   179 val Hypt = Free ("Hyp", propT --> proofT);
   180 val Oraclet = Free ("Oracle", propT --> proofT);
   181 val MinProoft = Free ("?", proofT);
   182 
   183 val mk_tyapp = foldl (fn (prf, T) => Const ("Appt",
   184   [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
   185 
   186 fun term_of _ (PThm ((name, _), _, _, None)) =
   187       Const (add_prefix "thm" name, proofT)
   188   | term_of _ (PThm ((name, _), _, _, Some Ts)) =
   189       mk_tyapp (Const (add_prefix "thm" name, proofT), Ts)
   190   | term_of _ (PAxm (name, _, None)) = Const (add_prefix "axm" name, proofT)
   191   | term_of _ (PAxm (name, _, Some Ts)) =
   192       mk_tyapp (Const (add_prefix "axm" name, proofT), Ts)
   193   | term_of _ (PBound i) = Bound i
   194   | term_of Ts (Abst (s, opT, prf)) = 
   195       let val T = if_none opT dummyT
   196       in Const ("Abst", (T --> proofT) --> proofT) $
   197         Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
   198       end
   199   | term_of Ts (AbsP (s, t, prf)) =
   200       AbsPt $ if_none t (Const ("dummy_pattern", propT)) $
   201         Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
   202   | term_of Ts (prf1 %% prf2) =
   203       AppPt $ term_of Ts prf1 $ term_of Ts prf2
   204   | term_of Ts (prf % opt) = 
   205       let val t = if_none opt (Const ("dummy_pattern", dummyT))
   206       in Const ("Appt",
   207         [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
   208           term_of Ts prf $ t
   209       end
   210   | term_of Ts (Hyp t) = Hypt $ t
   211   | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
   212   | term_of Ts (MinProof _) = MinProoft;
   213 
   214 val term_of_proof = term_of [];
   215 
   216 fun cterm_of_proof thy prf =
   217   let
   218     val (prf', tab) = disambiguate_names thy prf;
   219     val thys = thy :: Theory.ancestors_of thy;
   220     val thm_names = filter_out (equal "") (map fst (flat (map thms_of thys))) @
   221       map fst (Symtab.dest tab);
   222     val axm_names = map fst (flat (map (Symtab.dest o #axioms o rep_theory) thys));
   223     val sg = sign_of thy |>
   224       add_proof_syntax |>
   225       add_proof_atom_consts
   226         (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   227   in
   228     (cterm_of sg (term_of_proof prf'),
   229      proof_of_term thy tab true o Thm.term_of)
   230   end;
   231 
   232 fun read_term thy =
   233   let
   234     val thys = thy :: Theory.ancestors_of thy;
   235     val thm_names = filter_out (equal "") (map fst (flat (map thms_of thys)));
   236     val axm_names = map fst (flat (map (Symtab.dest o #axioms o rep_theory) thys));
   237     val sg = sign_of thy |>
   238       add_proof_syntax |>
   239       add_proof_atom_consts
   240         (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   241   in
   242     (fn T => fn s => Thm.term_of (read_cterm sg (s, T)))
   243   end;
   244 
   245 fun read_proof thy =
   246   let val rd = read_term thy proofT
   247   in
   248     (fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s)))
   249   end;
   250 
   251 fun pretty_proof sg prf =
   252   let
   253     val thm_names = map fst (Symtab.dest (thms_of_proof Symtab.empty prf)) \ "";
   254     val axm_names = map fst (Symtab.dest (axms_of_proof Symtab.empty prf));
   255     val sg' = sg |>
   256       add_proof_syntax |>
   257       add_proof_atom_consts
   258         (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   259   in
   260     Sign.pretty_term sg' (term_of_proof prf)
   261   end;
   262 
   263 fun pretty_proof_of full thm =
   264   let
   265     val {sign, der = (_, prf), prop, ...} = rep_thm thm;
   266     val prf' = (case strip_combt (fst (strip_combP prf)) of
   267         (PThm (_, prf', prop', _), _) => if prop=prop' then prf' else prf
   268       | _ => prf)
   269   in
   270     pretty_proof sign
   271       (if full then Reconstruct.reconstruct_proof sign prop prf' else prf')
   272   end;
   273 
   274 val print_proof_of = Pretty.writeln oo pretty_proof_of;
   275 
   276 end;