11522

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


2 
ID: $Id$

11539

3 
Author: Stefan Berghofer, TU Muenchen


4 
License: GPL (GNU GENERAL PUBLIC LICENSE)

11522

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", []);

11614

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


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

11522

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 **)

11614

47 

11522

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

11614

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


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

11522

58 
("Abst", (aT > proofT) > proofT, NoSyn),


59 
("AbsP", [propT, proofT > proofT] > proofT, NoSyn)]

11614

60 
> Sign.add_nonterminals ["param", "params"]

11522

61 
> Sign.add_syntax_i

11614

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 "_")]

11522

69 
> Sign.add_modesyntax_i (("xsymbols", true),

11614

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

11522

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")

11614

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")

11522

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"])]),

11614

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

11522

83 
Syntax.mk_appl (Constant "Abst")

11614

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

11522

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)

11614

105 
 rename (prf1 %% prf2) = rename prf1 %% rename prf2


106 
 rename (prf % t) = rename prf % t

11522

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 

11614

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


133 
(Term.no_dummy_patterns t);


134 

11522

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

11614

139 
"axm" :: xs =>

11522

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

11614

146 
 "thm" :: xs =>

11522

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)) =

11614

160 
AbsP (s, case t of


161 
Const ("dummy_pattern", _) => None


162 
 _ $ Const ("dummy_pattern", _) => None


163 
 _ => Some (mk_term t),

11522

164 
incr_pboundvars 0 (~1) (prf_of [] prf))


165 
 prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =

11614

166 
prf_of [] prf1 %% prf_of [] prf2

11522

167 
 prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =


168 
prf_of (T::Ts) prf

11614

169 
 prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %


170 
(case t of Const ("dummy_pattern", _) => None  _ => Some (mk_term t))

11522

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)) =

11614

187 
Const (add_prefix "thm" name, proofT)

11522

188 
 term_of _ (PThm ((name, _), _, _, Some Ts)) =

11614

189 
mk_tyapp (Const (add_prefix "thm" name, proofT), Ts)


190 
 term_of _ (PAxm (name, _, None)) = Const (add_prefix "axm" name, proofT)

11522

191 
 term_of _ (PAxm (name, _, Some Ts)) =

11614

192 
mk_tyapp (Const (add_prefix "axm" name, proofT), Ts)

11522

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))

11614

202 
 term_of Ts (prf1 %% prf2) =

11522

203 
AppPt $ term_of Ts prf1 $ term_of Ts prf2

11614

204 
 term_of Ts (prf % opt) =

11522

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

11614

226 
(map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)

11522

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

11614

240 
(map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)

11522

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

11614

258 
(map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)

11522

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

11614

271 
(if full then Reconstruct.reconstruct_proof sign prop prf' else prf')

11522

272 
end;


273 


274 
val print_proof_of = Pretty.writeln oo pretty_proof_of;


275 


276 
end;
