back-patching of axclass proofs;
authorwenzelm
Sat May 08 15:24:59 2010 +0200 (2010-05-08 ago)
changeset 367406248aa22c694
parent 36739 e9401d2efc5f
child 36741 d65ed9d7275e
back-patching of axclass proofs;
src/Pure/axclass.ML
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/axclass.ML	Sat May 08 14:41:23 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sat May 08 15:24:59 2010 +0200
     1.3 @@ -241,7 +241,7 @@
     1.4    end;
     1.5  
     1.6  
     1.7 -fun the_arity thy a (c, Ss) =
     1.8 +fun the_arity thy (a, Ss, c) =
     1.9    (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
    1.10      SOME (thm, _) => Thm.transfer thy thm
    1.11    | NONE => error ("Unproven type arity " ^
    1.12 @@ -295,10 +295,12 @@
    1.13    end;
    1.14  
    1.15  val _ = Context.>> (Context.map_theory
    1.16 -  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
    1.17 +  (Theory.at_begin complete_classrels #>
    1.18 +   Theory.at_begin complete_arities));
    1.19  
    1.20 -val the_classrel_prf = Thm.proof_of oo the_classrel;
    1.21 -val the_arity_prf = Thm.proof_of ooo the_arity;
    1.22 +val _ = Proofterm.install_axclass_proofs
    1.23 +  {classrel_proof = Thm.proof_of oo the_classrel,
    1.24 +   arity_proof = Thm.proof_of oo the_arity};
    1.25  
    1.26  
    1.27  (* maintain instance parameters *)
     2.1 --- a/src/Pure/proofterm.ML	Sat May 08 14:41:23 2010 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Sat May 08 15:24:59 2010 +0200
     2.3 @@ -110,6 +110,11 @@
     2.4    val equal_elim: term -> term -> proof -> proof -> proof
     2.5    val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
     2.6      sort list -> proof -> proof
     2.7 +  val classrel_proof: theory -> class * class -> proof
     2.8 +  val arity_proof: theory -> string * sort list * class -> proof
     2.9 +  val install_axclass_proofs:
    2.10 +   {classrel_proof: theory -> class * class -> proof,
    2.11 +    arity_proof: theory -> string * sort list * class -> proof} -> unit
    2.12    val axm_proof: string -> term -> proof
    2.13    val oracle_proof: string -> term -> oracle * proof
    2.14    val promise_proof: theory -> serial -> term -> proof
    2.15 @@ -886,7 +891,7 @@
    2.16    equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
    2.17  
    2.18  
    2.19 -(**** sort hypotheses ****)
    2.20 +(**** type classes ****)
    2.21  
    2.22  fun strip_shyps_proof algebra present witnessed extra_sorts prf =
    2.23    let
    2.24 @@ -902,6 +907,30 @@
    2.25    in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
    2.26  
    2.27  
    2.28 +local
    2.29 +
    2.30 +type axclass_proofs =
    2.31 + {classrel_proof: theory -> class * class -> proof,
    2.32 +  arity_proof: theory -> string * sort list * class -> proof};
    2.33 +
    2.34 +val axclass_proofs: axclass_proofs Single_Assignment.var =
    2.35 +  Single_Assignment.var "Proofterm.axclass_proofs";
    2.36 +
    2.37 +fun axclass_proof which thy x =
    2.38 +  (case Single_Assignment.peek axclass_proofs of
    2.39 +    NONE => raise Fail "Axclass proof operations not installed"
    2.40 +  | SOME prfs => which prfs thy x);
    2.41 +
    2.42 +in
    2.43 +
    2.44 +val classrel_proof = axclass_proof #classrel_proof;
    2.45 +val arity_proof = axclass_proof #arity_proof;
    2.46 +
    2.47 +fun install_axclass_proofs prfs = Single_Assignment.assign axclass_proofs prfs;
    2.48 +
    2.49 +end;
    2.50 +
    2.51 +
    2.52  (***** axioms and theorems *****)
    2.53  
    2.54  val proofs = Unsynchronized.ref 2;