improved rule calculation
authorhaftmann
Thu Dec 13 07:09:06 2007 +0100 (2007-12-13)
changeset 2561801f20279fea1
parent 25617 b495384e48e1
child 25619 e4d5cd384245
improved rule calculation
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Dec 13 07:09:05 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Dec 13 07:09:06 2007 +0100
     1.3 @@ -22,8 +22,7 @@
     1.4  
     1.5    val intro_classes_tac: thm list -> tactic
     1.6    val default_intro_classes_tac: thm list -> tactic
     1.7 -  val prove_subclass: class * class -> thm list -> Proof.context
     1.8 -    -> theory -> theory
     1.9 +  val prove_subclass: class * class -> thm -> theory -> theory
    1.10  
    1.11    val class_prefix: string -> string
    1.12    val is_class: theory -> class -> bool
    1.13 @@ -71,22 +70,6 @@
    1.14        (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    1.15    #> ProofContext.theory_of;
    1.16  
    1.17 -fun OF_LAST thm1 thm2 = thm1 RSN (Thm.nprems_of thm2, thm2);
    1.18 -
    1.19 -fun strip_all_ofclass thy sort =
    1.20 -  let
    1.21 -    val typ = TVar ((Name.aT, 0), sort);
    1.22 -    fun prem_inclass t =
    1.23 -      case Logic.strip_imp_prems t
    1.24 -       of ofcls :: _ => try Logic.dest_inclass ofcls
    1.25 -        | [] => NONE;
    1.26 -    fun strip_ofclass class thm =
    1.27 -      thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
    1.28 -    fun strip thm = case (prem_inclass o Thm.prop_of) thm
    1.29 -     of SOME (_, class) => thm |> strip_ofclass class |> strip
    1.30 -      | NONE => thm;
    1.31 -  in strip end;
    1.32 -
    1.33  fun get_remove_global_constraint c thy =
    1.34    let
    1.35      val ty = Sign.the_const_constraint thy c;
    1.36 @@ -151,27 +134,29 @@
    1.37      (*canonical interpretation*),
    1.38    morphism: morphism,
    1.39      (*partial morphism of canonical interpretation*)
    1.40 -  intro: thm,
    1.41 +  assm_intro: thm option,
    1.42 +  of_class: thm,
    1.43 +  axiom: thm option,
    1.44    defs: thm list,
    1.45    operations: (string * (class * (typ * term))) list
    1.46  };
    1.47  
    1.48  fun rep_class_data (ClassData d) = d;
    1.49 -fun mk_class_data ((consts, base_sort, inst, morphism, intro),
    1.50 +fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
    1.51      (defs, operations)) =
    1.52    ClassData { consts = consts, base_sort = base_sort, inst = inst,
    1.53 -    morphism = morphism, intro = intro, defs = defs,
    1.54 -    operations = operations };
    1.55 -fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro,
    1.56 -    defs, operations }) =
    1.57 -  mk_class_data (f ((consts, base_sort, inst, morphism, intro),
    1.58 +    morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom, 
    1.59 +    defs = defs, operations = operations };
    1.60 +fun map_class_data f (ClassData { consts, base_sort, inst, morphism,
    1.61 +    assm_intro, of_class, axiom, defs, operations }) =
    1.62 +  mk_class_data (f ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
    1.63      (defs, operations)));
    1.64  fun merge_class_data _ (ClassData { consts = consts,
    1.65 -    base_sort = base_sort, inst = inst, morphism = morphism, intro = intro,
    1.66 -    defs = defs1, operations = operations1 },
    1.67 -  ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _,
    1.68 -    defs = defs2, operations = operations2 }) =
    1.69 -  mk_class_data ((consts, base_sort, inst, morphism, intro),
    1.70 +    base_sort = base_sort, inst = inst, morphism = morphism, assm_intro = assm_intro,
    1.71 +    of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
    1.72 +  ClassData { consts = _, base_sort = _, inst = _, morphism = _, assm_intro = _,
    1.73 +    of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
    1.74 +  mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
    1.75      (Thm.merge_thms (defs1, defs2),
    1.76        AList.merge (op =) (K true) (operations1, operations2)));
    1.77  
    1.78 @@ -212,9 +197,9 @@
    1.79  
    1.80  fun morphism thy = #morphism o the_class_data thy;
    1.81  
    1.82 -fun these_intros thy =
    1.83 -  Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
    1.84 -    (ClassData.get thy) [];
    1.85 +fun these_assm_intros thy =
    1.86 +  Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
    1.87 +    ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
    1.88  
    1.89  fun these_operations thy =
    1.90    maps (#operations o the_class_data thy) o ancestry thy;
    1.91 @@ -257,17 +242,17 @@
    1.92  
    1.93  (* updaters *)
    1.94  
    1.95 -fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
    1.96 +fun add_class_data ((class, superclasses),
    1.97 +    (cs, base_sort, inst, phi, assm_intro, of_class, axiom)) thy =
    1.98    let
    1.99      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   1.100        (c, (class, (ty, Free v_ty)))) cs;
   1.101      val cs = (map o pairself) fst cs;
   1.102      val add_class = Graph.new_node (class,
   1.103 -        mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations)))
   1.104 +        mk_class_data ((cs, base_sort,
   1.105 +          map (SOME o Const) inst, phi, assm_intro, of_class, axiom), ([], operations)))
   1.106        #> fold (curry Graph.add_edge class) superclasses;
   1.107 -  in
   1.108 -    ClassData.map add_class thy
   1.109 -  end;
   1.110 +  in ClassData.map add_class thy end;
   1.111  
   1.112  fun register_operation class (c, (t, some_def)) thy =
   1.113    let
   1.114 @@ -304,34 +289,40 @@
   1.115      $> Morphism.typ_morphism subst_typ
   1.116    end;
   1.117  
   1.118 -fun class_intro thy class sups =
   1.119 +fun calculate_rules thy sups base_sort assm_axiom param_map class =
   1.120    let
   1.121 -    fun class_elim class =
   1.122 -      case (#axioms o AxClass.get_info thy) class
   1.123 -       of [thm] => SOME (Drule.unconstrainTs thm)
   1.124 -        | [] => NONE;
   1.125 -    val pred_intro = case Locale.intros thy class
   1.126 -     of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME
   1.127 -      | ([intro], []) => SOME intro
   1.128 -      | ([], [intro]) => SOME intro
   1.129 -      | _ => NONE;
   1.130 -    val pred_intro' = pred_intro
   1.131 -      |> Option.map (fn intro => intro OF map_filter class_elim sups);
   1.132 -    val class_intro = (#intro o AxClass.get_info thy) class;
   1.133 -    val raw_intro = case pred_intro'
   1.134 -     of SOME pred_intro => class_intro |> OF_LAST pred_intro
   1.135 -      | NONE => class_intro;
   1.136 -    val sort = Sign.super_classes thy class;
   1.137 -    val typ = TVar ((Name.aT, 0), sort);
   1.138 -    val defs = these_defs thy sups;
   1.139 -  in
   1.140 -    raw_intro
   1.141 -    |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] []
   1.142 -    |> strip_all_ofclass thy sort
   1.143 -    |> Thm.strip_shyps
   1.144 -    |> MetaSimplifier.rewrite_rule defs
   1.145 -    |> Drule.unconstrainTs
   1.146 -  end;
   1.147 +    (*FIXME use more primitves here rather than OF, simplifify code*)
   1.148 +    fun the_option [x] = SOME x
   1.149 +      | the_option [] = NONE;
   1.150 +    fun VarA sort = TVar ((Name.aT, 0), sort);
   1.151 +    fun FreeA sort = TFree (Name.aT, sort);
   1.152 +    fun instantiate sort1 sort2 =
   1.153 +      Thm.instantiate ([pairself (Thm.ctyp_of thy) (VarA sort1, FreeA sort2)], [])
   1.154 +    val (proto_assm_intro, locale_intro) = pairself the_option (Locale.intros thy class);
   1.155 +    val inst_ty = (map_atyps o K o VarA) base_sort;
   1.156 +    val assm_intro = proto_assm_intro
   1.157 +      |> Option.map (Thm.instantiate ([],
   1.158 +           map (fn ((v, _), (c, ty)) => pairself (Thm.cterm_of thy)
   1.159 +             (Var ((v, 0), inst_ty ty), Const (c, inst_ty ty))) param_map))
   1.160 +      |> Option.map (MetaSimplifier.rewrite_rule (these_defs thy sups));
   1.161 +    val axiom_premises = map_filter (#axiom o the_class_data thy) sups
   1.162 +      @ the_list assm_axiom;
   1.163 +    val axiom = case locale_intro
   1.164 +     of SOME proto_axiom => SOME
   1.165 +          ((instantiate base_sort [class] proto_axiom OF axiom_premises) |> Drule.standard)
   1.166 +      | NONE => assm_axiom;
   1.167 +    val class_intro = (instantiate [] base_sort o #intro o AxClass.get_info thy) class;
   1.168 +    val of_class_sups = if null sups
   1.169 +      then Drule.sort_triv thy (FreeA base_sort, base_sort)
   1.170 +      else map (Drule.implies_intr_hyps o #of_class o the_class_data thy) sups;
   1.171 +    val locale_dests = map Drule.standard (Locale.dests thy class);
   1.172 +    fun mk_pred_triv () = (Thm.assume o Thm.cterm_of thy
   1.173 +      o (map_types o map_atyps o K o FreeA) base_sort o Thm.prop_of o the) axiom;
   1.174 +    val pred_trivs = case length locale_dests
   1.175 +     of 0 => if is_none locale_intro then [] else [mk_pred_triv ()]
   1.176 +      | n => replicate n (mk_pred_triv ());
   1.177 +    val of_class = class_intro OF of_class_sups OF locale_dests OF pred_trivs;
   1.178 +  in (assm_intro, of_class, axiom) end;
   1.179  
   1.180  fun class_interpretation class facts defs thy =
   1.181    let
   1.182 @@ -347,15 +338,28 @@
   1.183      |-> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs)
   1.184    end;
   1.185  
   1.186 +fun prove_subclass (sub, sup) thm thy =
   1.187 +  let
   1.188 +    val of_class = (Drule.standard o #of_class o the_class_data thy) sup;
   1.189 +    val intro = Drule.standard (of_class OF [Drule.standard thm]);
   1.190 +    val classrel = intro OF (the_list o #axiom o the_class_data thy) sub;
   1.191 +  in
   1.192 +    thy
   1.193 +    |> AxClass.add_classrel classrel
   1.194 +    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac [thm]))
   1.195 +         I (sub, Locale.Locale sup)
   1.196 +    |> ClassData.map (Graph.add_edge (sub, sup))
   1.197 +  end;
   1.198 +
   1.199  fun intro_classes_tac facts st =
   1.200    let
   1.201      val thy = Thm.theory_of_thm st;
   1.202      val classes = Sign.all_classes thy;
   1.203      val class_trivs = map (Thm.class_triv thy) classes;
   1.204 -    val class_intros = these_intros thy;
   1.205 -    val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   1.206 +    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   1.207 +    val assm_intros = these_assm_intros thy;
   1.208    in
   1.209 -    Method.intros_tac (class_trivs @ class_intros @ axclass_intros) facts st
   1.210 +    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
   1.211    end;
   1.212  
   1.213  fun default_intro_classes_tac [] = intro_classes_tac []
   1.214 @@ -371,57 +375,6 @@
   1.215    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   1.216      "apply some intro/elim rule")]);
   1.217  
   1.218 -fun subclass_rule thy (sub, sup) =
   1.219 -  let
   1.220 -    val ctxt = Locale.init sub thy;
   1.221 -    val ctxt_thy = ProofContext.init thy;
   1.222 -    val props =
   1.223 -      Locale.global_asms_of thy sup
   1.224 -      |> maps snd
   1.225 -      |> map (ObjectLogic.ensure_propT thy);
   1.226 -    fun tac { prems, context } =
   1.227 -      Locale.intro_locales_tac true context prems
   1.228 -        ORELSE ALLGOALS assume_tac;
   1.229 -  in
   1.230 -    Goal.prove_multi ctxt [] [] props tac
   1.231 -    |> map (Assumption.export false ctxt ctxt_thy)
   1.232 -    |> Variable.export ctxt ctxt_thy
   1.233 -  end;
   1.234 -
   1.235 -fun prove_single_subclass (sub, sup) thms ctxt thy =
   1.236 -  let
   1.237 -    val ctxt_thy = ProofContext.init thy;
   1.238 -    val subclass_rule = Conjunction.intr_balanced thms
   1.239 -      |> Assumption.export false ctxt ctxt_thy
   1.240 -      |> singleton (Variable.export ctxt ctxt_thy);
   1.241 -    val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub]));
   1.242 -    val sub_ax = #axioms (AxClass.get_info thy sub);
   1.243 -    val classrel =
   1.244 -      #intro (AxClass.get_info thy sup)
   1.245 -      |> Drule.instantiate' [SOME sub_inst] []
   1.246 -      |> OF_LAST (subclass_rule OF sub_ax)
   1.247 -      |> strip_all_ofclass thy (Sign.super_classes thy sup)
   1.248 -      |> Thm.strip_shyps
   1.249 -  in
   1.250 -    thy
   1.251 -    |> AxClass.add_classrel classrel
   1.252 -    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac thms))
   1.253 -         I (sub, Locale.Locale sup)
   1.254 -    |> ClassData.map (Graph.add_edge (sub, sup))
   1.255 -  end;
   1.256 -
   1.257 -fun prove_subclass (sub, sup) thms ctxt thy =
   1.258 -  let
   1.259 -    val classes = ClassData.get thy;
   1.260 -    val is_sup = not o null o curry (Graph.irreducible_paths classes) sub;
   1.261 -    val supclasses = Graph.all_succs classes [sup] |> filter_out is_sup;
   1.262 -    fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms);
   1.263 -  in
   1.264 -    thy
   1.265 -    |> fold_rev (fn sup' => prove_single_subclass (sub, sup')
   1.266 -         (transform sup') ctxt) supclasses
   1.267 - end;
   1.268 -
   1.269  
   1.270  (** classes and class target **)
   1.271  
   1.272 @@ -547,12 +500,10 @@
   1.273  fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
   1.274    let
   1.275      val supclasses = map (prep_class thy) raw_supclasses;
   1.276 -    val sups = filter (is_class thy) supclasses;
   1.277 -    fun the_base_sort class = lookup_class_data thy class
   1.278 -      |> Option.map #base_sort
   1.279 -      |> the_default [class];
   1.280 -    val base_sort = Sign.minimize_sort thy (maps the_base_sort supclasses);
   1.281      val supsort = Sign.minimize_sort thy supclasses;
   1.282 +    val sups = filter (is_class thy) supsort;
   1.283 +    val base_sort = if null sups then supsort else
   1.284 +      (#base_sort o the_class_data thy o hd) sups;
   1.285      val suplocales = map Locale.Locale sups;
   1.286      val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   1.287        | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   1.288 @@ -577,30 +528,26 @@
   1.289  val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
   1.290  val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
   1.291  
   1.292 -fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
   1.293 +fun define_class_params name class superclasses consts dep_axiom other_consts thy =
   1.294    let
   1.295 -    val superclasses = map (Sign.certify_class thy) raw_superclasses;
   1.296 -    val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
   1.297      fun add_const ((c, ty), syn) =
   1.298        Sign.declare_const [] (c, Type.strip_sorts ty, syn) #>> Term.dest_Const;
   1.299 -    fun mk_axioms cs thy =
   1.300 -      raw_dep_axioms thy cs
   1.301 -      |> (map o apsnd o map) (Sign.cert_prop thy)
   1.302 -      |> rpair thy;
   1.303 -    fun constrain_typs class = (map o apsnd o Term.map_type_tfree)
   1.304 +    val constrain_typs = (map o apsnd o Term.map_type_tfree)
   1.305        (fn (v, _) => TFree (v, [class]))
   1.306 +    fun the_option [x] = SOME x
   1.307 +      | the_option [] = NONE;
   1.308    in
   1.309      thy
   1.310      |> Sign.add_path (Logic.const_of_class name)
   1.311      |> fold_map add_const consts
   1.312      ||> Sign.restore_naming thy
   1.313 -    |-> (fn cs => mk_axioms cs
   1.314 -    #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
   1.315 -           (map fst cs @ other_consts) axioms_prop
   1.316 -    #-> (fn class => `(fn _ => constrain_typs class cs)
   1.317 -    #-> (fn cs' => `(fn thy => AxClass.get_info thy class)
   1.318 -    #-> (fn {axioms, ...} => fold (Sign.add_const_constraint o apsnd SOME) cs'
   1.319 -    #> pair (class, (cs', axioms)))))))
   1.320 +    |-> (fn cs => `(fn thy => dep_axiom thy cs)
   1.321 +    #-> (fn axiom => AxClass.define_class (name, superclasses)
   1.322 +           (map fst cs @ other_consts) [axiom]
   1.323 +    #-> (fn _ => `(fn _ => constrain_typs cs)
   1.324 +    #-> (fn cs' => `(fn thy => (the_option o #axioms o AxClass.get_info thy) class)
   1.325 +    #-> (fn axiom => fold (Sign.add_const_constraint o apsnd SOME) cs'
   1.326 +    #> pair (cs', axiom))))))
   1.327    end;
   1.328  
   1.329  fun gen_class prep_spec prep_param bname
   1.330 @@ -618,7 +565,7 @@
   1.331        | fork_syntax x = pair x;
   1.332      val (elems, global_syn) = fold_map fork_syntax elems_syn [];
   1.333      fun globalize (c, ty) =
   1.334 -      ((c, Term.map_type_tfree (K (TFree (Name.aT, base_sort))) ty),
   1.335 +      ((c, map_atyps (K (TFree (Name.aT, base_sort))) ty),
   1.336          (the_default NoSyn o AList.lookup (op =) global_syn) c);
   1.337      fun extract_params thy =
   1.338        let
   1.339 @@ -636,8 +583,10 @@
   1.340            ((Sign.base_name name, map (Attrib.attribute_i thy) atts),
   1.341              (map o map_aterms) subst ts);
   1.342        in
   1.343 -        Locale.global_asms_of thy class
   1.344 -        |> map prep_asm
   1.345 +        Locale.intros thy class
   1.346 +        |> fst
   1.347 +        |> map (map_aterms subst o Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of)
   1.348 +        |> pair (bname ^ "_" ^ AxClass.axiomsN, [])
   1.349        end;
   1.350    in
   1.351      thy
   1.352 @@ -646,20 +595,19 @@
   1.353      |> ProofContext.theory_of
   1.354      |> `extract_params
   1.355      |-> (fn (all_params, params) =>
   1.356 -        define_class_params (bname, supsort) params
   1.357 +        define_class_params bname class supsort params
   1.358            (extract_assumes params) other_consts
   1.359 -      #-> (fn (_, (consts, axioms)) =>
   1.360 -        `(fn thy => class_intro thy class sups)
   1.361 -      #-> (fn class_intro =>
   1.362 -        PureThy.note_thmss_qualified "" (NameSpace.append class classN)
   1.363 -          [((introN, []), [([class_intro], [])])]
   1.364 -      #-> (fn [(_, [class_intro])] =>
   1.365 +      #-> (fn (consts, assm_axiom) =>
   1.366 +        `(fn thy => calculate_rules thy sups base_sort assm_axiom
   1.367 +          (all_params ~~ map snd supconsts @ consts) class)
   1.368 +      #-> (fn (assm_intro, assm_proj, axiom) =>
   1.369          add_class_data ((class, sups),
   1.370            (map fst params ~~ consts, base_sort,
   1.371              mk_inst class (map snd supconsts @ consts),
   1.372 -              calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
   1.373 -      #> class_interpretation class axioms []
   1.374 -      ))))
   1.375 +              calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)),
   1.376 +          assm_intro, assm_proj, axiom))
   1.377 +      #> class_interpretation class (the_list axiom) []
   1.378 +      )))
   1.379      |> init class
   1.380      |> pair class
   1.381    end;
   1.382 @@ -688,13 +636,15 @@
   1.383      val ty' = Term.fastype_of dict_def;
   1.384      val ty'' = Type.strip_sorts ty';
   1.385      val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
   1.386 +    fun get_axiom thy = ((Thm.varifyT o Thm.symmetric o Thm.get_axiom_i thy) c', thy);
   1.387    in
   1.388      thy'
   1.389      |> Sign.declare_const pos (c, ty'', mx) |> snd
   1.390      |> Thm.add_def false false (c, def_eq)
   1.391      |>> Thm.symmetric
   1.392 -    |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
   1.393 -          #> register_operation class (c', (dict', SOME (Thm.varifyT def))))
   1.394 +    ||>> get_axiom
   1.395 +    |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def]
   1.396 +          #> register_operation class (c', (dict', SOME def')))
   1.397      |> Sign.restore_naming thy
   1.398      |> Sign.add_const_constraint (c', SOME ty')
   1.399    end;