# HG changeset patch # User wenzelm # Date 1226781090 -3600 # Node ID 9f3ecb4aaac22bbc46a3a84758ada0821c373c05 # Parent ba0ffe4cfc2be43e01d6456220da878f5181c1e0 proof_of_term: removed obsolete disambiguisation table; adapted PThm; Thm.proof_of returns proof_body; diff -r ba0ffe4cfc2b -r 9f3ecb4aaac2 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sat Nov 15 21:31:29 2008 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Sat Nov 15 21:31:30 2008 +0100 @@ -9,10 +9,7 @@ sig val proofT: typ val add_proof_syntax: theory -> theory - val disambiguate_names: theory -> Proofterm.proof -> - Proofterm.proof * Proofterm.proof Symtab.table - val proof_of_term: theory -> Proofterm.proof Symtab.table -> - bool -> term -> Proofterm.proof + val proof_of_term: theory -> bool -> term -> Proofterm.proof val term_of_proof: Proofterm.proof -> term val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) val read_term: theory -> typ -> string -> term @@ -88,41 +85,9 @@ [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]); -(**** create unambiguous theorem names ****) - -fun disambiguate_names thy prf = - let - val thms = thms_of_proof prf Symtab.empty; - val thms' = map (apsnd Thm.full_prop_of) (PureThy.all_thms_of thy); - - val tab = Symtab.fold (fn (key, ps) => fn tab => - let val prop = the_default (Bound 0) (AList.lookup (op =) thms' key) - in fst (fold_rev (fn (prop', prf) => fn x as (tab, i) => - if prop <> prop' then - (Symtab.update (key ^ "_" ^ string_of_int i, prf) tab, i+1) - else x) ps (tab, 1)) - end) thms Symtab.empty; - - fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf) - | rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf) - | rename (prf1 %% prf2) = rename prf1 %% rename prf2 - | rename (prf % t) = rename prf % t - | rename (prf' as PThm (s, prf, prop, Ts)) = - let - val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s); - val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s))) - in if prop = prop' then prf' else - PThm (s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps), - prf, prop, Ts) - end - | rename prf = prf - - in (rename prf, tab) end; - - (**** translation between proof terms and pure terms ****) -fun proof_of_term thy tab ty = +fun proof_of_term thy ty = let val thms = PureThy.all_thms_of thy; val axms = Theory.all_axioms_of thy; @@ -144,10 +109,8 @@ | "thm" :: xs => let val name = NameSpace.implode xs; in (case AList.lookup (op =) thms name of - SOME thm => fst (strip_combt (Thm.proof_of thm)) - | NONE => (case Symtab.lookup tab name of - SOME prf => prf - | NONE => error ("Unknown theorem " ^ quote name))) + SOME thm => fst (strip_combt (Proofterm.proof_of (Thm.proof_of thm))) + | NONE => error ("Unknown theorem " ^ quote name)) end | _ => error ("Illegal proof constant name: " ^ quote s)) | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop @@ -184,9 +147,9 @@ val mk_tyapp = fold (fn T => fn prf => Const ("Appt", [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); -fun term_of _ (PThm (name, _, _, NONE)) = +fun term_of _ (PThm (_, ((name, _, NONE), _))) = Const (NameSpace.append "thm" name, proofT) - | term_of _ (PThm (name, _, _, SOME Ts)) = + | term_of _ (PThm (_, ((name, _, SOME Ts), _))) = mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT)) | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT) | term_of _ (PAxm (name, _, SOME Ts)) = @@ -210,23 +173,20 @@ end | term_of Ts (Hyp t) = Hypt $ t | term_of Ts (Oracle (_, t, _)) = Oraclet $ t - | term_of Ts (MinProof _) = MinProoft; + | term_of Ts MinProof = MinProoft; val term_of_proof = term_of []; fun cterm_of_proof thy prf = let - val (prf', tab) = disambiguate_names thy prf; - val thm_names = filter_out (fn s => s = "") - (map fst (PureThy.all_thms_of thy) @ map fst (Symtab.dest tab)); + val thm_names = map fst (PureThy.all_thms_of thy); val axm_names = map fst (Theory.all_axioms_of thy); val thy' = thy |> add_proof_syntax |> add_proof_atom_consts - (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names) + (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names); in - (cterm_of thy' (term_of_proof prf'), - proof_of_term thy tab true o Thm.term_of) + (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) end; fun read_term thy = @@ -248,13 +208,15 @@ fun read_proof thy = let val rd = read_term thy proofT - in fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s)) end; + in fn ty => fn s => proof_of_term thy ty (Logic.varify (rd s)) end; fun proof_syntax prf = let - val thm_names = filter_out (fn s => s = "") - (map fst (Symtab.dest (thms_of_proof prf Symtab.empty))); - val axm_names = map fst (Symtab.dest (axms_of_proof prf Symtab.empty)); + val thm_names = Symtab.keys (fold_proof_atoms true + (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I + | _ => I) [prf] Symtab.empty); + val axm_names = Symtab.keys (fold_proof_atoms true + (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); in add_proof_syntax #> add_proof_atom_consts @@ -265,9 +227,9 @@ let val thy = Thm.theory_of_thm thm; val prop = Thm.full_prop_of thm; - val prf = Thm.proof_of thm; + val prf = Proofterm.proof_of (Thm.proof_of thm); val prf' = (case strip_combt (fst (strip_combP prf)) of - (PThm (_, prf', prop', _), _) => if prop = prop' then prf' else prf + (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then force_proof body else prf | _ => prf) in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;