src/Pure/proofterm.ML
changeset 36741 d65ed9d7275e
parent 36740 6248aa22c694
child 36742 6f8bbe9ca8a2
     1.1 --- a/src/Pure/proofterm.ML	Sat May 08 15:24:59 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Sat May 08 16:03:09 2010 +0200
     1.3 @@ -112,6 +112,7 @@
     1.4      sort list -> proof -> proof
     1.5    val classrel_proof: theory -> class * class -> proof
     1.6    val arity_proof: theory -> string * sort list * class -> proof
     1.7 +  val of_sort_proof: theory -> (typ * class -> proof) -> typ * sort -> proof list
     1.8    val install_axclass_proofs:
     1.9     {classrel_proof: theory -> class * class -> proof,
    1.10      arity_proof: theory -> string * sort list * class -> proof} -> unit
    1.11 @@ -931,6 +932,29 @@
    1.12  end;
    1.13  
    1.14  
    1.15 +local
    1.16 +
    1.17 +fun canonical_instance typs =
    1.18 +  let
    1.19 +    val names = Name.invents Name.context Name.aT (length typs);
    1.20 +    val instT = map2 (fn a => fn T => (((a, 0), []), Type.strip_sorts T)) names typs;
    1.21 +  in instantiate (instT, []) end;
    1.22 +
    1.23 +in
    1.24 +
    1.25 +fun of_sort_proof thy hyps =
    1.26 +  Sorts.of_sort_derivation (Sign.classes_of thy)
    1.27 +   {class_relation = fn typ => fn (prf, c1) => fn c2 =>
    1.28 +      if c1 = c2 then prf
    1.29 +      else canonical_instance [typ] (classrel_proof thy (c1, c2)) %% prf,
    1.30 +    type_constructor = fn (a, typs) => fn dom => fn c =>
    1.31 +      let val Ss = map (map snd) dom and prfs = maps (map fst) dom
    1.32 +      in proof_combP (canonical_instance typs (arity_proof thy (a, Ss, c)), prfs) end,
    1.33 +    type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)};
    1.34 +
    1.35 +end;
    1.36 +
    1.37 +
    1.38  (***** axioms and theorems *****)
    1.39  
    1.40  val proofs = Unsynchronized.ref 2;