src/Pure/axclass.ML
changeset 36418 752ee03427c2
parent 36417 54bc1a44967d
child 36419 7aea10d10113
     1.1 --- a/src/Pure/axclass.ML	Tue Apr 27 14:19:47 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Apr 27 14:41:27 2010 +0200
     1.3 @@ -72,8 +72,8 @@
     1.4  datatype data = Data of
     1.5   {axclasses: info Symtab.table,
     1.6    params: param list,
     1.7 -  proven_classrels: (thm * proof) Symreltab.table,
     1.8 -  proven_arities: ((class * sort list) * ((thm * string) * proof)) list Symtab.table,
     1.9 +  proven_classrels: thm Symreltab.table,
    1.10 +  proven_arities: ((class * sort list) * (thm * string)) list Symtab.table,
    1.11      (*arity theorems with theory name*)
    1.12    inst_params:
    1.13      (string * thm) Symtab.table Symtab.table *
    1.14 @@ -189,13 +189,10 @@
    1.15  
    1.16  fun the_classrel thy (c1, c2) =
    1.17    (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
    1.18 -    SOME classrel => classrel
    1.19 +    SOME thm => Thm.transfer thy thm
    1.20    | NONE => error ("Unproven class relation " ^
    1.21        Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
    1.22  
    1.23 -fun the_classrel_thm thy = Thm.transfer thy o #1 o the_classrel thy;
    1.24 -fun the_classrel_prf thy = #2 o the_classrel thy;
    1.25 -
    1.26  fun put_trancl_classrel ((c1, c2), th) thy =
    1.27    let
    1.28      val cert = Thm.cterm_of thy;
    1.29 @@ -207,14 +204,13 @@
    1.30      fun reflcl_classrel (c1', c2') =
    1.31        if c1' = c2'
    1.32        then Thm.trivial (cert (Logic.mk_of_class (TVar ((Name.aT, 0), []), c1')))
    1.33 -      else the_classrel_thm thy (c1', c2');
    1.34 +      else the_classrel thy (c1', c2');
    1.35      fun gen_classrel (c1_pred, c2_succ) =
    1.36        let
    1.37          val th' = ((reflcl_classrel (c1_pred, c1) RS th) RS reflcl_classrel (c2, c2_succ))
    1.38            |> Drule.instantiate' [SOME (certT (TVar ((Name.aT, 0), [])))] []
    1.39            |> Thm.close_derivation;
    1.40 -        val prf' = Thm.proof_of th';
    1.41 -      in ((c1_pred, c2_succ), (th', prf')) end;
    1.42 +      in ((c1_pred, c2_succ), th') end;
    1.43  
    1.44      val new_classrels =
    1.45        Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
    1.46 @@ -233,7 +229,7 @@
    1.47      val diff_merge_classrels = diff_merge_classrels_of thy;
    1.48      val (needed, thy') = (false, thy) |>
    1.49        fold (fn rel => fn (needed, thy) =>
    1.50 -          put_trancl_classrel (rel, Symreltab.lookup classrels rel |> the |> #1) thy
    1.51 +          put_trancl_classrel (rel, Symreltab.lookup classrels rel |> the) thy
    1.52            |>> (fn b => needed orelse b))
    1.53          diff_merge_classrels;
    1.54    in
    1.55 @@ -244,19 +240,16 @@
    1.56  
    1.57  fun the_arity thy a (c, Ss) =
    1.58    (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
    1.59 -    SOME arity => arity
    1.60 +    SOME (thm, _) => Thm.transfer thy thm
    1.61    | NONE => error ("Unproven type arity " ^
    1.62        Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
    1.63  
    1.64 -fun the_arity_thm thy a c_Ss = the_arity thy a c_Ss |> #1 |> #1 |> Thm.transfer thy;
    1.65 -fun the_arity_prf thy a c_Ss = the_arity thy a c_Ss |> #2;
    1.66 -
    1.67  fun thynames_of_arity thy (c, a) =
    1.68    Symtab.lookup_list (proven_arities_of thy) a
    1.69 -  |> map_filter (fn ((c', _), ((_, name), _)) => if c = c' then SOME name else NONE)
    1.70 +  |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
    1.71    |> rev;
    1.72  
    1.73 -fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name), _))) arities =
    1.74 +fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name)))) arities =
    1.75    let
    1.76      val algebra = Sign.classes_of thy;
    1.77      val ars = Symtab.lookup_list arities t;
    1.78 @@ -270,19 +263,15 @@
    1.79  
    1.80      val completions = super_class_completions |> map (fn c1 =>
    1.81        let
    1.82 -        val th1 = (th RS the_classrel_thm thy (c, c1))
    1.83 +        val th1 = (th RS the_classrel thy (c, c1))
    1.84            |> Drule.instantiate' std_vars []
    1.85            |> Thm.close_derivation;
    1.86 -        val prf1 = Thm.proof_of th1;
    1.87 -      in (((th1, thy_name), prf1), c1) end);
    1.88 -    val arities' = fold (fn (th_thy_prf1, c1) => Symtab.cons_list (t, ((c1, Ss), th_thy_prf1)))
    1.89 -      completions arities;
    1.90 +      in ((th1, thy_name), c1) end);
    1.91 +    val arities' = fold (fn (th, c1) => Symtab.cons_list (t, ((c1, Ss), th))) completions arities;
    1.92    in (null completions, arities') end;
    1.93  
    1.94  fun put_arity ((t, Ss, c), th) thy =
    1.95 -  let
    1.96 -    val arity = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th)));
    1.97 -  in
    1.98 +  let val arity = (t, ((c, Ss), (th, Context.theory_name thy))) in
    1.99      thy
   1.100      |> map_proven_arities
   1.101        (Symtab.insert_list (eq_fst op =) arity #> insert_arity_completions thy arity #> #2)
   1.102 @@ -302,6 +291,9 @@
   1.103  val _ = Context.>> (Context.map_theory
   1.104    (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
   1.105  
   1.106 +val the_classrel_prf = Thm.proof_of oo the_classrel;
   1.107 +val the_arity_prf = Thm.proof_of ooo the_arity;
   1.108 +
   1.109  
   1.110  (* maintain instance parameters *)
   1.111