src/HOL/Tools/inductive.ML
changeset 37734 489ac1ecb9f1
parent 37264 8b931fb51cc6
child 37901 ea7d4423cb5b
     1.1 --- a/src/HOL/Tools/inductive.ML	Tue Jul 06 08:08:35 2010 -0700
     1.2 +++ b/src/HOL/Tools/inductive.ML	Wed Jul 07 08:25:21 2010 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  sig
     1.5    type inductive_result =
     1.6      {preds: term list, elims: thm list, raw_induct: thm,
     1.7 -     induct: thm, inducts: thm list, intrs: thm list}
     1.8 +     induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}
     1.9    val morph_result: morphism -> inductive_result -> inductive_result
    1.10    type inductive_info = {names: string list, coind: bool} * inductive_result
    1.11    val the_inductive: Proof.context -> string -> inductive_info
    1.12 @@ -73,7 +73,7 @@
    1.13      local_theory -> inductive_result * local_theory
    1.14    val declare_rules: binding -> bool -> bool -> string list -> term list ->
    1.15      thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
    1.16 -    thm -> local_theory -> thm list * thm list * thm * thm list * local_theory
    1.17 +    thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory
    1.18    val add_ind_def: add_ind_def
    1.19    val gen_add_inductive_i: add_ind_def -> inductive_flags ->
    1.20      ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
    1.21 @@ -120,16 +120,16 @@
    1.22  
    1.23  type inductive_result =
    1.24    {preds: term list, elims: thm list, raw_induct: thm,
    1.25 -   induct: thm, inducts: thm list, intrs: thm list};
    1.26 +   induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
    1.27  
    1.28 -fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs} =
    1.29 +fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
    1.30    let
    1.31      val term = Morphism.term phi;
    1.32      val thm = Morphism.thm phi;
    1.33      val fact = Morphism.fact phi;
    1.34    in
    1.35     {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
    1.36 -    induct = thm induct, inducts = fact inducts, intrs = fact intrs}
    1.37 +    induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs}
    1.38    end;
    1.39  
    1.40  type inductive_info =
    1.41 @@ -244,6 +244,9 @@
    1.42    | mk_names a 1 = [a]
    1.43    | mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n);
    1.44  
    1.45 +fun select_disj 1 1 = []
    1.46 +  | select_disj _ 1 = [rtac disjI1]
    1.47 +  | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    1.48  
    1.49  
    1.50  (** process rules **)
    1.51 @@ -347,10 +350,6 @@
    1.52        (mono RS (fp_def RS
    1.53          (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
    1.54  
    1.55 -    fun select_disj 1 1 = []
    1.56 -      | select_disj _ 1 = [rtac disjI1]
    1.57 -      | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    1.58 -
    1.59      val rules = [refl, TrueI, notFalseI, exI, conjI];
    1.60  
    1.61      val intrs = map_index (fn (i, intr) =>
    1.62 @@ -361,7 +360,6 @@
    1.63          (*Not ares_tac, since refl must be tried before any equality assumptions;
    1.64            backtracking may occur if the premises have extra variables!*)
    1.65          DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)])
    1.66 -       |> rulify
    1.67         |> singleton (ProofContext.export ctxt ctxt')) intr_ts
    1.68  
    1.69    in (intrs, unfold) end;
    1.70 @@ -408,14 +406,78 @@
    1.71               REPEAT (FIRSTGOAL (eresolve_tac rules2)),
    1.72               EVERY (map (fn prem =>
    1.73                 DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
    1.74 -          |> rulify
    1.75            |> singleton (ProofContext.export ctxt'' ctxt'''),
    1.76           map #2 c_intrs, length Ts)
    1.77        end
    1.78  
    1.79     in map prove_elim cs end;
    1.80  
    1.81 +(* prove simplification equations *)
    1.82  
    1.83 +fun prove_eqs quiet_mode cs params intr_ts intrs elims ctxt ctxt'' =
    1.84 +  let
    1.85 +    val _ = clean_message quiet_mode "  Proving the simplification rules ...";
    1.86 +    
    1.87 +    fun dest_intr r =
    1.88 +      (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
    1.89 +       Logic.strip_assums_hyp r, Logic.strip_params r);
    1.90 +    val intr_ts' = map dest_intr intr_ts;
    1.91 +    fun prove_eq c elim =
    1.92 +      let
    1.93 +        val Ts = arg_types_of (length params) c;
    1.94 +        val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt;
    1.95 +        val frees = map Free (anames ~~ Ts);
    1.96 +        val c_intrs = filter (equal c o #1 o #1 o #1) (intr_ts' ~~ intrs);
    1.97 +        fun mk_intr_conj (((_, _, us, _), ts, params'), _) =
    1.98 +          let
    1.99 +            fun list_ex ([], t) = t
   1.100 +              | list_ex ((a,T)::vars, t) =
   1.101 +                 (HOLogic.exists_const T) $ (Abs(a, T, list_ex(vars,t)));
   1.102 +            val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts)
   1.103 +          in
   1.104 +            list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs)
   1.105 +          end;
   1.106 +        val lhs = list_comb (c, params @ frees)
   1.107 +        val rhs =
   1.108 +          if null c_intrs then @{term False} else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs)
   1.109 +        val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.110 +        fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   1.111 +            let
   1.112 +              val (prems', last_prem) = split_last prems
   1.113 +            in
   1.114 +              EVERY1 (select_disj (length c_intrs) (i + 1))
   1.115 +              THEN EVERY (replicate (length params) (rtac @{thm exI} 1))
   1.116 +              THEN EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems')
   1.117 +              THEN rtac last_prem 1
   1.118 +            end) ctxt' 1
   1.119 +        fun prove_intr2 (((_, _, us, _), ts, params'), intr) =
   1.120 +          EVERY (replicate (length params') (etac @{thm exE} 1))
   1.121 +          THEN EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1))
   1.122 +          THEN Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   1.123 +            let
   1.124 +              val (eqs, prems') = chop (length us) prems
   1.125 +              val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs
   1.126 +            in
   1.127 +              rewrite_goal_tac rew_thms 1
   1.128 +              THEN rtac intr 1
   1.129 +              THEN (EVERY (map (fn p => rtac p 1) prems'))              
   1.130 +            end) ctxt' 1 
   1.131 +      in
   1.132 +        Skip_Proof.prove ctxt' [] [] eq (fn {...} =>
   1.133 +          rtac @{thm iffI} 1 THEN etac (#1 elim) 1
   1.134 +          THEN EVERY (map_index prove_intr1 c_intrs)
   1.135 +          THEN (if null c_intrs then etac @{thm FalseE} 1 else
   1.136 +            let val (c_intrs', last_c_intr) = split_last c_intrs in
   1.137 +              EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs')
   1.138 +              THEN prove_intr2 last_c_intr
   1.139 +            end))
   1.140 +        |> rulify
   1.141 +        |> singleton (ProofContext.export ctxt' ctxt'')
   1.142 +      end;  
   1.143 +  in
   1.144 +    map2 prove_eq cs elims
   1.145 +  end;
   1.146 +  
   1.147  (* derivation of simplified elimination rules *)
   1.148  
   1.149  local
   1.150 @@ -455,7 +517,6 @@
   1.151  
   1.152  end;
   1.153  
   1.154 -
   1.155  (* inductive_cases *)
   1.156  
   1.157  fun gen_inductive_cases prep_att prep_prop args lthy =
   1.158 @@ -483,7 +544,37 @@
   1.159          in Method.erule 0 rules end))
   1.160      "dynamic case analysis on predicates";
   1.161  
   1.162 +(* derivation of simplified equation *)
   1.163  
   1.164 +fun mk_simp_eq ctxt prop =
   1.165 +  let
   1.166 +    val (c, args) = strip_comb (HOLogic.dest_Trueprop prop)
   1.167 +    val ctxt' = Variable.auto_fixes prop ctxt
   1.168 +    val cname = fst (dest_Const c)
   1.169 +    val info = the_inductive ctxt cname
   1.170 +    val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info)))
   1.171 +    val (_, args') = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq))))
   1.172 +    val certify = cterm_of (ProofContext.theory_of ctxt)
   1.173 +  in
   1.174 +    cterm_instantiate (map (pairself certify) (args' ~~ args)) eq
   1.175 +    |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
   1.176 +      (Simplifier.full_rewrite (simpset_of ctxt))))
   1.177 +    |> singleton (Variable.export ctxt' ctxt)
   1.178 +  end
   1.179 +
   1.180 +(* inductive simps *)
   1.181 +
   1.182 +fun gen_inductive_simps prep_att prep_prop args lthy =
   1.183 +  let
   1.184 +    val thy = ProofContext.theory_of lthy;
   1.185 +    val facts = args |> map (fn ((a, atts), props) =>
   1.186 +      ((a, map (prep_att thy) atts),
   1.187 +        map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
   1.188 +  in lthy |> Local_Theory.notes facts |>> map snd end;
   1.189 +
   1.190 +val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
   1.191 +val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
   1.192 +    
   1.193  (* prove induction rule *)
   1.194  
   1.195  fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
   1.196 @@ -697,7 +788,7 @@
   1.197    end;
   1.198  
   1.199  fun declare_rules rec_binding coind no_ind cnames
   1.200 -    preds intrs intr_bindings intr_atts elims raw_induct lthy =
   1.201 +    preds intrs intr_bindings intr_atts elims eqs raw_induct lthy =
   1.202    let
   1.203      val rec_name = Binding.name_of rec_binding;
   1.204      fun rec_qualified qualified = Binding.qualify qualified rec_name;
   1.205 @@ -737,18 +828,23 @@
   1.206          ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
   1.207            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
   1.208  
   1.209 -    val (inducts, lthy3) =
   1.210 -      if no_ind orelse coind then ([], lthy2)
   1.211 +    val (eqs', lthy3) = lthy2 |> 
   1.212 +      fold_map (fn (name, eq) => Local_Theory.note
   1.213 +          ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), []), [eq])
   1.214 +          #> apfst (hd o snd))
   1.215 +        (if null eqs then [] else (cnames ~~ eqs))
   1.216 +    val (inducts, lthy4) =
   1.217 +      if no_ind orelse coind then ([], lthy3)
   1.218        else
   1.219 -        let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
   1.220 -          lthy2 |>
   1.221 +        let val inducts = cnames ~~ Project_Rule.projects lthy3 (1 upto length cnames) induct' in
   1.222 +          lthy3 |>
   1.223            Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
   1.224              inducts |> map (fn (name, th) => ([th],
   1.225                [Attrib.internal (K ind_case_names),
   1.226                 Attrib.internal (K (Rule_Cases.consumes 1)),
   1.227                 Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
   1.228          end;
   1.229 -  in (intrs', elims', induct', inducts, lthy3) end;
   1.230 +  in (intrs', elims', eqs', induct', inducts, lthy4) end;
   1.231  
   1.232  type inductive_flags =
   1.233    {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
   1.234 @@ -794,17 +890,23 @@
   1.235         else
   1.236           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
   1.237             rec_preds_defs lthy2 lthy1);
   1.238 +    val eqs =
   1.239 +      if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1
   1.240  
   1.241 -    val (intrs', elims', induct, inducts, lthy3) = declare_rules rec_name coind no_ind
   1.242 -      cnames preds intrs intr_names intr_atts elims raw_induct lthy1;
   1.243 +    val elims' = map (fn (th, ns, i) => (rulify th, ns, i)) elims
   1.244 +    val intrs' = map rulify intrs
   1.245 +
   1.246 +    val (intrs'', elims'', eqs', induct, inducts, lthy3) = declare_rules rec_name coind no_ind
   1.247 +      cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
   1.248  
   1.249      val result =
   1.250        {preds = preds,
   1.251 -       intrs = intrs',
   1.252 -       elims = elims',
   1.253 +       intrs = intrs'',
   1.254 +       elims = elims'',
   1.255         raw_induct = rulify raw_induct,
   1.256         induct = induct,
   1.257 -       inducts = inducts};
   1.258 +       inducts = inducts,
   1.259 +       eqs = eqs'};
   1.260  
   1.261      val lthy4 = lthy3
   1.262        |> Local_Theory.declaration false (fn phi =>
   1.263 @@ -993,4 +1095,9 @@
   1.264      "create simplified instances of elimination rules (improper)" Keyword.thy_script
   1.265      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
   1.266  
   1.267 +val _ =
   1.268 +  Outer_Syntax.local_theory "inductive_simps"
   1.269 +    "create simplification rules for inductive predicates" Keyword.thy_script
   1.270 +    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
   1.271 +
   1.272  end;