isabelle: src/Pure/Proof/proof_syntax.ML@d8cac577493c

     1 (*  Title:      Pure/Proof/proof_syntax.ML

     2     ID:         $Id$

     3     Author:     Stefan Berghofer, TU Muenchen

     5 Function for parsing and printing proof terms.

     6 *)

     8 signature PROOF_SYNTAX =

     9 sig

    10   val proofT : typ

    11   val add_proof_syntax : Sign.sg -> Sign.sg

    12   val disambiguate_names : theory -> Proofterm.proof ->

    13     Proofterm.proof * Proofterm.proof Symtab.table

    14   val proof_of_term : theory -> Proofterm.proof Symtab.table ->

    15     bool -> term -> Proofterm.proof

    16   val term_of_proof : Proofterm.proof -> term

    17   val cterm_of_proof : theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)

    18   val read_term : theory -> typ -> string -> term

    19   val read_proof : theory -> bool -> string -> Proofterm.proof

    20   val pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T

    21   val pretty_proof_of : bool -> thm -> Pretty.T

    22   val print_proof_of : bool -> thm -> unit

    23 end;

    25 structure ProofSyntax : PROOF_SYNTAX =

    26 struct

    28 open Proofterm;

    30 (**** add special syntax for embedding proof terms ****)

    32 val proofT = Type ("proof", []);

    33 val paramT = Type ("param", []);

    34 val paramsT = Type ("params", []);

    35 val idtT = Type ("idt", []);

    36 val aT = TFree ("'a", []);

    38 (** constants for theorems and axioms **)

    40 fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b);

    42 fun add_proof_atom_consts names sg = Sign.add_consts_i

    43   (map (fn name => (name, proofT, NoSyn)) names) (Sign.add_path "//" sg);

    45 (** constants for application and abstraction **)

    47 fun add_proof_syntax sg =

    48   sg

    49   |> Sign.copy

    50   |> Sign.add_path "/"

    51   |> Sign.add_defsort_i []

    52   |> Sign.add_types [("proof", 0, NoSyn)]

    53   |> Sign.add_consts_i

    54       [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),

    55        ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),

    56        ("Abst", (aT --> proofT) --> proofT, NoSyn),

    57        ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),

    58        ("Hyp", propT --> proofT, NoSyn),

    59        ("Oracle", propT --> proofT, NoSyn),

    60        ("MinProof", proofT, Delimfix "?")]

    61   |> Sign.add_nonterminals ["param", "params"]

    62   |> Sign.add_syntax_i

    63       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),

    64        ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),

    65        ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),

    66        ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),

    67        ("", paramT --> paramT, Delimfix "'(_')"),

    68        ("", idtT --> paramsT, Delimfix "_"),

    69        ("", paramT --> paramsT, Delimfix "_")]

    70   |> Sign.add_modesyntax_i (("xsymbols", true),

    71       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),

    72        ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),

    73        ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))])

    74   |> Sign.add_modesyntax_i (("latex", false),

    75       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))])

    76   |> Sign.add_trrules_i (map Syntax.ParsePrintRule

    77       [(Syntax.mk_appl (Constant "_Lam")

    78           [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],

    79         Syntax.mk_appl (Constant "_Lam")

    80           [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),

    81        (Syntax.mk_appl (Constant "_Lam")

    82           [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],

    83         Syntax.mk_appl (Constant "AbsP") [Variable "A",

    84           (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),

    85        (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],

    86         Syntax.mk_appl (Constant "Abst")

    87           [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);

    90 (**** create unambiguous theorem names ****)

    92 fun disambiguate_names thy prf =

    93   let

    94     val thms = thms_of_proof Symtab.empty prf;

    95     val thms' = map (apsnd (#prop o rep_thm)) (List.concat

    96       (map PureThy.thms_of (thy :: Theory.ancestors_of thy)));

    98     val tab = Symtab.foldl (fn (tab, (key, ps)) =>

    99       let val prop = getOpt (assoc (thms', key), Bound 0)

   100       in fst (foldr (fn ((prop', prf), x as (tab, i)) =>

   101         if prop <> prop' then

   102           (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)

   103         else x) (tab, 1) ps)

   104       end) (Symtab.empty, thms);

   106     fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)

   107       | rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf)

   108       | rename (prf1 %% prf2) = rename prf1 %% rename prf2

   109       | rename (prf % t) = rename prf % t

   110       | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =

   111           let

   112             val prop' = getOpt (assoc (thms', s), Bound 0);

   113             val ps = map fst (valOf (Symtab.lookup (thms, s))) \ prop'

   114           in if prop = prop' then prf' else

   115             PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),

   116               prf, prop, Ts)

   117           end

   118       | rename prf = prf

   120   in (rename prf, tab) end;

   123 (**** translation between proof terms and pure terms ****)

   125 fun proof_of_term thy tab ty =

   126   let

   127     val thys = thy :: Theory.ancestors_of thy;

   128     val thms = List.concat (map thms_of thys);

   129     val axms = List.concat (map (Symtab.dest o #axioms o rep_theory) thys);

   131     fun mk_term t = (if ty then I else map_term_types (K dummyT))

   132       (Term.no_dummy_patterns t);

   134     fun prf_of [] (Bound i) = PBound i

   135       | prf_of Ts (Const (s, Type ("proof", _))) =

   136           change_type (if ty then SOME Ts else NONE)

   137             (case NameSpace.unpack s of

   138                "axm" :: xs =>

   139                  let

   140                    val name = NameSpace.pack xs;

   141                    val prop = (case assoc (axms, name) of

   142                        SOME prop => prop

   143                      | NONE => error ("Unknown axiom " ^ quote name))

   144                  in PAxm (name, prop, NONE) end

   145              | "thm" :: xs =>

   146                  let val name = NameSpace.pack xs;

   147                  in (case assoc (thms, name) of

   148                      SOME thm => fst (strip_combt (Thm.proof_of thm))

   149                    | NONE => (case Symtab.lookup (tab, name) of

   150                          SOME prf => prf

   151                        | NONE => error ("Unknown theorem " ^ quote name)))

   152                  end

   153              | _ => error ("Illegal proof constant name: " ^ quote s))

   154       | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop

   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)

   174   in prf_of [] end;

   177 val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);

   178 val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);

   179 val Hypt = Const ("Hyp", propT --> proofT);

   180 val Oraclet = Const ("Oracle", propT --> proofT);

   181 val MinProoft = Const ("MinProof", proofT);

   183 val mk_tyapp = Library.foldl (fn (prf, T) => Const ("Appt",

   184   [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);

   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 = getOpt (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 $ getOpt (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 = getOpt (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;

   214 val term_of_proof = term_of [];

   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 (List.concat (map thms_of thys))) @

   221       map fst (Symtab.dest tab);

   222     val axm_names = map fst (List.concat (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;

   232 fun read_term thy =

   233   let

   234     val thys = thy :: Theory.ancestors_of thy;

   235     val thm_names = filter_out (equal "") (map fst (List.concat (map thms_of thys)));

   236     val axm_names = map fst (List.concat (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;

   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;

   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;

   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;

   274 val print_proof_of = Pretty.writeln oo pretty_proof_of;

   276 end;

author	wenzelm
	Tue May 31 11:53:40 2005 +0200 (2005-05-31)
changeset 16149	d8cac577493c
parent 15574	b1d1b5bfc464
child 16182	a5c77d298ad7
permissions	-rw-r--r--