tuned primitive inferences
authorhaftmann
Wed Dec 19 22:33:44 2007 +0100 (2007-12-19)
changeset 2571191cee0cefaf7
parent 25710 4cdf7de81e1b
child 25712 f488a37cfad4
tuned primitive inferences
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Wed Dec 19 17:40:48 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Dec 19 22:33:44 2007 +0100
     1.3 @@ -132,7 +132,7 @@
     1.4    base_sort: sort,
     1.5    inst: term option list
     1.6      (*canonical interpretation*),
     1.7 -  morphism: morphism,
     1.8 +  morphism: theory -> thm list -> morphism,
     1.9      (*partial morphism of canonical interpretation*)
    1.10    assm_intro: thm option,
    1.11    of_class: thm,
    1.12 @@ -195,7 +195,8 @@
    1.13  
    1.14  fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
    1.15  
    1.16 -fun morphism thy = #morphism o the_class_data thy;
    1.17 +fun partial_morphism thy class = #morphism (the_class_data thy class) thy [];
    1.18 +fun morphism thy class = #morphism (the_class_data thy class) thy (these_defs thy [class]);
    1.19  
    1.20  fun these_assm_intros thy =
    1.21    Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
    1.22 @@ -243,7 +244,7 @@
    1.23  (* updaters *)
    1.24  
    1.25  fun add_class_data ((class, superclasses),
    1.26 -    (params, base_sort, inst, phi, assm_intro, of_class, axiom)) thy =
    1.27 +    (params, base_sort, inst, phi, axiom, assm_intro, of_class)) thy =
    1.28    let
    1.29      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
    1.30        (c, (class, (ty, Free v_ty)))) params;
    1.31 @@ -276,6 +277,7 @@
    1.32  
    1.33  fun calculate thy sups base_sort assm_axiom param_map class =
    1.34    let
    1.35 +    (*static parts of morphism*)
    1.36      val subst_typ = map_atyps (fn TFree (v, sort) =>
    1.37            if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort)
    1.38        | ty => ty);
    1.39 @@ -283,52 +285,62 @@
    1.40           of SOME (c, _) => Const (c, ty)
    1.41            | NONE => t)
    1.42        | subst_aterm t = t;
    1.43 -    val subst_term = map_aterms subst_aterm #> map_types subst_typ;
    1.44 -    val matches = ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
    1.45 -      (base_sort, [class])], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
    1.46 -        (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), [class])) ty),
    1.47 -          Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), [class])) ty))) param_map);
    1.48 -    val inst_thm = Thm.instantiate matches;
    1.49 +    fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
    1.50 +      (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
    1.51 +        (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
    1.52 +          Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
    1.53 +    val instantiate_base_sort = instantiate thy base_sort;
    1.54 +    val instantiate_class = instantiate thy [class];
    1.55      val (proto_assm_intro, locale_intro) = Locale.intros thy class
    1.56        |> pairself (try the_single);
    1.57      val axiom_premises = map_filter (#axiom o the_class_data thy) sups
    1.58        @ the_list assm_axiom;
    1.59 -    val axiom = case locale_intro
    1.60 -     of SOME proto_axiom => SOME ((inst_thm proto_axiom OF axiom_premises) |> Drule.standard)
    1.61 -      | NONE => assm_axiom;
    1.62 -    val lift_axiom = case axiom of SOME axiom =>
    1.63 -          (fn thm => Thm.implies_elim (inst_thm thm) axiom)
    1.64 +    val axiom = locale_intro
    1.65 +      |> Option.map (Drule.standard o (fn thm => thm OF axiom_premises) o instantiate_class)
    1.66 +      |> (fn x as SOME _ => x | NONE => assm_axiom);
    1.67 +    val lift_axiom = case axiom
    1.68 +     of SOME axiom => (fn thm => Thm.implies_elim thm axiom)
    1.69        | NONE => I;
    1.70 -    val subst_thm = Drule.standard' #> inst_thm #> lift_axiom;
    1.71 -    val morphism = Morphism.term_morphism subst_term
    1.72 -      $> Morphism.typ_morphism subst_typ
    1.73 -      $> Morphism.thm_morphism subst_thm;
    1.74  
    1.75 -    (*FIXME use more primitives here rather than OF, simplifify code*)
    1.76 -    fun VarA sort = TVar ((Name.aT, 0), sort);
    1.77 -    fun FreeA sort = TFree (Name.aT, sort);
    1.78 -    fun instantiate sort1 sort2 =
    1.79 -      Thm.instantiate ([pairself (Thm.ctyp_of thy) (VarA sort1, FreeA sort2)], [])
    1.80 -    val inst_ty = (map_atyps o K o VarA) base_sort;
    1.81 +    (*dynamic parts of morphism*)
    1.82 +    fun rew_term thy defs = Pattern.rewrite_term thy
    1.83 +      (map (Logic.dest_equals o Thm.prop_of) defs) [];
    1.84 +    fun subst_term thy defs = map_aterms subst_aterm #> rew_term thy defs
    1.85 +      #> map_types subst_typ;
    1.86 +    fun subst_thm defs = Drule.standard' #> instantiate_class #> lift_axiom
    1.87 +      #> MetaSimplifier.rewrite_rule defs;
    1.88 +    fun morphism thy defs = 
    1.89 +      Morphism.typ_morphism subst_typ
    1.90 +      $> Morphism.term_morphism (subst_term thy defs)
    1.91 +      $> Morphism.thm_morphism (subst_thm defs);
    1.92 +
    1.93 +    (*class rules*)
    1.94 +    val defs = these_defs thy sups;
    1.95      val assm_intro = proto_assm_intro
    1.96 -      |> Option.map (Thm.instantiate ([],
    1.97 -           map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
    1.98 -             (Var ((v, 0), inst_ty ty), Const (c, inst_ty ty))) param_map))
    1.99 -      |> Option.map (MetaSimplifier.rewrite_rule (these_defs thy sups))
   1.100 +      |> Option.map instantiate_base_sort
   1.101 +      |> Option.map (MetaSimplifier.rewrite_rule defs)
   1.102        |> Option.map Goal.close_result;
   1.103 -    val class_intro = (instantiate [] base_sort o #intro o AxClass.get_info thy) class;
   1.104 +    val fixate = Thm.instantiate
   1.105 +      (map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)),
   1.106 +        (TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], [])
   1.107 +    val class_intro = (fixate o #intro o AxClass.get_info thy) class;
   1.108      val of_class_sups = if null sups
   1.109 -      then Drule.sort_triv thy (FreeA base_sort, base_sort)
   1.110 -      else map (Drule.implies_intr_hyps o #of_class o the_class_data thy) sups;
   1.111 +      then map (fixate o Thm.class_triv thy) base_sort
   1.112 +      else map (fixate o #of_class o the_class_data thy) sups;
   1.113      val locale_dests = map Drule.standard' (Locale.dests thy class);
   1.114 -    fun mk_pred_triv () = (Thm.assume o Thm.cterm_of thy
   1.115 -      o (map_types o map_atyps o K o FreeA) base_sort o Thm.prop_of o the) axiom;
   1.116 -    val pred_trivs = case length locale_dests
   1.117 -     of 0 => if is_none locale_intro then [] else [mk_pred_triv ()]
   1.118 -      | n => replicate n (mk_pred_triv ());
   1.119 +    val num_trivs = case length locale_dests
   1.120 +     of 0 => if is_none axiom then 0 else 1
   1.121 +      | n => n;
   1.122 +    val pred_trivs = if num_trivs = 0 then []
   1.123 +      else the axiom
   1.124 +        |> Thm.prop_of
   1.125 +        |> (map_types o map_atyps o K) (TFree (Name.aT, base_sort))
   1.126 +        |> (Thm.assume o Thm.cterm_of thy)
   1.127 +        |> replicate num_trivs;
   1.128      val of_class = (class_intro OF of_class_sups OF locale_dests OF pred_trivs)
   1.129 +      |> Drule.standard'
   1.130        |> Goal.close_result;
   1.131 -  in (morphism, assm_intro, of_class, axiom) end;
   1.132 +  in (morphism, axiom, assm_intro, of_class) end;
   1.133  
   1.134  fun class_interpretation class facts defs thy =
   1.135    let
   1.136 @@ -346,7 +358,7 @@
   1.137  
   1.138  fun prove_subclass (sub, sup) thm thy =
   1.139    let
   1.140 -    val of_class = (Drule.standard' o #of_class o the_class_data thy) sup;
   1.141 +    val of_class = (#of_class o the_class_data thy) sup;
   1.142      val intro = Drule.standard' (of_class OF [Drule.standard' thm]);
   1.143      val classrel = intro OF (the_list o #axiom o the_class_data thy) sub;
   1.144    in
   1.145 @@ -600,9 +612,9 @@
   1.146      |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax other_consts
   1.147      |-> (fn (param_map, params, assm_axiom) =>
   1.148           `(fn thy => calculate thy sups base_sort assm_axiom param_map class)
   1.149 -    #-> (fn (morphism, assm_intro, assm_proj, axiom) =>
   1.150 +    #-> (fn (morphism, axiom, assm_intro, of_class) =>
   1.151          add_class_data ((class, sups), (params, base_sort,
   1.152 -          map snd param_map, morphism, assm_intro, assm_proj, axiom))
   1.153 +          map snd param_map, morphism, axiom, assm_intro, of_class))
   1.154      #> class_interpretation class (the_list axiom) []))
   1.155      |> init class
   1.156      |> pair class
   1.157 @@ -624,7 +636,7 @@
   1.158    let
   1.159      val prfx = class_prefix class;
   1.160      val thy' = thy |> Sign.add_path prfx;
   1.161 -    val phi = morphism thy' class;
   1.162 +    val phi = partial_morphism thy' class;
   1.163  
   1.164      val c' = Sign.full_name thy' c;
   1.165      val dict' = Morphism.term phi dict;
   1.166 @@ -652,8 +664,7 @@
   1.167      val phi = morphism thy class;
   1.168  
   1.169      val c' = Sign.full_name thy' c;
   1.170 -    val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class])
   1.171 -    val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs;
   1.172 +    val rhs' = Morphism.term phi rhs;
   1.173      val ty' = Logic.unvarifyT (Term.fastype_of rhs');
   1.174    in
   1.175      thy'
   1.176 @@ -704,14 +715,6 @@
   1.177  
   1.178  (* syntax *)
   1.179  
   1.180 -fun subst_param thy params = map_aterms (fn t as Const (c, ty) =>
   1.181 -    (case AxClass.inst_tyco_of thy (c, ty)
   1.182 -     of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   1.183 -         of SOME v_ty => Free v_ty
   1.184 -          | NONE => t)
   1.185 -      | NONE => t)
   1.186 -  | t => t);
   1.187 -
   1.188  fun inst_term_check ts lthy =
   1.189    let
   1.190      val params = instantiation_params lthy;
   1.191 @@ -724,9 +727,17 @@
   1.192                | NONE => I)
   1.193            | NONE => I)
   1.194        | check_improve _ = I;
   1.195 +    val subst_param = map_aterms (fn t as Const (c, ty) =>
   1.196 +        (case AxClass.inst_tyco_of thy (c, ty)
   1.197 +         of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   1.198 +             of SOME v_ty => Free v_ty
   1.199 +              | NONE => t)
   1.200 +          | NONE => t)
   1.201 +      | t => t);
   1.202 +
   1.203      val improvement = (fold o fold_aterms) check_improve ts Vartab.empty;
   1.204      val ts' = (map o map_types) (Envir.typ_subst_TVars improvement) ts;
   1.205 -    val ts'' = map (subst_param thy params) ts';
   1.206 +    val ts'' = map subst_param ts';
   1.207    in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', lthy) end;
   1.208  
   1.209  fun inst_term_uncheck ts lthy =