1.1 --- a/etc/isar-keywords.el	Tue Jul 06 08:08:35 2010 -0700
     1.2 +++ b/etc/isar-keywords.el	Wed Jul 07 08:25:21 2010 +0200
     1.3 @@ -120,6 +120,7 @@
     1.4      "inductive"
     1.5      "inductive_cases"
     1.6      "inductive_set"
     1.7 +    "inductive_simps"
     1.8      "init_toplevel"
     1.9      "instance"
    1.10      "instantiation"
    1.11 @@ -550,7 +551,8 @@
    1.12      "use"))
    1.13  
    1.14  (defconst isar-keywords-theory-script
    1.15 -  '("inductive_cases"))
    1.16 +  '("inductive_cases"
    1.17 +    "inductive_simps"))
    1.18  
    1.19  (defconst isar-keywords-theory-goal
    1.20    '("ax_specification"

     2.1 --- a/src/HOL/Tools/inductive.ML	Tue Jul 06 08:08:35 2010 -0700
     2.2 +++ b/src/HOL/Tools/inductive.ML	Wed Jul 07 08:25:21 2010 +0200
     2.3 @@ -22,7 +22,7 @@
     2.4  sig
     2.5    type inductive_result =
     2.6      {preds: term list, elims: thm list, raw_induct: thm,
     2.7 -     induct: thm, inducts: thm list, intrs: thm list}
     2.8 +     induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}
     2.9    val morph_result: morphism -> inductive_result -> inductive_result
    2.10    type inductive_info = {names: string list, coind: bool} * inductive_result
    2.11    val the_inductive: Proof.context -> string -> inductive_info
    2.12 @@ -73,7 +73,7 @@
    2.13      local_theory -> inductive_result * local_theory
    2.14    val declare_rules: binding -> bool -> bool -> string list -> term list ->
    2.15      thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
    2.16 -    thm -> local_theory -> thm list * thm list * thm * thm list * local_theory
    2.17 +    thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory
    2.18    val add_ind_def: add_ind_def
    2.19    val gen_add_inductive_i: add_ind_def -> inductive_flags ->
    2.20      ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
    2.21 @@ -120,16 +120,16 @@
    2.22  
    2.23  type inductive_result =
    2.24    {preds: term list, elims: thm list, raw_induct: thm,
    2.25 -   induct: thm, inducts: thm list, intrs: thm list};
    2.26 +   induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
    2.27  
    2.28 -fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs} =
    2.29 +fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
    2.30    let
    2.31      val term = Morphism.term phi;
    2.32      val thm = Morphism.thm phi;
    2.33      val fact = Morphism.fact phi;
    2.34    in
    2.35     {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
    2.36 -    induct = thm induct, inducts = fact inducts, intrs = fact intrs}
    2.37 +    induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs}
    2.38    end;
    2.39  
    2.40  type inductive_info =
    2.41 @@ -244,6 +244,9 @@
    2.42    | mk_names a 1 = [a]
    2.43    | mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n);
    2.44  
    2.45 +fun select_disj 1 1 = []
    2.46 +  | select_disj _ 1 = [rtac disjI1]
    2.47 +  | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    2.48  
    2.49  
    2.50  (** process rules **)
    2.51 @@ -347,10 +350,6 @@
    2.52        (mono RS (fp_def RS
    2.53          (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
    2.54  
    2.55 -    fun select_disj 1 1 = []
    2.56 -      | select_disj _ 1 = [rtac disjI1]
    2.57 -      | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    2.58 -
    2.59      val rules = [refl, TrueI, notFalseI, exI, conjI];
    2.60  
    2.61      val intrs = map_index (fn (i, intr) =>
    2.62 @@ -361,7 +360,6 @@
    2.63          (*Not ares_tac, since refl must be tried before any equality assumptions;
    2.64            backtracking may occur if the premises have extra variables!*)
    2.65          DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)])
    2.66 -       |> rulify
    2.67         |> singleton (ProofContext.export ctxt ctxt')) intr_ts
    2.68  
    2.69    in (intrs, unfold) end;
    2.70 @@ -408,14 +406,78 @@
    2.71               REPEAT (FIRSTGOAL (eresolve_tac rules2)),
    2.72               EVERY (map (fn prem =>
    2.73                 DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
    2.74 -          |> rulify
    2.75            |> singleton (ProofContext.export ctxt'' ctxt'''),
    2.76           map #2 c_intrs, length Ts)
    2.77        end
    2.78  
    2.79     in map prove_elim cs end;
    2.80  
    2.81 +(* prove simplification equations *)
    2.82  
    2.83 +fun prove_eqs quiet_mode cs params intr_ts intrs elims ctxt ctxt'' =
    2.84 +  let
    2.85 +    val _ = clean_message quiet_mode "  Proving the simplification rules ...";
    2.86 +    
    2.87 +    fun dest_intr r =
    2.88 +      (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
    2.89 +       Logic.strip_assums_hyp r, Logic.strip_params r);
    2.90 +    val intr_ts' = map dest_intr intr_ts;
    2.91 +    fun prove_eq c elim =
    2.92 +      let
    2.93 +        val Ts = arg_types_of (length params) c;
    2.94 +        val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt;
    2.95 +        val frees = map Free (anames ~~ Ts);
    2.96 +        val c_intrs = filter (equal c o #1 o #1 o #1) (intr_ts' ~~ intrs);
    2.97 +        fun mk_intr_conj (((_, _, us, _), ts, params'), _) =
    2.98 +          let
    2.99 +            fun list_ex ([], t) = t
   2.100 +              | list_ex ((a,T)::vars, t) =
   2.101 +                 (HOLogic.exists_const T) $ (Abs(a, T, list_ex(vars,t)));
   2.102 +            val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts)
   2.103 +          in
   2.104 +            list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs)
   2.105 +          end;
   2.106 +        val lhs = list_comb (c, params @ frees)
   2.107 +        val rhs =
   2.108 +          if null c_intrs then @{term False} else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs)
   2.109 +        val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   2.110 +        fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   2.111 +            let
   2.112 +              val (prems', last_prem) = split_last prems
   2.113 +            in
   2.114 +              EVERY1 (select_disj (length c_intrs) (i + 1))
   2.115 +              THEN EVERY (replicate (length params) (rtac @{thm exI} 1))
   2.116 +              THEN EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems')
   2.117 +              THEN rtac last_prem 1
   2.118 +            end) ctxt' 1
   2.119 +        fun prove_intr2 (((_, _, us, _), ts, params'), intr) =
   2.120 +          EVERY (replicate (length params') (etac @{thm exE} 1))
   2.121 +          THEN EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1))
   2.122 +          THEN Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   2.123 +            let
   2.124 +              val (eqs, prems') = chop (length us) prems
   2.125 +              val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs
   2.126 +            in
   2.127 +              rewrite_goal_tac rew_thms 1
   2.128 +              THEN rtac intr 1
   2.129 +              THEN (EVERY (map (fn p => rtac p 1) prems'))              
   2.130 +            end) ctxt' 1 
   2.131 +      in
   2.132 +        Skip_Proof.prove ctxt' [] [] eq (fn {...} =>
   2.133 +          rtac @{thm iffI} 1 THEN etac (#1 elim) 1
   2.134 +          THEN EVERY (map_index prove_intr1 c_intrs)
   2.135 +          THEN (if null c_intrs then etac @{thm FalseE} 1 else
   2.136 +            let val (c_intrs', last_c_intr) = split_last c_intrs in
   2.137 +              EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs')
   2.138 +              THEN prove_intr2 last_c_intr
   2.139 +            end))
   2.140 +        |> rulify
   2.141 +        |> singleton (ProofContext.export ctxt' ctxt'')
   2.142 +      end;  
   2.143 +  in
   2.144 +    map2 prove_eq cs elims
   2.145 +  end;
   2.146 +  
   2.147  (* derivation of simplified elimination rules *)
   2.148  
   2.149  local
   2.150 @@ -455,7 +517,6 @@
   2.151  
   2.152  end;
   2.153  
   2.154 -
   2.155  (* inductive_cases *)
   2.156  
   2.157  fun gen_inductive_cases prep_att prep_prop args lthy =
   2.158 @@ -483,7 +544,37 @@
   2.159          in Method.erule 0 rules end))
   2.160      "dynamic case analysis on predicates";
   2.161  
   2.162 +(* derivation of simplified equation *)
   2.163  
   2.164 +fun mk_simp_eq ctxt prop =
   2.165 +  let
   2.166 +    val (c, args) = strip_comb (HOLogic.dest_Trueprop prop)
   2.167 +    val ctxt' = Variable.auto_fixes prop ctxt
   2.168 +    val cname = fst (dest_Const c)
   2.169 +    val info = the_inductive ctxt cname
   2.170 +    val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info)))
   2.171 +    val (_, args') = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq))))
   2.172 +    val certify = cterm_of (ProofContext.theory_of ctxt)
   2.173 +  in
   2.174 +    cterm_instantiate (map (pairself certify) (args' ~~ args)) eq
   2.175 +    |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
   2.176 +      (Simplifier.full_rewrite (simpset_of ctxt))))
   2.177 +    |> singleton (Variable.export ctxt' ctxt)
   2.178 +  end
   2.179 +
   2.180 +(* inductive simps *)
   2.181 +
   2.182 +fun gen_inductive_simps prep_att prep_prop args lthy =
   2.183 +  let
   2.184 +    val thy = ProofContext.theory_of lthy;
   2.185 +    val facts = args |> map (fn ((a, atts), props) =>
   2.186 +      ((a, map (prep_att thy) atts),
   2.187 +        map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
   2.188 +  in lthy |> Local_Theory.notes facts |>> map snd end;
   2.189 +
   2.190 +val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
   2.191 +val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
   2.192 +    
   2.193  (* prove induction rule *)
   2.194  
   2.195  fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
   2.196 @@ -697,7 +788,7 @@
   2.197    end;
   2.198  
   2.199  fun declare_rules rec_binding coind no_ind cnames
   2.200 -    preds intrs intr_bindings intr_atts elims raw_induct lthy =
   2.201 +    preds intrs intr_bindings intr_atts elims eqs raw_induct lthy =
   2.202    let
   2.203      val rec_name = Binding.name_of rec_binding;
   2.204      fun rec_qualified qualified = Binding.qualify qualified rec_name;
   2.205 @@ -737,18 +828,23 @@
   2.206          ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
   2.207            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
   2.208  
   2.209 -    val (inducts, lthy3) =
   2.210 -      if no_ind orelse coind then ([], lthy2)
   2.211 +    val (eqs', lthy3) = lthy2 |> 
   2.212 +      fold_map (fn (name, eq) => Local_Theory.note
   2.213 +          ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), []), [eq])
   2.214 +          #> apfst (hd o snd))
   2.215 +        (if null eqs then [] else (cnames ~~ eqs))
   2.216 +    val (inducts, lthy4) =
   2.217 +      if no_ind orelse coind then ([], lthy3)
   2.218        else
   2.219 -        let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
   2.220 -          lthy2 |>
   2.221 +        let val inducts = cnames ~~ Project_Rule.projects lthy3 (1 upto length cnames) induct' in
   2.222 +          lthy3 |>
   2.223            Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
   2.224              inducts |> map (fn (name, th) => ([th],
   2.225                [Attrib.internal (K ind_case_names),
   2.226                 Attrib.internal (K (Rule_Cases.consumes 1)),
   2.227                 Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
   2.228          end;
   2.229 -  in (intrs', elims', induct', inducts, lthy3) end;
   2.230 +  in (intrs', elims', eqs', induct', inducts, lthy4) end;
   2.231  
   2.232  type inductive_flags =
   2.233    {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
   2.234 @@ -794,17 +890,23 @@
   2.235         else
   2.236           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
   2.237             rec_preds_defs lthy2 lthy1);
   2.238 +    val eqs =
   2.239 +      if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1
   2.240  
   2.241 -    val (intrs', elims', induct, inducts, lthy3) = declare_rules rec_name coind no_ind
   2.242 -      cnames preds intrs intr_names intr_atts elims raw_induct lthy1;
   2.243 +    val elims' = map (fn (th, ns, i) => (rulify th, ns, i)) elims
   2.244 +    val intrs' = map rulify intrs
   2.245 +
   2.246 +    val (intrs'', elims'', eqs', induct, inducts, lthy3) = declare_rules rec_name coind no_ind
   2.247 +      cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
   2.248  
   2.249      val result =
   2.250        {preds = preds,
   2.251 -       intrs = intrs',
   2.252 -       elims = elims',
   2.253 +       intrs = intrs'',
   2.254 +       elims = elims'',
   2.255         raw_induct = rulify raw_induct,
   2.256         induct = induct,
   2.257 -       inducts = inducts};
   2.258 +       inducts = inducts,
   2.259 +       eqs = eqs'};
   2.260  
   2.261      val lthy4 = lthy3
   2.262        |> Local_Theory.declaration false (fn phi =>
   2.263 @@ -993,4 +1095,9 @@
   2.264      "create simplified instances of elimination rules (improper)" Keyword.thy_script
   2.265      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
   2.266  
   2.267 +val _ =
   2.268 +  Outer_Syntax.local_theory "inductive_simps"
   2.269 +    "create simplification rules for inductive predicates" Keyword.thy_script
   2.270 +    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
   2.271 +
   2.272  end;

     3.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Jul 06 08:08:35 2010 -0700
     3.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Jul 07 08:25:21 2010 +0200
     3.3 @@ -520,16 +520,17 @@
     3.4      val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
     3.5      val (intr_names, intr_atts) = split_list (map fst intros);
     3.6      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     3.7 -    val (intrs', elims', induct, inducts, lthy4) =
     3.8 +    val eqs = [] (* TODO: define equations *)
     3.9 +    val (intrs', elims', eqs', induct, inducts, lthy4) =
    3.10        Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
    3.11          (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
    3.12          (map (fn th => (to_set [] (Context.Proof lthy3) th,
    3.13             map fst (fst (Rule_Cases.get th)),
    3.14             Rule_Cases.get_constraints th)) elims)
    3.15 -        raw_induct' lthy3;
    3.16 +        eqs raw_induct' lthy3;
    3.17    in
    3.18      ({intrs = intrs', elims = elims', induct = induct, inducts = inducts,
    3.19 -      raw_induct = raw_induct', preds = map fst defs},
    3.20 +      raw_induct = raw_induct', preds = map fst defs, eqs = eqs'},
    3.21       lthy4)
    3.22    end;
    3.23