src/HOL/Tools/inductive.ML
changeset 45651 172aa230ce69
parent 45649 2d995773da1a
child 45652 18214436e1d3
     1.1 --- a/src/HOL/Tools/inductive.ML	Sun Nov 27 21:53:38 2011 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sun Nov 27 22:03:22 2011 +0100
     1.3 @@ -27,9 +27,9 @@
     1.4    type inductive_info = {names: string list, coind: bool} * inductive_result
     1.5    val the_inductive: Proof.context -> string -> inductive_info
     1.6    val print_inductives: Proof.context -> unit
     1.7 +  val get_monos: Proof.context -> thm list
     1.8    val mono_add: attribute
     1.9    val mono_del: attribute
    1.10 -  val get_monos: Proof.context -> thm list
    1.11    val mk_cases: Proof.context -> term -> thm
    1.12    val inductive_forall_def: thm
    1.13    val rulify: thm -> thm
    1.14 @@ -88,7 +88,6 @@
    1.15  structure Inductive: INDUCTIVE =
    1.16  struct
    1.17  
    1.18 -
    1.19  (** theory context references **)
    1.20  
    1.21  val inductive_forall_def = @{thm induct_forall_def};
    1.22 @@ -114,106 +113,6 @@
    1.23  
    1.24  
    1.25  
    1.26 -(** context data **)
    1.27 -
    1.28 -type inductive_result =
    1.29 -  {preds: term list, elims: thm list, raw_induct: thm,
    1.30 -   induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
    1.31 -
    1.32 -fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
    1.33 -  let
    1.34 -    val term = Morphism.term phi;
    1.35 -    val thm = Morphism.thm phi;
    1.36 -    val fact = Morphism.fact phi;
    1.37 -  in
    1.38 -   {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
    1.39 -    induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs}
    1.40 -  end;
    1.41 -
    1.42 -type inductive_info =
    1.43 -  {names: string list, coind: bool} * inductive_result;
    1.44 -
    1.45 -structure Data = Generic_Data
    1.46 -(
    1.47 -  type T = inductive_info Symtab.table * thm list;
    1.48 -  val empty = (Symtab.empty, []);
    1.49 -  val extend = I;
    1.50 -  fun merge ((tab1, monos1), (tab2, monos2)) : T =
    1.51 -    (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2));
    1.52 -);
    1.53 -
    1.54 -val get_inductives = Data.get o Context.Proof;
    1.55 -
    1.56 -fun print_inductives ctxt =
    1.57 -  let
    1.58 -    val (tab, monos) = get_inductives ctxt;
    1.59 -    val space = Consts.space_of (Proof_Context.consts_of ctxt);
    1.60 -  in
    1.61 -    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))),
    1.62 -     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
    1.63 -    |> Pretty.chunks |> Pretty.writeln
    1.64 -  end;
    1.65 -
    1.66 -
    1.67 -(* get and put data *)
    1.68 -
    1.69 -fun the_inductive ctxt name =
    1.70 -  (case Symtab.lookup (#1 (get_inductives ctxt)) name of
    1.71 -    NONE => error ("Unknown (co)inductive predicate " ^ quote name)
    1.72 -  | SOME info => info);
    1.73 -
    1.74 -fun put_inductives names info =
    1.75 -  Data.map (apfst (fold (fn name => Symtab.update (name, info)) names));
    1.76 -
    1.77 -
    1.78 -
    1.79 -(** monotonicity rules **)
    1.80 -
    1.81 -val get_monos = #2 o get_inductives;
    1.82 -val map_monos = Data.map o apsnd;
    1.83 -
    1.84 -fun mk_mono ctxt thm =
    1.85 -  let
    1.86 -    fun eq2mono thm' = thm' RS (thm' RS eq_to_mono);
    1.87 -    fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
    1.88 -      handle THM _ => thm RS @{thm le_boolD}
    1.89 -  in
    1.90 -    (case concl_of thm of
    1.91 -      Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    1.92 -    | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq2mono thm
    1.93 -    | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
    1.94 -      dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    1.95 -        (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
    1.96 -    | _ => thm)
    1.97 -  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
    1.98 -
    1.99 -val mono_add =
   1.100 -  Thm.declaration_attribute (fn thm => fn context =>
   1.101 -    map_monos (Thm.add_thm (mk_mono (Context.proof_of context) thm)) context);
   1.102 -
   1.103 -val mono_del =
   1.104 -  Thm.declaration_attribute (fn thm => fn context =>
   1.105 -    map_monos (Thm.del_thm (mk_mono (Context.proof_of context) thm)) context);
   1.106 -
   1.107 -
   1.108 -
   1.109 -(** equations **)
   1.110 -
   1.111 -structure Equation_Data = Generic_Data   (* FIXME just one data slot per module *)
   1.112 -(
   1.113 -  type T = thm Item_Net.T;
   1.114 -  val empty = Item_Net.init (op aconv o pairself Thm.prop_of)
   1.115 -    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);  (* FIXME fragile wrt. morphisms *)
   1.116 -  val extend = I;
   1.117 -  val merge = Item_Net.merge;
   1.118 -);
   1.119 -
   1.120 -val add_equation = Thm.declaration_attribute (Equation_Data.map o Item_Net.update);
   1.121 -
   1.122 -val get_equations = Equation_Data.get o Context.Proof;
   1.123 -
   1.124 -
   1.125 -
   1.126  (** misc utilities **)
   1.127  
   1.128  fun message quiet_mode s = if quiet_mode then () else writeln s;
   1.129 @@ -222,7 +121,7 @@
   1.130  fun coind_prefix true = "co"
   1.131    | coind_prefix false = "";
   1.132  
   1.133 -fun log (b:int) m n = if m >= n then 0 else 1 + log b (b * m) n;
   1.134 +fun log (b: int) m n = if m >= n then 0 else 1 + log b (b * m) n;
   1.135  
   1.136  fun make_bool_args f g [] i = []
   1.137    | make_bool_args f g (x :: xs) i =
   1.138 @@ -269,6 +168,117 @@
   1.139  
   1.140  
   1.141  
   1.142 +(** context data **)
   1.143 +
   1.144 +type inductive_result =
   1.145 +  {preds: term list, elims: thm list, raw_induct: thm,
   1.146 +   induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
   1.147 +
   1.148 +fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
   1.149 +  let
   1.150 +    val term = Morphism.term phi;
   1.151 +    val thm = Morphism.thm phi;
   1.152 +    val fact = Morphism.fact phi;
   1.153 +  in
   1.154 +   {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
   1.155 +    induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs}
   1.156 +  end;
   1.157 +
   1.158 +type inductive_info = {names: string list, coind: bool} * inductive_result;
   1.159 +
   1.160 +val empty_equations =
   1.161 +  Item_Net.init
   1.162 +    (op aconv o pairself Thm.prop_of)
   1.163 +    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);  (* FIXME fragile wrt. morphisms *)
   1.164 +
   1.165 +datatype data = Data of
   1.166 + {infos: inductive_info Symtab.table,
   1.167 +  monos: thm list,
   1.168 +  equations: thm Item_Net.T};
   1.169 +
   1.170 +fun make_data (infos, monos, equations) =
   1.171 +  Data {infos = infos, monos = monos, equations = equations};
   1.172 +
   1.173 +structure Data = Generic_Data
   1.174 +(
   1.175 +  type T = data;
   1.176 +  val empty = make_data (Symtab.empty, [], empty_equations);
   1.177 +  val extend = I;
   1.178 +  fun merge (Data {infos = infos1, monos = monos1, equations = equations1},
   1.179 +      Data {infos = infos2, monos = monos2, equations = equations2}) =
   1.180 +    make_data (Symtab.merge (K true) (infos1, infos2),
   1.181 +      Thm.merge_thms (monos1, monos2),
   1.182 +      Item_Net.merge (equations1, equations2));
   1.183 +);
   1.184 +
   1.185 +fun map_data f =
   1.186 +  Data.map (fn Data {infos, monos, equations} => make_data (f (infos, monos, equations)));
   1.187 +
   1.188 +fun rep_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data rep => rep);
   1.189 +
   1.190 +fun print_inductives ctxt =
   1.191 +  let
   1.192 +    val {infos, monos, ...} = rep_data ctxt;
   1.193 +    val space = Consts.space_of (Proof_Context.consts_of ctxt);
   1.194 +  in
   1.195 +    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, infos))),
   1.196 +     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
   1.197 +    |> Pretty.chunks |> Pretty.writeln
   1.198 +  end;
   1.199 +
   1.200 +
   1.201 +(* inductive info *)
   1.202 +
   1.203 +fun the_inductive ctxt name =
   1.204 +  (case Symtab.lookup (#infos (rep_data ctxt)) name of
   1.205 +    NONE => error ("Unknown (co)inductive predicate " ^ quote name)
   1.206 +  | SOME info => info);
   1.207 +
   1.208 +fun put_inductives names info =
   1.209 +  map_data (fn (infos, monos, equations) =>
   1.210 +    (fold (fn name => Symtab.update (name, info)) names infos, monos, equations));
   1.211 +
   1.212 +
   1.213 +(* monotonicity rules *)
   1.214 +
   1.215 +val get_monos = #monos o rep_data;
   1.216 +
   1.217 +fun mk_mono ctxt thm =
   1.218 +  let
   1.219 +    fun eq_to_mono thm' = thm' RS (thm' RS @{thm eq_to_mono});
   1.220 +    fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
   1.221 +      handle THM _ => thm RS @{thm le_boolD}
   1.222 +  in
   1.223 +    (case concl_of thm of
   1.224 +      Const ("==", _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
   1.225 +    | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm
   1.226 +    | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
   1.227 +      dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   1.228 +        (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
   1.229 +    | _ => thm)
   1.230 +  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
   1.231 +
   1.232 +val mono_add =
   1.233 +  Thm.declaration_attribute (fn thm => fn context =>
   1.234 +    map_data (fn (infos, monos, equations) =>
   1.235 +      (infos, Thm.add_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context);
   1.236 +
   1.237 +val mono_del =
   1.238 +  Thm.declaration_attribute (fn thm => fn context =>
   1.239 +    map_data (fn (infos, monos, equations) =>
   1.240 +      (infos, Thm.del_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context);
   1.241 +
   1.242 +
   1.243 +(* equations *)
   1.244 +
   1.245 +val get_equations = #equations o rep_data;
   1.246 +
   1.247 +val equation_add =
   1.248 +  Thm.declaration_attribute (fn thm =>
   1.249 +    map_data (fn (infos, monos, equations) => (infos, monos, Item_Net.update thm equations)));
   1.250 +
   1.251 +
   1.252 +
   1.253  (** process rules **)
   1.254  
   1.255  local
   1.256 @@ -597,7 +607,7 @@
   1.257        map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
   1.258          (Term.add_vars (lhs_of eq) []);
   1.259    in
   1.260 -    cterm_instantiate inst eq
   1.261 +    Drule.cterm_instantiate inst eq
   1.262      |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite (simpset_of ctxt))))
   1.263      |> singleton (Variable.export ctxt' ctxt)
   1.264    end
   1.265 @@ -875,7 +885,7 @@
   1.266      val (eqs', lthy3) = lthy2 |>
   1.267        fold_map (fn (name, eq) => Local_Theory.note
   1.268            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
   1.269 -            [Attrib.internal (K add_equation)]), [eq])
   1.270 +            [Attrib.internal (K equation_add)]), [eq])
   1.271            #> apfst (hd o snd))
   1.272          (if null eqs then [] else (cnames ~~ eqs))
   1.273      val (inducts, lthy4) =