just one data slot per module;
authorwenzelm
Sun Nov 27 22:03:22 2011 +0100 (2011-11-27)
changeset 45651172aa230ce69
parent 45650 d314a4e8038f
child 45652 18214436e1d3
just one data slot per module;
tuned;
src/HOL/Set.thy
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Set.thy	Sun Nov 27 21:53:38 2011 +0100
     1.2 +++ b/src/HOL/Set.thy	Sun Nov 27 22:03:22 2011 +0100
     1.3 @@ -1797,7 +1797,6 @@
     1.4  val bspec = @{thm bspec}
     1.5  val contra_subsetD = @{thm contra_subsetD}
     1.6  val distinct_lemma = @{thm distinct_lemma}
     1.7 -val eq_to_mono = @{thm eq_to_mono}
     1.8  val equalityCE = @{thm equalityCE}
     1.9  val equalityD1 = @{thm equalityD1}
    1.10  val equalityD2 = @{thm equalityD2}
     2.1 --- a/src/HOL/Tools/inductive.ML	Sun Nov 27 21:53:38 2011 +0100
     2.2 +++ b/src/HOL/Tools/inductive.ML	Sun Nov 27 22:03:22 2011 +0100
     2.3 @@ -27,9 +27,9 @@
     2.4    type inductive_info = {names: string list, coind: bool} * inductive_result
     2.5    val the_inductive: Proof.context -> string -> inductive_info
     2.6    val print_inductives: Proof.context -> unit
     2.7 +  val get_monos: Proof.context -> thm list
     2.8    val mono_add: attribute
     2.9    val mono_del: attribute
    2.10 -  val get_monos: Proof.context -> thm list
    2.11    val mk_cases: Proof.context -> term -> thm
    2.12    val inductive_forall_def: thm
    2.13    val rulify: thm -> thm
    2.14 @@ -88,7 +88,6 @@
    2.15  structure Inductive: INDUCTIVE =
    2.16  struct
    2.17  
    2.18 -
    2.19  (** theory context references **)
    2.20  
    2.21  val inductive_forall_def = @{thm induct_forall_def};
    2.22 @@ -114,106 +113,6 @@
    2.23  
    2.24  
    2.25  
    2.26 -(** context data **)
    2.27 -
    2.28 -type inductive_result =
    2.29 -  {preds: term list, elims: thm list, raw_induct: thm,
    2.30 -   induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
    2.31 -
    2.32 -fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
    2.33 -  let
    2.34 -    val term = Morphism.term phi;
    2.35 -    val thm = Morphism.thm phi;
    2.36 -    val fact = Morphism.fact phi;
    2.37 -  in
    2.38 -   {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
    2.39 -    induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs}
    2.40 -  end;
    2.41 -
    2.42 -type inductive_info =
    2.43 -  {names: string list, coind: bool} * inductive_result;
    2.44 -
    2.45 -structure Data = Generic_Data
    2.46 -(
    2.47 -  type T = inductive_info Symtab.table * thm list;
    2.48 -  val empty = (Symtab.empty, []);
    2.49 -  val extend = I;
    2.50 -  fun merge ((tab1, monos1), (tab2, monos2)) : T =
    2.51 -    (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2));
    2.52 -);
    2.53 -
    2.54 -val get_inductives = Data.get o Context.Proof;
    2.55 -
    2.56 -fun print_inductives ctxt =
    2.57 -  let
    2.58 -    val (tab, monos) = get_inductives ctxt;
    2.59 -    val space = Consts.space_of (Proof_Context.consts_of ctxt);
    2.60 -  in
    2.61 -    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))),
    2.62 -     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
    2.63 -    |> Pretty.chunks |> Pretty.writeln
    2.64 -  end;
    2.65 -
    2.66 -
    2.67 -(* get and put data *)
    2.68 -
    2.69 -fun the_inductive ctxt name =
    2.70 -  (case Symtab.lookup (#1 (get_inductives ctxt)) name of
    2.71 -    NONE => error ("Unknown (co)inductive predicate " ^ quote name)
    2.72 -  | SOME info => info);
    2.73 -
    2.74 -fun put_inductives names info =
    2.75 -  Data.map (apfst (fold (fn name => Symtab.update (name, info)) names));
    2.76 -
    2.77 -
    2.78 -
    2.79 -(** monotonicity rules **)
    2.80 -
    2.81 -val get_monos = #2 o get_inductives;
    2.82 -val map_monos = Data.map o apsnd;
    2.83 -
    2.84 -fun mk_mono ctxt thm =
    2.85 -  let
    2.86 -    fun eq2mono thm' = thm' RS (thm' RS eq_to_mono);
    2.87 -    fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
    2.88 -      handle THM _ => thm RS @{thm le_boolD}
    2.89 -  in
    2.90 -    (case concl_of thm of
    2.91 -      Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    2.92 -    | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq2mono thm
    2.93 -    | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
    2.94 -      dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    2.95 -        (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
    2.96 -    | _ => thm)
    2.97 -  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
    2.98 -
    2.99 -val mono_add =
   2.100 -  Thm.declaration_attribute (fn thm => fn context =>
   2.101 -    map_monos (Thm.add_thm (mk_mono (Context.proof_of context) thm)) context);
   2.102 -
   2.103 -val mono_del =
   2.104 -  Thm.declaration_attribute (fn thm => fn context =>
   2.105 -    map_monos (Thm.del_thm (mk_mono (Context.proof_of context) thm)) context);
   2.106 -
   2.107 -
   2.108 -
   2.109 -(** equations **)
   2.110 -
   2.111 -structure Equation_Data = Generic_Data   (* FIXME just one data slot per module *)
   2.112 -(
   2.113 -  type T = thm Item_Net.T;
   2.114 -  val empty = Item_Net.init (op aconv o pairself Thm.prop_of)
   2.115 -    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);  (* FIXME fragile wrt. morphisms *)
   2.116 -  val extend = I;
   2.117 -  val merge = Item_Net.merge;
   2.118 -);
   2.119 -
   2.120 -val add_equation = Thm.declaration_attribute (Equation_Data.map o Item_Net.update);
   2.121 -
   2.122 -val get_equations = Equation_Data.get o Context.Proof;
   2.123 -
   2.124 -
   2.125 -
   2.126  (** misc utilities **)
   2.127  
   2.128  fun message quiet_mode s = if quiet_mode then () else writeln s;
   2.129 @@ -222,7 +121,7 @@
   2.130  fun coind_prefix true = "co"
   2.131    | coind_prefix false = "";
   2.132  
   2.133 -fun log (b:int) m n = if m >= n then 0 else 1 + log b (b * m) n;
   2.134 +fun log (b: int) m n = if m >= n then 0 else 1 + log b (b * m) n;
   2.135  
   2.136  fun make_bool_args f g [] i = []
   2.137    | make_bool_args f g (x :: xs) i =
   2.138 @@ -269,6 +168,117 @@
   2.139  
   2.140  
   2.141  
   2.142 +(** context data **)
   2.143 +
   2.144 +type inductive_result =
   2.145 +  {preds: term list, elims: thm list, raw_induct: thm,
   2.146 +   induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
   2.147 +
   2.148 +fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
   2.149 +  let
   2.150 +    val term = Morphism.term phi;
   2.151 +    val thm = Morphism.thm phi;
   2.152 +    val fact = Morphism.fact phi;
   2.153 +  in
   2.154 +   {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
   2.155 +    induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs}
   2.156 +  end;
   2.157 +
   2.158 +type inductive_info = {names: string list, coind: bool} * inductive_result;
   2.159 +
   2.160 +val empty_equations =
   2.161 +  Item_Net.init
   2.162 +    (op aconv o pairself Thm.prop_of)
   2.163 +    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);  (* FIXME fragile wrt. morphisms *)
   2.164 +
   2.165 +datatype data = Data of
   2.166 + {infos: inductive_info Symtab.table,
   2.167 +  monos: thm list,
   2.168 +  equations: thm Item_Net.T};
   2.169 +
   2.170 +fun make_data (infos, monos, equations) =
   2.171 +  Data {infos = infos, monos = monos, equations = equations};
   2.172 +
   2.173 +structure Data = Generic_Data
   2.174 +(
   2.175 +  type T = data;
   2.176 +  val empty = make_data (Symtab.empty, [], empty_equations);
   2.177 +  val extend = I;
   2.178 +  fun merge (Data {infos = infos1, monos = monos1, equations = equations1},
   2.179 +      Data {infos = infos2, monos = monos2, equations = equations2}) =
   2.180 +    make_data (Symtab.merge (K true) (infos1, infos2),
   2.181 +      Thm.merge_thms (monos1, monos2),
   2.182 +      Item_Net.merge (equations1, equations2));
   2.183 +);
   2.184 +
   2.185 +fun map_data f =
   2.186 +  Data.map (fn Data {infos, monos, equations} => make_data (f (infos, monos, equations)));
   2.187 +
   2.188 +fun rep_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data rep => rep);
   2.189 +
   2.190 +fun print_inductives ctxt =
   2.191 +  let
   2.192 +    val {infos, monos, ...} = rep_data ctxt;
   2.193 +    val space = Consts.space_of (Proof_Context.consts_of ctxt);
   2.194 +  in
   2.195 +    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, infos))),
   2.196 +     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
   2.197 +    |> Pretty.chunks |> Pretty.writeln
   2.198 +  end;
   2.199 +
   2.200 +
   2.201 +(* inductive info *)
   2.202 +
   2.203 +fun the_inductive ctxt name =
   2.204 +  (case Symtab.lookup (#infos (rep_data ctxt)) name of
   2.205 +    NONE => error ("Unknown (co)inductive predicate " ^ quote name)
   2.206 +  | SOME info => info);
   2.207 +
   2.208 +fun put_inductives names info =
   2.209 +  map_data (fn (infos, monos, equations) =>
   2.210 +    (fold (fn name => Symtab.update (name, info)) names infos, monos, equations));
   2.211 +
   2.212 +
   2.213 +(* monotonicity rules *)
   2.214 +
   2.215 +val get_monos = #monos o rep_data;
   2.216 +
   2.217 +fun mk_mono ctxt thm =
   2.218 +  let
   2.219 +    fun eq_to_mono thm' = thm' RS (thm' RS @{thm eq_to_mono});
   2.220 +    fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
   2.221 +      handle THM _ => thm RS @{thm le_boolD}
   2.222 +  in
   2.223 +    (case concl_of thm of
   2.224 +      Const ("==", _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
   2.225 +    | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm
   2.226 +    | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
   2.227 +      dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   2.228 +        (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
   2.229 +    | _ => thm)
   2.230 +  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
   2.231 +
   2.232 +val mono_add =
   2.233 +  Thm.declaration_attribute (fn thm => fn context =>
   2.234 +    map_data (fn (infos, monos, equations) =>
   2.235 +      (infos, Thm.add_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context);
   2.236 +
   2.237 +val mono_del =
   2.238 +  Thm.declaration_attribute (fn thm => fn context =>
   2.239 +    map_data (fn (infos, monos, equations) =>
   2.240 +      (infos, Thm.del_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context);
   2.241 +
   2.242 +
   2.243 +(* equations *)
   2.244 +
   2.245 +val get_equations = #equations o rep_data;
   2.246 +
   2.247 +val equation_add =
   2.248 +  Thm.declaration_attribute (fn thm =>
   2.249 +    map_data (fn (infos, monos, equations) => (infos, monos, Item_Net.update thm equations)));
   2.250 +
   2.251 +
   2.252 +
   2.253  (** process rules **)
   2.254  
   2.255  local
   2.256 @@ -597,7 +607,7 @@
   2.257        map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
   2.258          (Term.add_vars (lhs_of eq) []);
   2.259    in
   2.260 -    cterm_instantiate inst eq
   2.261 +    Drule.cterm_instantiate inst eq
   2.262      |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite (simpset_of ctxt))))
   2.263      |> singleton (Variable.export ctxt' ctxt)
   2.264    end
   2.265 @@ -875,7 +885,7 @@
   2.266      val (eqs', lthy3) = lthy2 |>
   2.267        fold_map (fn (name, eq) => Local_Theory.note
   2.268            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
   2.269 -            [Attrib.internal (K add_equation)]), [eq])
   2.270 +            [Attrib.internal (K equation_add)]), [eq])
   2.271            #> apfst (hd o snd))
   2.272          (if null eqs then [] else (cnames ~~ eqs))
   2.273      val (inducts, lthy4) =