src/Pure/Isar/class.ML
changeset 25683 d9fefc4859be
parent 25668 a9ebfc170fbc
child 25711 91cee0cefaf7
     1.1 --- a/src/Pure/Isar/class.ML	Mon Dec 17 22:40:12 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Dec 17 22:40:13 2007 +0100
     1.3 @@ -243,13 +243,12 @@
     1.4  (* updaters *)
     1.5  
     1.6  fun add_class_data ((class, superclasses),
     1.7 -    (cs, base_sort, inst, phi, assm_intro, of_class, axiom)) thy =
     1.8 +    (params, base_sort, inst, phi, assm_intro, of_class, axiom)) thy =
     1.9    let
    1.10      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
    1.11 -      (c, (class, (ty, Free v_ty)))) cs;
    1.12 -    val cs = (map o pairself) fst cs;
    1.13 +      (c, (class, (ty, Free v_ty)))) params;
    1.14      val add_class = Graph.new_node (class,
    1.15 -        mk_class_data ((cs, base_sort,
    1.16 +        mk_class_data (((map o pairself) fst params, base_sort,
    1.17            map (SOME o Const) inst, phi, assm_intro, of_class, axiom), ([], operations)))
    1.18        #> fold (curry Graph.add_edge class) superclasses;
    1.19    in ClassData.map add_class thy end;
    1.20 @@ -275,48 +274,53 @@
    1.21  
    1.22  val class_prefix = Logic.const_of_class o Sign.base_name;
    1.23  
    1.24 -fun calculate_morphism class cs =
    1.25 +fun calculate thy sups base_sort assm_axiom param_map class =
    1.26    let
    1.27 -    val subst_typ = Term.map_type_tfree (fn var as (v, sort) =>
    1.28 -      if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort));
    1.29 -    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
    1.30 +    val subst_typ = map_atyps (fn TFree (v, sort) =>
    1.31 +          if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort)
    1.32 +      | ty => ty);
    1.33 +    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) param_map v
    1.34           of SOME (c, _) => Const (c, ty)
    1.35            | NONE => t)
    1.36        | subst_aterm t = t;
    1.37      val subst_term = map_aterms subst_aterm #> map_types subst_typ;
    1.38 -  in
    1.39 -    Morphism.term_morphism subst_term
    1.40 -    $> Morphism.typ_morphism subst_typ
    1.41 -  end;
    1.42 +    val matches = ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
    1.43 +      (base_sort, [class])], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
    1.44 +        (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), [class])) ty),
    1.45 +          Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), [class])) ty))) param_map);
    1.46 +    val inst_thm = Thm.instantiate matches;
    1.47 +    val (proto_assm_intro, locale_intro) = Locale.intros thy class
    1.48 +      |> pairself (try the_single);
    1.49 +    val axiom_premises = map_filter (#axiom o the_class_data thy) sups
    1.50 +      @ the_list assm_axiom;
    1.51 +    val axiom = case locale_intro
    1.52 +     of SOME proto_axiom => SOME ((inst_thm proto_axiom OF axiom_premises) |> Drule.standard)
    1.53 +      | NONE => assm_axiom;
    1.54 +    val lift_axiom = case axiom of SOME axiom =>
    1.55 +          (fn thm => Thm.implies_elim (inst_thm thm) axiom)
    1.56 +      | NONE => I;
    1.57 +    val subst_thm = Drule.standard' #> inst_thm #> lift_axiom;
    1.58 +    val morphism = Morphism.term_morphism subst_term
    1.59 +      $> Morphism.typ_morphism subst_typ
    1.60 +      $> Morphism.thm_morphism subst_thm;
    1.61  
    1.62 -fun calculate_rules thy sups base_sort assm_axiom param_map class =
    1.63 -  let
    1.64 -    (*FIXME use more primitves here rather than OF, simplifify code*)
    1.65 -    fun the_option [x] = SOME x
    1.66 -      | the_option [] = NONE;
    1.67 +    (*FIXME use more primitives here rather than OF, simplifify code*)
    1.68      fun VarA sort = TVar ((Name.aT, 0), sort);
    1.69      fun FreeA sort = TFree (Name.aT, sort);
    1.70      fun instantiate sort1 sort2 =
    1.71        Thm.instantiate ([pairself (Thm.ctyp_of thy) (VarA sort1, FreeA sort2)], [])
    1.72 -    val (proto_assm_intro, locale_intro) = pairself the_option (Locale.intros thy class);
    1.73      val inst_ty = (map_atyps o K o VarA) base_sort;
    1.74      val assm_intro = proto_assm_intro
    1.75        |> Option.map (Thm.instantiate ([],
    1.76 -           map (fn ((v, _), (c, ty)) => pairself (Thm.cterm_of thy)
    1.77 +           map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
    1.78               (Var ((v, 0), inst_ty ty), Const (c, inst_ty ty))) param_map))
    1.79        |> Option.map (MetaSimplifier.rewrite_rule (these_defs thy sups))
    1.80        |> Option.map Goal.close_result;
    1.81 -    val axiom_premises = map_filter (#axiom o the_class_data thy) sups
    1.82 -      @ the_list assm_axiom;
    1.83 -    val axiom = case locale_intro
    1.84 -     of SOME proto_axiom => SOME
    1.85 -          ((instantiate base_sort [class] proto_axiom OF axiom_premises) |> Drule.standard)
    1.86 -      | NONE => assm_axiom;
    1.87      val class_intro = (instantiate [] base_sort o #intro o AxClass.get_info thy) class;
    1.88      val of_class_sups = if null sups
    1.89        then Drule.sort_triv thy (FreeA base_sort, base_sort)
    1.90        else map (Drule.implies_intr_hyps o #of_class o the_class_data thy) sups;
    1.91 -    val locale_dests = map Drule.standard (Locale.dests thy class);
    1.92 +    val locale_dests = map Drule.standard' (Locale.dests thy class);
    1.93      fun mk_pred_triv () = (Thm.assume o Thm.cterm_of thy
    1.94        o (map_types o map_atyps o K o FreeA) base_sort o Thm.prop_of o the) axiom;
    1.95      val pred_trivs = case length locale_dests
    1.96 @@ -324,7 +328,7 @@
    1.97        | n => replicate n (mk_pred_triv ());
    1.98      val of_class = (class_intro OF of_class_sups OF locale_dests OF pred_trivs)
    1.99        |> Goal.close_result;
   1.100 -  in (assm_intro, of_class, axiom) end;
   1.101 +  in (morphism, assm_intro, of_class, axiom) end;
   1.102  
   1.103  fun class_interpretation class facts defs thy =
   1.104    let
   1.105 @@ -342,8 +346,8 @@
   1.106  
   1.107  fun prove_subclass (sub, sup) thm thy =
   1.108    let
   1.109 -    val of_class = (Drule.standard o #of_class o the_class_data thy) sup;
   1.110 -    val intro = Drule.standard (of_class OF [Drule.standard thm]);
   1.111 +    val of_class = (Drule.standard' o #of_class o the_class_data thy) sup;
   1.112 +    val intro = Drule.standard' (of_class OF [Drule.standard' thm]);
   1.113      val classrel = intro OF (the_list o #axiom o the_class_data thy) sub;
   1.114    in
   1.115      thy
   1.116 @@ -511,105 +515,95 @@
   1.117        | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   1.118      val supexpr = Locale.Merge suplocales;
   1.119      val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
   1.120 -    val supconsts = AList.make (the o AList.lookup (op =) (these_params thy sups))
   1.121 -      (map fst supparams);
   1.122      val mergeexpr = Locale.Merge (suplocales @ includes);
   1.123      val constrain = Element.Constrains ((map o apsnd o map_atyps)
   1.124        (fn TFree (_, sort) => TFree (Name.aT, sort)) supparams);
   1.125 -  in
   1.126 -    ProofContext.init thy
   1.127 -    |> Locale.cert_expr supexpr [constrain]
   1.128 -    |> snd
   1.129 -    |> init_ctxt sups base_sort
   1.130 -    |> process_expr Locale.empty raw_elems
   1.131 -    |> fst
   1.132 -    |> (fn elems => ((((sups, supconsts), (supsort, base_sort, mergeexpr)),
   1.133 -          (*FIXME*) if null includes then constrain :: elems else elems)))
   1.134 -  end;
   1.135 +    fun fork_syn (Element.Fixes xs) =
   1.136 +          fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
   1.137 +          #>> Element.Fixes
   1.138 +      | fork_syn x = pair x;
   1.139 +    fun fork_syntax elems =
   1.140 +      let
   1.141 +        val (elems', global_syntax) = fold_map fork_syn elems [];
   1.142 +      in (if null includes (*FIXME*) then constrain :: elems' else elems', global_syntax) end;
   1.143 +    val (elems, global_syntax) =
   1.144 +      ProofContext.init thy
   1.145 +      |> Locale.cert_expr supexpr [constrain]
   1.146 +      |> snd
   1.147 +      |> init_ctxt sups base_sort
   1.148 +      |> process_expr Locale.empty raw_elems
   1.149 +      |> fst
   1.150 +      |> fork_syntax
   1.151 +  in (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) end;
   1.152  
   1.153  val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
   1.154  val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
   1.155  
   1.156 -fun define_class_params name class superclasses consts dep_axiom other_consts thy =
   1.157 +fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax other_consts thy =
   1.158    let
   1.159 -    fun add_const ((c, ty), syn) =
   1.160 -      Sign.declare_const [] (c, Type.strip_sorts ty, syn) #>> Term.dest_Const;
   1.161 -    val constrain_typs = (map o apsnd o Term.map_type_tfree)
   1.162 -      (fn (v, _) => TFree (v, [class]))
   1.163 -    fun the_option [x] = SOME x
   1.164 -      | the_option [] = NONE;
   1.165 +    val supconsts = map fst supparams
   1.166 +      |> AList.make (the o AList.lookup (op =) (these_params thy sups))
   1.167 +      |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
   1.168 +    val all_params = map fst (Locale.parameters_of thy class);
   1.169 +    fun add_const (v, raw_ty) thy =
   1.170 +      let
   1.171 +        val c = Sign.full_name thy v;
   1.172 +        val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
   1.173 +        val ty0 = Type.strip_sorts ty;
   1.174 +        val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
   1.175 +        val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v;
   1.176 +      in
   1.177 +        thy
   1.178 +        |> Sign.declare_const [] (v, ty0, syn)
   1.179 +        |> snd
   1.180 +        |> pair ((v, ty), (c, ty'))
   1.181 +      end;
   1.182 +    fun add_consts raw_params thy =
   1.183 +      thy
   1.184 +      |> Sign.add_path (Logic.const_of_class bname)
   1.185 +      |> fold_map add_const raw_params
   1.186 +      ||> Sign.restore_naming thy
   1.187 +      |-> (fn params => pair (supconsts @ (map o apfst) fst params, params));
   1.188 +    fun globalize param_map = map_aterms
   1.189 +      (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
   1.190 +        | t => t);
   1.191 +    val raw_pred = Locale.intros thy class
   1.192 +      |> fst
   1.193 +      |> map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of);
   1.194 +    fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
   1.195 +     of [] => NONE
   1.196 +      | [thm] => SOME thm;
   1.197    in
   1.198      thy
   1.199 -    |> Sign.add_path (Logic.const_of_class name)
   1.200 -    |> fold_map add_const consts
   1.201 -    ||> Sign.restore_naming thy
   1.202 -    |-> (fn cs => `(fn thy => dep_axiom thy cs)
   1.203 -    #-> (fn axiom => AxClass.define_class (name, superclasses)
   1.204 -           (map fst cs @ other_consts) [axiom]
   1.205 -    #-> (fn _ => `(fn _ => constrain_typs cs)
   1.206 -    #-> (fn cs' => `(fn thy => (the_option o #axioms o AxClass.get_info thy) class)
   1.207 -    #-> (fn axiom => fold (Sign.add_const_constraint o apsnd SOME) cs'
   1.208 -    #> pair (cs', axiom))))))
   1.209 +    |> add_consts ((snd o chop (length supparams)) all_params)
   1.210 +    |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
   1.211 +          (map (fst o snd) params @ other_consts)
   1.212 +          [((bname ^ "_" ^ AxClass.axiomsN, []), map (globalize param_map) raw_pred)]
   1.213 +    #> snd
   1.214 +    #> `get_axiom
   1.215 +    #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
   1.216 +    #> pair (param_map, params, assm_axiom)))
   1.217    end;
   1.218  
   1.219  fun gen_class prep_spec prep_param bname
   1.220      raw_supclasses raw_includes_elems raw_other_consts thy =
   1.221    let
   1.222      val class = Sign.full_name thy bname;
   1.223 -    val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) =
   1.224 +    val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
   1.225        prep_spec thy raw_supclasses raw_includes_elems;
   1.226      val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
   1.227 -    fun mk_inst class cs =
   1.228 -      (map o apsnd o Term.map_type_tfree) (fn (v, _) => TFree (v, [class])) cs;
   1.229 -    fun fork_syntax (Element.Fixes xs) =
   1.230 -          fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
   1.231 -          #>> Element.Fixes
   1.232 -      | fork_syntax x = pair x;
   1.233 -    val (elems, global_syn) = fold_map fork_syntax elems_syn [];
   1.234 -    fun globalize (c, ty) =
   1.235 -      ((c, map_atyps (K (TFree (Name.aT, base_sort))) ty),
   1.236 -        (the_default NoSyn o AList.lookup (op =) global_syn) c);
   1.237 -    fun extract_params thy =
   1.238 -      let
   1.239 -        val params = map fst (Locale.parameters_of thy class);
   1.240 -      in
   1.241 -        (params, (map globalize o snd o chop (length supconsts)) params)
   1.242 -      end;
   1.243 -    fun extract_assumes params thy cs =
   1.244 -      let
   1.245 -        val consts = supconsts @ (map (fst o fst) params ~~ cs);
   1.246 -        fun subst (Free (c, ty)) =
   1.247 -              Const ((fst o the o AList.lookup (op =) consts) c, ty)
   1.248 -          | subst t = t;
   1.249 -        fun prep_asm ((name, atts), ts) =
   1.250 -          ((Sign.base_name name, map (Attrib.attribute_i thy) atts),
   1.251 -            (map o map_aterms) subst ts);
   1.252 -      in
   1.253 -        Locale.intros thy class
   1.254 -        |> fst
   1.255 -        |> map (map_aterms subst o Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of)
   1.256 -        |> pair (bname ^ "_" ^ AxClass.axiomsN, [])
   1.257 -      end;
   1.258    in
   1.259      thy
   1.260      |> Locale.add_locale_i (SOME "") bname mergeexpr elems
   1.261      |> snd
   1.262      |> ProofContext.theory_of
   1.263 -    |> `extract_params
   1.264 -    |-> (fn (all_params, params) =>
   1.265 -        define_class_params bname class supsort params
   1.266 -          (extract_assumes params) other_consts
   1.267 -      #-> (fn (consts, assm_axiom) =>
   1.268 -        `(fn thy => calculate_rules thy sups base_sort assm_axiom
   1.269 -          (all_params ~~ map snd supconsts @ consts) class)
   1.270 -      #-> (fn (assm_intro, assm_proj, axiom) =>
   1.271 -        add_class_data ((class, sups),
   1.272 -          (map fst params ~~ consts, base_sort,
   1.273 -            mk_inst class (map snd supconsts @ consts),
   1.274 -              calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)),
   1.275 -          assm_intro, assm_proj, axiom))
   1.276 -      #> class_interpretation class (the_list axiom) []
   1.277 -      )))
   1.278 +    |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax other_consts
   1.279 +    |-> (fn (param_map, params, assm_axiom) =>
   1.280 +         `(fn thy => calculate thy sups base_sort assm_axiom param_map class)
   1.281 +    #-> (fn (morphism, assm_intro, assm_proj, axiom) =>
   1.282 +        add_class_data ((class, sups), (params, base_sort,
   1.283 +          map snd param_map, morphism, assm_intro, assm_proj, axiom))
   1.284 +    #> class_interpretation class (the_list axiom) []))
   1.285      |> init class
   1.286      |> pair class
   1.287    end;
   1.288 @@ -832,3 +826,4 @@
   1.289    end;
   1.290  
   1.291  end;
   1.292 +