summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 08 May 2010 16:03:09 +0200 | |

changeset 36741 | d65ed9d7275e |

parent 36740 | 6248aa22c694 |

child 36742 | 6f8bbe9ca8a2 |

added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;

--- a/src/Pure/proofterm.ML Sat May 08 15:24:59 2010 +0200 +++ b/src/Pure/proofterm.ML Sat May 08 16:03:09 2010 +0200 @@ -112,6 +112,7 @@ sort list -> proof -> proof val classrel_proof: theory -> class * class -> proof val arity_proof: theory -> string * sort list * class -> proof + val of_sort_proof: theory -> (typ * class -> proof) -> typ * sort -> proof list val install_axclass_proofs: {classrel_proof: theory -> class * class -> proof, arity_proof: theory -> string * sort list * class -> proof} -> unit @@ -931,6 +932,29 @@ end; +local + +fun canonical_instance typs = + let + val names = Name.invents Name.context Name.aT (length typs); + val instT = map2 (fn a => fn T => (((a, 0), []), Type.strip_sorts T)) names typs; + in instantiate (instT, []) end; + +in + +fun of_sort_proof thy hyps = + Sorts.of_sort_derivation (Sign.classes_of thy) + {class_relation = fn typ => fn (prf, c1) => fn c2 => + if c1 = c2 then prf + else canonical_instance [typ] (classrel_proof thy (c1, c2)) %% prf, + type_constructor = fn (a, typs) => fn dom => fn c => + let val Ss = map (map snd) dom and prfs = maps (map fst) dom + in proof_combP (canonical_instance typs (arity_proof thy (a, Ss, c)), prfs) end, + type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)}; + +end; + + (***** axioms and theorems *****) val proofs = Unsynchronized.ref 2;