1.1 --- a/src/Pure/Tools/class_package.ML Tue Jul 24 15:20:50 2007 +0200
1.2 +++ b/src/Pure/Tools/class_package.ML Tue Jul 24 15:20:51 2007 +0200
1.3 @@ -29,7 +29,6 @@
1.4 val instance_sort_cmd: string * string -> theory -> Proof.state
1.5 val prove_instance_sort: tactic -> class * sort -> theory -> theory
1.6
1.7 - val INTERPRET_DEF: bool ref
1.8 val class_of_locale: theory -> string -> class option
1.9 val add_const_in_class: string -> (string * term) * Syntax.mixfix
1.10 -> theory -> theory
1.11 @@ -210,7 +209,7 @@
1.12 |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities)
1.13 end;
1.14
1.15 -fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
1.16 +fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
1.17 fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof;
1.18 fun tactic_proof tac after_qed arities =
1.19 fold (fn arity => AxClass.prove_arity arity tac) arities
1.20 @@ -218,7 +217,7 @@
1.21
1.22 in
1.23
1.24 -val instance_arity_cmd = instance_arity_e' axclass_instance_arity;
1.25 +val instance_arity_cmd = instance_arity_cmd' axclass_instance_arity;
1.26 val instance_arity = instance_arity' axclass_instance_arity;
1.27 val prove_instance_arity = instance_arity' o tactic_proof;
1.28
1.29 @@ -235,9 +234,7 @@
1.30 consts: (string * string) list
1.31 (*locale parameter ~> toplevel theory constant*),
1.32 v: string option,
1.33 - intro: thm,
1.34 - propnames: string list
1.35 - (*for ad-hoc instance_in*)
1.36 + intro: thm
1.37 };
1.38
1.39 fun rep_classdata (ClassData c) = c;
1.40 @@ -281,8 +278,6 @@
1.41 Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_classdata) data))
1.42 ((fst o ClassData.get) thy) [];
1.43
1.44 -val the_propnames = #propnames oo the_class_data;
1.45 -
1.46 fun print_classes thy =
1.47 let
1.48 val algebra = Sign.classes_of thy;
1.49 @@ -318,15 +313,14 @@
1.50
1.51 (* updaters *)
1.52
1.53 -fun add_class_data ((class, superclasses), (locale, consts, v, intro, propnames)) =
1.54 +fun add_class_data ((class, superclasses), (locale, consts, v, intro)) =
1.55 ClassData.map (fn (gr, tab) => (
1.56 gr
1.57 |> Graph.new_node (class, ClassData {
1.58 locale = locale,
1.59 consts = consts,
1.60 v = v,
1.61 - intro = intro,
1.62 - propnames = propnames}
1.63 + intro = intro}
1.64 )
1.65 |> fold (curry Graph.add_edge class) superclasses,
1.66 tab
1.67 @@ -380,56 +374,38 @@
1.68 |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
1.69 |> ProofContext.theory_of;
1.70
1.71 -fun instance_sort' do_proof (class, sort) theory =
1.72 +
1.73 +(* constructing class introduction and other rules from axclass and locale rules *)
1.74 +
1.75 +fun mk_instT class = Symtab.empty
1.76 + |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
1.77 +
1.78 +fun mk_inst class param_names cs =
1.79 + Symtab.empty
1.80 + |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
1.81 + (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
1.82 +
1.83 +fun OF_LAST thm1 thm2 =
1.84 let
1.85 - val loc_name = (#locale o the_class_data theory) class;
1.86 - val loc_expr =
1.87 - (Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort;
1.88 - val const_names = (map (NameSpace.base o snd)
1.89 - o maps (#consts o the_class_data theory)
1.90 - o ancestry theory) [class];
1.91 - fun get_thms thy =
1.92 - ancestry thy sort
1.93 - |> AList.make (the_propnames thy)
1.94 - |> map (apsnd (map (NameSpace.append (Logic.const_of_class loc_name))))
1.95 - |> map_filter (fn (superclass, thm_names) =>
1.96 - case map_filter (try (PureThy.get_thm thy o Name)) thm_names
1.97 - of [] => NONE
1.98 - | thms => SOME (superclass, thms));
1.99 - fun after_qed thy =
1.100 - thy
1.101 - |> `get_thms
1.102 - |-> fold (fn (supclass, thms) => I
1.103 - AxClass.prove_classrel (class, supclass)
1.104 - (ALLGOALS (K (intro_classes_tac [])) THEN
1.105 - (ALLGOALS o ProofContext.fact_tac) thms))
1.106 - in
1.107 - theory
1.108 - |> do_proof after_qed (loc_name, loc_expr)
1.109 - end;
1.110 + val n = (length o Logic.strip_imp_prems o prop_of) thm2;
1.111 + in (thm1 RSN (n, thm2)) end;
1.112
1.113 -val prove_instance_sort = instance_sort' o prove_interpretation_in;
1.114 -
1.115 -
1.116 -(* constructing class introduction rules from axclass and locale rules *)
1.117 -
1.118 -fun class_intro thy locale class sups =
1.119 +fun strip_all_ofclass thy sort =
1.120 let
1.121 - fun OF_LAST thm1 thm2 =
1.122 - let
1.123 - val n = (length o Logic.strip_imp_prems o prop_of) thm2;
1.124 - in (thm1 RSN (n, thm2)) end;
1.125 + val typ = TVar ((AxClass.param_tyvarname, 0), sort);
1.126 fun prem_inclass t =
1.127 case Logic.strip_imp_prems t
1.128 of ofcls :: _ => try Logic.dest_inclass ofcls
1.129 | [] => NONE;
1.130 - val typ = TVar ((AxClass.param_tyvarname, 0), Sign.super_classes thy class);
1.131 fun strip_ofclass class thm =
1.132 thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
1.133 - fun strip_all_ofclass thm =
1.134 - case (prem_inclass o Thm.prop_of) thm
1.135 - of SOME (_, class) => thm |> strip_ofclass class |> strip_all_ofclass
1.136 - | NONE => thm;
1.137 + fun strip thm = case (prem_inclass o Thm.prop_of) thm
1.138 + of SOME (_, class) => thm |> strip_ofclass class |> strip
1.139 + | NONE => thm;
1.140 + in strip end;
1.141 +
1.142 +fun class_intro thy locale class sups =
1.143 + let
1.144 fun class_elim class =
1.145 case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class
1.146 of [thm] => SOME thm
1.147 @@ -445,24 +421,39 @@
1.148 val raw_intro = case pred_intro'
1.149 of SOME pred_intro => class_intro |> OF_LAST pred_intro
1.150 | NONE => class_intro;
1.151 + val sort = Sign.super_classes thy class;
1.152 + val typ = TVar ((AxClass.param_tyvarname, 0), sort);
1.153 in
1.154 raw_intro
1.155 |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] []
1.156 - |> strip_all_ofclass
1.157 + |> strip_all_ofclass thy sort
1.158 |> Thm.strip_shyps
1.159 |> Drule.unconstrainTs
1.160 end;
1.161
1.162 +fun interpretation_in_rule thy (class1, class2) =
1.163 + let
1.164 + val (params, consts) = split_list (param_map thy [class1]);
1.165 + (*FIXME also remember this at add_class*)
1.166 + fun mk_axioms class =
1.167 + let
1.168 + val name_locale = (#locale o the_class_data thy) class;
1.169 + val inst = mk_inst class params consts;
1.170 + in
1.171 + Locale.global_asms_of thy name_locale
1.172 + |> maps snd
1.173 + |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup inst) s | t => t)
1.174 + |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T)
1.175 + |> map (ObjectLogic.ensure_propT thy)
1.176 + end;
1.177 + val (prems, concls) = pairself mk_axioms (class1, class2);
1.178 + in
1.179 + Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls)
1.180 + (Locale.intro_locales_tac true (ProofContext.init thy))
1.181 + end;
1.182
1.183 -(* classes and instances *)
1.184
1.185 -fun mk_instT class = Symtab.empty
1.186 - |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
1.187 -
1.188 -fun mk_inst class param_names cs =
1.189 - Symtab.empty
1.190 - |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
1.191 - (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
1.192 +(* classes *)
1.193
1.194 local
1.195
1.196 @@ -530,10 +521,6 @@
1.197 Locale.global_asms_of thy name_locale
1.198 |> map prep_asm
1.199 end;
1.200 - fun extract_axiom_names thy name_locale =
1.201 - name_locale
1.202 - |> Locale.global_asms_of thy
1.203 - |> map (NameSpace.base o fst o fst) (*FIXME - is finally dropped*);
1.204 fun note_intro name_axclass class_intro =
1.205 PureThy.note_thmss_qualified "" ((Logic.const_of_class o NameSpace.base) name_axclass)
1.206 [(("intro", []), [([class_intro], [])])]
1.207 @@ -547,11 +534,10 @@
1.208 axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts
1.209 #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
1.210 `(fn thy => class_intro thy name_locale name_axclass sups)
1.211 - ##>> `(fn thy => extract_axiom_names thy name_locale)
1.212 - #-> (fn (class_intro, axiom_names) =>
1.213 + #-> (fn class_intro =>
1.214 add_class_data ((name_axclass, sups),
1.215 (name_locale, map (fst o fst) params ~~ map fst consts, v,
1.216 - class_intro, axiom_names))
1.217 + class_intro))
1.218 (*FIXME: class_data should already contain data relevant
1.219 for interpretation; use this later for class target*)
1.220 (*FIXME: general export_fixes which may be parametrized
1.221 @@ -573,6 +559,41 @@
1.222
1.223 local
1.224
1.225 +fun singular_instance_subclass (class1, class2) thy =
1.226 + let
1.227 + val interp = interpretation_in_rule thy (class1, class2);
1.228 + val ax = #axioms (AxClass.get_definition thy class1);
1.229 + val intro = #intro (AxClass.get_definition thy class2)
1.230 + |> Drule.instantiate' [SOME (Thm.ctyp_of thy
1.231 + (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
1.232 + val thm =
1.233 + intro
1.234 + |> OF_LAST (interp OF ax)
1.235 + |> strip_all_ofclass thy (Sign.super_classes thy class2);
1.236 + in
1.237 + thy |> AxClass.add_classrel thm
1.238 + end;
1.239 +
1.240 +fun instance_subsort (class, sort) thy =
1.241 + let
1.242 + val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra
1.243 + o Sign.classes_of) thy sort;
1.244 + val classes = filter_out (fn class' => Sign.subsort thy ([class], [class']))
1.245 + (rev super_sort);
1.246 + in
1.247 + thy |> fold (curry singular_instance_subclass class) classes
1.248 + end;
1.249 +
1.250 +fun instance_sort' do_proof (class, sort) theory =
1.251 + let
1.252 + val loc_name = (#locale o the_class_data theory) class;
1.253 + val loc_expr =
1.254 + (Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort;
1.255 + in
1.256 + theory
1.257 + |> do_proof (instance_subsort (class, sort)) (loc_name, loc_expr)
1.258 + end;
1.259 +
1.260 fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory =
1.261 let
1.262 val class = prep_class theory raw_class;
1.263 @@ -595,6 +616,7 @@
1.264
1.265 val instance_sort_cmd = gen_instance_sort Sign.read_class Sign.read_sort;
1.266 val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort;
1.267 +val prove_instance_sort = instance_sort' o prove_interpretation_in;
1.268 val instance_class_cmd = gen_instance_class Sign.read_class;
1.269 val instance_class = gen_instance_class Sign.certify_class;
1.270
1.271 @@ -603,8 +625,6 @@
1.272
1.273 (** class target **)
1.274
1.275 -val INTERPRET_DEF = ref false;
1.276 -
1.277 fun export_fixes thy class =
1.278 let
1.279 val v = (#v o the_class_data thy) class;
1.280 @@ -651,8 +671,12 @@
1.281 |> Sign.parent_path
1.282 |> Sign.sticky_prefix prfx
1.283 |> PureThy.add_defs_i false [(def, [])]
1.284 - |-> (fn [def] => ! INTERPRET_DEF ? interpret def)
1.285 + |-> (fn [def] => interpret def)
1.286 |> Sign.restore_naming thy
1.287 end;
1.288
1.289 +
1.290 +(** experimental interpretation_in **)
1.291 +
1.292 +
1.293 end;