# HG changeset patch # User bulwahn # Date 1278483921 -7200 # Node ID 489ac1ecb9f10d19029d1a4f5fdc8f1bb9dc8aa6 # Parent bf6c1216db43bc086af7f23eddd312c753297a9f added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation diff -r bf6c1216db43 -r 489ac1ecb9f1 etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Jul 06 08:08:35 2010 -0700 +++ b/etc/isar-keywords.el Wed Jul 07 08:25:21 2010 +0200 @@ -120,6 +120,7 @@ "inductive" "inductive_cases" "inductive_set" + "inductive_simps" "init_toplevel" "instance" "instantiation" @@ -550,7 +551,8 @@ "use")) (defconst isar-keywords-theory-script - '("inductive_cases")) + '("inductive_cases" + "inductive_simps")) (defconst isar-keywords-theory-goal '("ax_specification" diff -r bf6c1216db43 -r 489ac1ecb9f1 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Tue Jul 06 08:08:35 2010 -0700 +++ b/src/HOL/Tools/inductive.ML Wed Jul 07 08:25:21 2010 +0200 @@ -22,7 +22,7 @@ sig type inductive_result = {preds: term list, elims: thm list, raw_induct: thm, - induct: thm, inducts: thm list, intrs: thm list} + induct: thm, inducts: thm list, intrs: thm list, eqs: thm list} val morph_result: morphism -> inductive_result -> inductive_result type inductive_info = {names: string list, coind: bool} * inductive_result val the_inductive: Proof.context -> string -> inductive_info @@ -73,7 +73,7 @@ local_theory -> inductive_result * local_theory val declare_rules: binding -> bool -> bool -> string list -> term list -> thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list -> - thm -> local_theory -> thm list * thm list * thm * thm list * local_theory + thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory val add_ind_def: add_ind_def val gen_add_inductive_i: add_ind_def -> inductive_flags -> ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> @@ -120,16 +120,16 @@ type inductive_result = {preds: term list, elims: thm list, raw_induct: thm, - induct: thm, inducts: thm list, intrs: thm list}; + induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}; -fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs} = +fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} = let val term = Morphism.term phi; val thm = Morphism.thm phi; val fact = Morphism.fact phi; in {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct, - induct = thm induct, inducts = fact inducts, intrs = fact intrs} + induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs} end; type inductive_info = @@ -244,6 +244,9 @@ | mk_names a 1 = [a] | mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n); +fun select_disj 1 1 = [] + | select_disj _ 1 = [rtac disjI1] + | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1)); (** process rules **) @@ -347,10 +350,6 @@ (mono RS (fp_def RS (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold}))); - fun select_disj 1 1 = [] - | select_disj _ 1 = [rtac disjI1] - | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1)); - val rules = [refl, TrueI, notFalseI, exI, conjI]; val intrs = map_index (fn (i, intr) => @@ -361,7 +360,6 @@ (*Not ares_tac, since refl must be tried before any equality assumptions; backtracking may occur if the premises have extra variables!*) DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]) - |> rulify |> singleton (ProofContext.export ctxt ctxt')) intr_ts in (intrs, unfold) end; @@ -408,14 +406,78 @@ REPEAT (FIRSTGOAL (eresolve_tac rules2)), EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))]) - |> rulify |> singleton (ProofContext.export ctxt'' ctxt'''), map #2 c_intrs, length Ts) end in map prove_elim cs end; +(* prove simplification equations *) +fun prove_eqs quiet_mode cs params intr_ts intrs elims ctxt ctxt'' = + let + val _ = clean_message quiet_mode " Proving the simplification rules ..."; + + fun dest_intr r = + (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))), + Logic.strip_assums_hyp r, Logic.strip_params r); + val intr_ts' = map dest_intr intr_ts; + fun prove_eq c elim = + let + val Ts = arg_types_of (length params) c; + val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt; + val frees = map Free (anames ~~ Ts); + val c_intrs = filter (equal c o #1 o #1 o #1) (intr_ts' ~~ intrs); + fun mk_intr_conj (((_, _, us, _), ts, params'), _) = + let + fun list_ex ([], t) = t + | list_ex ((a,T)::vars, t) = + (HOLogic.exists_const T) $ (Abs(a, T, list_ex(vars,t))); + val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts) + in + list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs) + end; + val lhs = list_comb (c, params @ frees) + val rhs = + if null c_intrs then @{term False} else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs) + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) + fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} => + let + val (prems', last_prem) = split_last prems + in + EVERY1 (select_disj (length c_intrs) (i + 1)) + THEN EVERY (replicate (length params) (rtac @{thm exI} 1)) + THEN EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') + THEN rtac last_prem 1 + end) ctxt' 1 + fun prove_intr2 (((_, _, us, _), ts, params'), intr) = + EVERY (replicate (length params') (etac @{thm exE} 1)) + THEN EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) + THEN Subgoal.FOCUS_PREMS (fn {params, prems, ...} => + let + val (eqs, prems') = chop (length us) prems + val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs + in + rewrite_goal_tac rew_thms 1 + THEN rtac intr 1 + THEN (EVERY (map (fn p => rtac p 1) prems')) + end) ctxt' 1 + in + Skip_Proof.prove ctxt' [] [] eq (fn {...} => + rtac @{thm iffI} 1 THEN etac (#1 elim) 1 + THEN EVERY (map_index prove_intr1 c_intrs) + THEN (if null c_intrs then etac @{thm FalseE} 1 else + let val (c_intrs', last_c_intr) = split_last c_intrs in + EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') + THEN prove_intr2 last_c_intr + end)) + |> rulify + |> singleton (ProofContext.export ctxt' ctxt'') + end; + in + map2 prove_eq cs elims + end; + (* derivation of simplified elimination rules *) local @@ -455,7 +517,6 @@ end; - (* inductive_cases *) fun gen_inductive_cases prep_att prep_prop args lthy = @@ -483,7 +544,37 @@ in Method.erule 0 rules end)) "dynamic case analysis on predicates"; +(* derivation of simplified equation *) +fun mk_simp_eq ctxt prop = + let + val (c, args) = strip_comb (HOLogic.dest_Trueprop prop) + val ctxt' = Variable.auto_fixes prop ctxt + val cname = fst (dest_Const c) + val info = the_inductive ctxt cname + val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info))) + val (_, args') = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq)))) + val certify = cterm_of (ProofContext.theory_of ctxt) + in + cterm_instantiate (map (pairself certify) (args' ~~ args)) eq + |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv + (Simplifier.full_rewrite (simpset_of ctxt)))) + |> singleton (Variable.export ctxt' ctxt) + end + +(* inductive simps *) + +fun gen_inductive_simps prep_att prep_prop args lthy = + let + val thy = ProofContext.theory_of lthy; + val facts = args |> map (fn ((a, atts), props) => + ((a, map (prep_att thy) atts), + map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props)); + in lthy |> Local_Theory.notes facts |>> map snd end; + +val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop; +val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop; + (* prove induction rule *) fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono @@ -697,7 +788,7 @@ end; fun declare_rules rec_binding coind no_ind cnames - preds intrs intr_bindings intr_atts elims raw_induct lthy = + preds intrs intr_bindings intr_atts elims eqs raw_induct lthy = let val rec_name = Binding.name_of rec_binding; fun rec_qualified qualified = Binding.qualify qualified rec_name; @@ -737,18 +828,23 @@ ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); - val (inducts, lthy3) = - if no_ind orelse coind then ([], lthy2) + val (eqs', lthy3) = lthy2 |> + fold_map (fn (name, eq) => Local_Theory.note + ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), []), [eq]) + #> apfst (hd o snd)) + (if null eqs then [] else (cnames ~~ eqs)) + val (inducts, lthy4) = + if no_ind orelse coind then ([], lthy3) else - let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in - lthy2 |> + let val inducts = cnames ~~ Project_Rule.projects lthy3 (1 upto length cnames) induct' in + lthy3 |> Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []), inducts |> map (fn (name, th) => ([th], [Attrib.internal (K ind_case_names), Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd end; - in (intrs', elims', induct', inducts, lthy3) end; + in (intrs', elims', eqs', induct', inducts, lthy4) end; type inductive_flags = {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, @@ -794,17 +890,23 @@ else prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def rec_preds_defs lthy2 lthy1); + val eqs = + if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1 - val (intrs', elims', induct, inducts, lthy3) = declare_rules rec_name coind no_ind - cnames preds intrs intr_names intr_atts elims raw_induct lthy1; + val elims' = map (fn (th, ns, i) => (rulify th, ns, i)) elims + val intrs' = map rulify intrs + + val (intrs'', elims'', eqs', induct, inducts, lthy3) = declare_rules rec_name coind no_ind + cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1; val result = {preds = preds, - intrs = intrs', - elims = elims', + intrs = intrs'', + elims = elims'', raw_induct = rulify raw_induct, induct = induct, - inducts = inducts}; + inducts = inducts, + eqs = eqs'}; val lthy4 = lthy3 |> Local_Theory.declaration false (fn phi => @@ -993,4 +1095,9 @@ "create simplified instances of elimination rules (improper)" Keyword.thy_script (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases)); +val _ = + Outer_Syntax.local_theory "inductive_simps" + "create simplification rules for inductive predicates" Keyword.thy_script + (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps)); + end; diff -r bf6c1216db43 -r 489ac1ecb9f1 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Tue Jul 06 08:08:35 2010 -0700 +++ b/src/HOL/Tools/inductive_set.ML Wed Jul 07 08:25:21 2010 +0200 @@ -520,16 +520,17 @@ val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn; (* FIXME *) val (intr_names, intr_atts) = split_list (map fst intros); val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct; - val (intrs', elims', induct, inducts, lthy4) = + val eqs = [] (* TODO: define equations *) + val (intrs', elims', eqs', induct, inducts, lthy4) = Inductive.declare_rules rec_name coind no_ind cnames (map fst defs) (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts (map (fn th => (to_set [] (Context.Proof lthy3) th, map fst (fst (Rule_Cases.get th)), Rule_Cases.get_constraints th)) elims) - raw_induct' lthy3; + eqs raw_induct' lthy3; in ({intrs = intrs', elims = elims', induct = induct, inducts = inducts, - raw_induct = raw_induct', preds = map fst defs}, + raw_induct = raw_induct', preds = map fst defs, eqs = eqs'}, lthy4) end;