berghofe@11522: (* Title: Pure/Proof/proof_syntax.ML wenzelm@11539: Author: Stefan Berghofer, TU Muenchen berghofe@11522: berghofe@11522: Function for parsing and printing proof terms. berghofe@11522: *) berghofe@11522: berghofe@11522: signature PROOF_SYNTAX = berghofe@11522: sig wenzelm@17078: val proofT: typ wenzelm@17078: val add_proof_syntax: theory -> theory wenzelm@28807: val proof_of_term: theory -> bool -> term -> Proofterm.proof wenzelm@17078: val term_of_proof: Proofterm.proof -> term wenzelm@17078: val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) wenzelm@17078: val read_term: theory -> typ -> string -> term wenzelm@17078: val read_proof: theory -> bool -> string -> Proofterm.proof wenzelm@17078: val proof_syntax: Proofterm.proof -> theory -> theory wenzelm@17078: val proof_of: bool -> thm -> Proofterm.proof wenzelm@27260: val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T wenzelm@27260: val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T berghofe@11522: end; berghofe@11522: berghofe@11522: structure ProofSyntax : PROOF_SYNTAX = berghofe@11522: struct berghofe@11522: berghofe@11522: open Proofterm; berghofe@11522: berghofe@11522: (**** add special syntax for embedding proof terms ****) berghofe@11522: berghofe@11522: val proofT = Type ("proof", []); berghofe@11614: val paramT = Type ("param", []); berghofe@11614: val paramsT = Type ("params", []); berghofe@11522: val idtT = Type ("idt", []); wenzelm@24848: val aT = TFree (Name.aT, []); berghofe@11522: berghofe@11522: (** constants for theorems and axioms **) berghofe@11522: wenzelm@16425: fun add_proof_atom_consts names thy = wenzelm@16425: thy wenzelm@30435: |> Sign.root_path wenzelm@30435: |> Sign.add_consts_i (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); berghofe@11522: berghofe@11522: (** constants for application and abstraction **) berghofe@11614: wenzelm@16425: fun add_proof_syntax thy = wenzelm@16425: thy wenzelm@16425: |> Theory.copy wenzelm@22796: |> Sign.root_path wenzelm@22796: |> Sign.add_defsort_i [] wenzelm@30344: |> Sign.add_types [(Binding.name "proof", 0, NoSyn)] wenzelm@22796: |> Sign.add_consts_i wenzelm@30344: [(Binding.name "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)), wenzelm@30344: (Binding.name "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)), wenzelm@30344: (Binding.name "Abst", (aT --> proofT) --> proofT, NoSyn), wenzelm@30344: (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn), wenzelm@30344: (Binding.name "Hyp", propT --> proofT, NoSyn), wenzelm@30344: (Binding.name "Oracle", propT --> proofT, NoSyn), wenzelm@31903: (Binding.name "Inclass", (Term.a_itselfT --> propT) --> proofT, NoSyn), wenzelm@30344: (Binding.name "MinProof", proofT, Delimfix "?")] wenzelm@30344: |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"] wenzelm@22796: |> Sign.add_syntax_i berghofe@11640: [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), berghofe@11614: ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), berghofe@11614: ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), berghofe@11614: ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)), berghofe@11614: ("", paramT --> paramT, Delimfix "'(_')"), berghofe@11614: ("", idtT --> paramsT, Delimfix "_"), berghofe@11614: ("", paramT --> paramsT, Delimfix "_")] wenzelm@22796: |> Sign.add_modesyntax_i ("xsymbols", true) berghofe@11640: [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\_./ _)", [0, 3], 3)), berghofe@11522: ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), wenzelm@16425: ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] wenzelm@22796: |> Sign.add_modesyntax_i ("latex", false) wenzelm@16425: [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\_./ _)", [0, 3], 3))] wenzelm@22796: |> Sign.add_trrules_i (map Syntax.ParsePrintRule berghofe@11522: [(Syntax.mk_appl (Constant "_Lam") berghofe@11614: [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"], berghofe@11614: Syntax.mk_appl (Constant "_Lam") berghofe@11614: [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]), berghofe@11614: (Syntax.mk_appl (Constant "_Lam") berghofe@11522: [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"], berghofe@11522: Syntax.mk_appl (Constant "AbsP") [Variable "A", berghofe@11522: (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]), berghofe@11614: (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"], berghofe@11522: Syntax.mk_appl (Constant "Abst") berghofe@11614: [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]); berghofe@11522: berghofe@11522: berghofe@11522: (**** translation between proof terms and pure terms ****) berghofe@11522: wenzelm@28807: fun proof_of_term thy ty = berghofe@11522: let wenzelm@16350: val thms = PureThy.all_thms_of thy; wenzelm@16350: val axms = Theory.all_axioms_of thy; berghofe@11522: wenzelm@20548: fun mk_term t = (if ty then I else map_types (K dummyT)) berghofe@11614: (Term.no_dummy_patterns t); berghofe@11614: berghofe@11522: fun prf_of [] (Bound i) = PBound i berghofe@11522: | prf_of Ts (Const (s, Type ("proof", _))) = skalberg@15531: change_type (if ty then SOME Ts else NONE) wenzelm@30364: (case Long_Name.explode s of berghofe@11614: "axm" :: xs => berghofe@11522: let wenzelm@30364: val name = Long_Name.implode xs; wenzelm@17223: val prop = (case AList.lookup (op =) axms name of skalberg@15531: SOME prop => prop skalberg@15531: | NONE => error ("Unknown axiom " ^ quote name)) skalberg@15531: in PAxm (name, prop, NONE) end berghofe@11614: | "thm" :: xs => wenzelm@30364: let val name = Long_Name.implode xs; wenzelm@17223: in (case AList.lookup (op =) thms name of wenzelm@28814: SOME thm => fst (strip_combt (Thm.proof_of thm)) wenzelm@28807: | NONE => error ("Unknown theorem " ^ quote name)) berghofe@11522: end berghofe@11522: | _ => error ("Illegal proof constant name: " ^ quote s)) wenzelm@31903: | prf_of Ts (Const ("Inclass", _) $ Const (c_class, _)) = wenzelm@31903: (case try Logic.class_of_const c_class of wenzelm@31903: SOME c => wenzelm@31903: change_type (if ty then SOME Ts else NONE) wenzelm@31903: (Inclass (TVar ((Name.aT, 0), []), c)) wenzelm@31903: | NONE => error ("Bad class constant: " ^ quote c_class)) berghofe@13199: | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop berghofe@11522: | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v berghofe@11522: | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) = berghofe@25245: if T = proofT then berghofe@25245: error ("Term variable abstraction may not bind proof variable " ^ quote s) berghofe@25245: else Abst (s, if ty then SOME T else NONE, berghofe@11522: incr_pboundvars (~1) 0 (prf_of [] prf)) berghofe@11522: | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) = berghofe@11614: AbsP (s, case t of skalberg@15531: Const ("dummy_pattern", _) => NONE skalberg@15531: | _ $ Const ("dummy_pattern", _) => NONE skalberg@15531: | _ => SOME (mk_term t), berghofe@11522: incr_pboundvars 0 (~1) (prf_of [] prf)) berghofe@11522: | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = berghofe@11614: prf_of [] prf1 %% prf_of [] prf2 berghofe@11522: | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) = berghofe@11522: prf_of (T::Ts) prf berghofe@11614: | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % skalberg@15531: (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t)) berghofe@11522: | prf_of _ t = error ("Not a proof term:\n" ^ wenzelm@26939: Syntax.string_of_term_global thy t) berghofe@11522: berghofe@11522: in prf_of [] end; berghofe@11522: berghofe@11522: berghofe@11522: val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT); berghofe@11522: val AppPt = Const ("AppP", [proofT, proofT] ---> proofT); berghofe@13199: val Hypt = Const ("Hyp", propT --> proofT); berghofe@13199: val Oraclet = Const ("Oracle", propT --> proofT); wenzelm@31903: val Inclasst = Const ("Inclass", (Term.itselfT dummyT --> propT) --> proofT); berghofe@13199: val MinProoft = Const ("MinProof", proofT); berghofe@11522: wenzelm@19473: val mk_tyapp = fold (fn T => fn prf => Const ("Appt", wenzelm@19391: [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); berghofe@11522: wenzelm@28807: fun term_of _ (PThm (_, ((name, _, NONE), _))) = wenzelm@30364: Const (Long_Name.append "thm" name, proofT) wenzelm@28807: | term_of _ (PThm (_, ((name, _, SOME Ts), _))) = wenzelm@30364: mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT)) wenzelm@30364: | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT) skalberg@15531: | term_of _ (PAxm (name, _, SOME Ts)) = wenzelm@30364: mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT)) wenzelm@31903: | term_of _ (Inclass (T, c)) = wenzelm@31903: mk_tyapp [T] (Inclasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT)) berghofe@11522: | term_of _ (PBound i) = Bound i wenzelm@27260: | term_of Ts (Abst (s, opT, prf)) = wenzelm@18939: let val T = the_default dummyT opT berghofe@11522: in Const ("Abst", (T --> proofT) --> proofT) $ berghofe@11522: Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf)) berghofe@11522: end berghofe@11522: | term_of Ts (AbsP (s, t, prf)) = wenzelm@18939: AbsPt $ the_default (Term.dummy_pattern propT) t $ berghofe@11522: Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf)) berghofe@11614: | term_of Ts (prf1 %% prf2) = berghofe@11522: AppPt $ term_of Ts prf1 $ term_of Ts prf2 wenzelm@27260: | term_of Ts (prf % opt) = wenzelm@18939: let val t = the_default (Term.dummy_pattern dummyT) opt berghofe@11522: in Const ("Appt", berghofe@11522: [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $ berghofe@11522: term_of Ts prf $ t berghofe@11522: end berghofe@11522: | term_of Ts (Hyp t) = Hypt $ t berghofe@11522: | term_of Ts (Oracle (_, t, _)) = Oraclet $ t wenzelm@28807: | term_of Ts MinProof = MinProoft; berghofe@11522: berghofe@11522: val term_of_proof = term_of []; berghofe@11522: berghofe@11522: fun cterm_of_proof thy prf = berghofe@11522: let wenzelm@28807: val thm_names = map fst (PureThy.all_thms_of thy); wenzelm@16350: val axm_names = map fst (Theory.all_axioms_of thy); wenzelm@16425: val thy' = thy wenzelm@16425: |> add_proof_syntax wenzelm@16425: |> add_proof_atom_consts wenzelm@30364: (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names); berghofe@11522: in wenzelm@28807: (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) berghofe@11522: end; berghofe@11522: berghofe@11522: fun read_term thy = berghofe@11522: let wenzelm@28375: val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy)); wenzelm@16350: val axm_names = map fst (Theory.all_axioms_of thy); wenzelm@27260: val ctxt = thy wenzelm@16425: |> add_proof_syntax wenzelm@16425: |> add_proof_atom_consts wenzelm@30364: (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) wenzelm@27260: |> ProofContext.init wenzelm@27260: |> ProofContext.allow_dummies wenzelm@27260: |> ProofContext.set_mode ProofContext.mode_schematic; wenzelm@27260: in wenzelm@27260: fn ty => fn s => wenzelm@27260: (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s wenzelm@27260: |> TypeInfer.constrain ty |> Syntax.check_term ctxt wenzelm@27260: end; berghofe@11522: berghofe@11522: fun read_proof thy = berghofe@11522: let val rd = read_term thy proofT wenzelm@28807: in fn ty => fn s => proof_of_term thy ty (Logic.varify (rd s)) end; berghofe@11522: wenzelm@17078: fun proof_syntax prf = berghofe@11522: let wenzelm@28807: val thm_names = Symtab.keys (fold_proof_atoms true wenzelm@28807: (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I wenzelm@28807: | _ => I) [prf] Symtab.empty); wenzelm@28807: val axm_names = Symtab.keys (fold_proof_atoms true wenzelm@28807: (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); berghofe@11522: in wenzelm@17078: add_proof_syntax #> wenzelm@17078: add_proof_atom_consts wenzelm@30364: (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) berghofe@11522: end; berghofe@11522: wenzelm@17078: fun proof_of full thm = wenzelm@17078: let wenzelm@26626: val thy = Thm.theory_of_thm thm; wenzelm@17078: val prop = Thm.full_prop_of thm; wenzelm@28814: val prf = Thm.proof_of thm; wenzelm@17078: val prf' = (case strip_combt (fst (strip_combP prf)) of wenzelm@29635: (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then join_proof body else prf wenzelm@17078: | _ => prf) wenzelm@17078: in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end; wenzelm@17078: wenzelm@27260: fun pretty_proof ctxt prf = wenzelm@27260: ProofContext.pretty_term_abbrev wenzelm@27260: (ProofContext.transfer_syntax (proof_syntax prf (ProofContext.theory_of ctxt)) ctxt) wenzelm@27260: (term_of_proof prf); wenzelm@17078: wenzelm@27260: fun pretty_proof_of ctxt full th = wenzelm@27260: pretty_proof ctxt (proof_of full th); berghofe@11522: berghofe@11522: end;