# HG changeset patch # User wenzelm # Date 1322400031 -3600 # Node ID 96af0578571cc960278c4d5750c7f46f27e88931 # Parent 02afa20cf397040c0a3b01d19147b9aafb1f3dae misc tuning; diff -r 02afa20cf397 -r 96af0578571c src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sun Nov 27 13:12:42 2011 +0100 +++ b/src/HOL/Tools/inductive.ML Sun Nov 27 14:20:31 2011 +0100 @@ -114,6 +114,7 @@ [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}]; + (** context data **) type inductive_result = @@ -133,7 +134,7 @@ type inductive_info = {names: string list, coind: bool} * inductive_result; -structure InductiveData = Generic_Data +structure Data = Generic_Data ( type T = inductive_info Symtab.table * thm list; val empty = (Symtab.empty, []); @@ -142,7 +143,7 @@ (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2)); ); -val get_inductives = InductiveData.get o Context.Proof; +val get_inductives = Data.get o Context.Proof; fun print_inductives ctxt = let @@ -162,15 +163,15 @@ NONE => error ("Unknown (co)inductive predicate " ^ quote name) | SOME info => info); -fun put_inductives names info = InductiveData.map - (apfst (fold (fn name => Symtab.update (name, info)) names)); +fun put_inductives names info = + Data.map (apfst (fold (fn name => Symtab.update (name, info)) names)); (** monotonicity rules **) val get_monos = #2 o get_inductives; -val map_monos = InductiveData.map o apsnd; +val map_monos = Data.map o apsnd; fun mk_mono ctxt thm = let @@ -178,13 +179,13 @@ fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD}) handle THM _ => thm RS @{thm le_boolD} in - case concl_of thm of + (case concl_of thm of Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq) | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq2mono thm | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) => dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm)) - | _ => thm + | _ => thm) end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm); val mono_add = @@ -199,7 +200,7 @@ (** equations **) -structure Equation_Data = Generic_Data +structure Equation_Data = Generic_Data (* FIXME just one data slot per module *) ( type T = thm Item_Net.T; val empty = Item_Net.init (op aconv o pairself Thm.prop_of) @@ -263,7 +264,8 @@ fun select_disj 1 1 = [] | select_disj _ 1 = [rtac disjI1] - | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1)); + | select_disj n i = rtac disjI2 :: select_disj (n - 1) (i - 1); + (** process rules **) @@ -298,17 +300,19 @@ val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems; val arule = list_all_free (params', Logic.list_implies (aprems, concl)); - fun check_ind err t = case dest_predicate cs params t of + fun check_ind err t = + (case dest_predicate cs params t of NONE => err (bad_app ^ commas (map (Syntax.string_of_term ctxt) params)) | SOME (_, _, ys, _) => if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs - then err bad_ind_occ else (); + then err bad_ind_occ else ()); fun check_prem' prem t = if member (op =) cs (head_of t) then check_ind (err_in_prem ctxt binding rule prem) t - else (case t of + else + (case t of Abs (_, _, t) => check_prem' prem t | t $ u => (check_prem' prem t; check_prem' prem u) | _ => ()); @@ -316,14 +320,16 @@ fun check_prem (prem, aprem) = if can HOLogic.dest_Trueprop aprem then check_prem' prem prem else err_in_prem ctxt binding rule prem "Non-atomic premise"; - in - (case concl of - Const (@{const_name Trueprop}, _) $ t => - if member (op =) cs (head_of t) then + + val _ = + (case concl of + Const (@{const_name Trueprop}, _) $ t => + if member (op =) cs (head_of t) then (check_ind (err_in_rule ctxt binding rule') t; List.app check_prem (prems ~~ aprems)) - else err_in_rule ctxt binding rule' bad_concl - | _ => err_in_rule ctxt binding rule' bad_concl); + else err_in_rule ctxt binding rule' bad_concl + | _ => err_in_rule ctxt binding rule' bad_concl); + in ((binding, att), arule) end; @@ -428,16 +434,19 @@ in map prove_elim cs end; + (* prove simplification equations *) -fun prove_eqs quiet_mode cs params intr_ts intrs (elims: (thm * bstring list * int) list) ctxt ctxt'' = +fun prove_eqs quiet_mode cs params intr_ts intrs + (elims: (thm * bstring list * int) list) ctxt ctxt'' = (* FIXME 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: thm * 'a * 'b) = let val Ts = arg_types_of (length params) c; @@ -447,53 +456,56 @@ 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) + | 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 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)) + 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 + 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 + 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, ...} => + 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 + 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 + 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 + 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 + EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') THEN + prove_intr2 last_c_intr end)) |> rulify |> singleton (Proof_Context.export ctxt' ctxt'') - end; + end; in map2 prove_eq cs elims end; - + + (* derivation of simplified elimination rules *) local @@ -533,6 +545,7 @@ end; + (* inductive_cases *) fun gen_inductive_cases prep_att prep_prop args lthy = @@ -560,31 +573,35 @@ in Method.erule 0 rules end)) "dynamic case analysis on predicates"; + (* derivation of simplified equation *) fun mk_simp_eq ctxt prop = let - val thy = Proof_Context.theory_of ctxt - val ctxt' = Variable.auto_fixes prop ctxt - val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of - val substs = Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop) + val thy = Proof_Context.theory_of ctxt; + val ctxt' = Variable.auto_fixes prop ctxt; + val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of; + val substs = + Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop) |> map_filter (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop) (Vartab.empty, Vartab.empty), eq) - handle Pattern.MATCH => NONE) - val (subst, eq) = case substs of + handle Pattern.MATCH => NONE); + val (subst, eq) = + (case substs of [s] => s | _ => error - ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique") - val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) - (Term.add_vars (lhs_of eq) []) - in + ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique")); + val inst = + map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) + (Term.add_vars (lhs_of eq) []); + in cterm_instantiate inst eq - |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv - (Simplifier.full_rewrite (simpset_of ctxt)))) + |> 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 = @@ -598,19 +615,20 @@ 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 - fp_def rec_preds_defs ctxt ctxt''' = + fp_def rec_preds_defs ctxt ctxt''' = (* FIXME ctxt''' ?? *) let val _ = clean_message quiet_mode " Proving the induction rule ..."; - val thy = Proof_Context.theory_of ctxt; (* predicates for induction rule *) val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt; - val preds = map2 (curry Free) pnames - (map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs); + val preds = + map2 (curry Free) pnames + (map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs); (* transform an introduction rule into a premise for induction rule *) @@ -625,12 +643,12 @@ val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs); val Q = list_abs (mk_names "x" k ~~ Ts, HOLogic.mk_binop inductive_conj_name - (list_comb (incr_boundvars k s, bs), P)) + (list_comb (incr_boundvars k s, bs), P)); in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end | NONE => (case s of - (t $ u) => (fst (subst t) $ fst (subst u), NONE) - | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE) + t $ u => (fst (subst t) $ fst (subst u), NONE) + | Abs (a, T, t) => (Abs (a, T, fst (subst t)), NONE) | _ => (s, NONE))); fun mk_prem s prems = @@ -638,9 +656,8 @@ (_, SOME (t, u)) => t :: u :: prems | (t, _) => t :: prems); - val SOME (_, i, ys, _) = dest_predicate cs params - (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)) - + val SOME (_, i, ys, _) = + dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); in list_all_free (Logic.strip_params r, Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem @@ -654,27 +671,28 @@ (* make conclusions for induction rules *) val Tss = map (binder_types o fastype_of) preds; - val (xnames, ctxt'') = - Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt'; - val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + val (xnames, ctxt'') = Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt'; + val mutual_ind_concl = + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (((xnames, Ts), c), P) => - let val frees = map Free (xnames ~~ Ts) - in HOLogic.mk_imp - (list_comb (c, params @ frees), list_comb (P, frees)) - end) (unflat Tss xnames ~~ Tss ~~ cs ~~ preds))); + let val frees = map Free (xnames ~~ Ts) + in HOLogic.mk_imp (list_comb (c, params @ frees), list_comb (P, frees)) end) + (unflat Tss xnames ~~ Tss ~~ cs ~~ preds))); (* make predicate for instantiation of abstract induction rule *) - val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj - (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp) - (make_bool_args HOLogic.mk_not I bs i) - (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds)); + val ind_pred = + fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj + (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp) + (make_bool_args HOLogic.mk_not I bs i) + (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds)); - val ind_concl = HOLogic.mk_Trueprop - (HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred)); + val ind_concl = + HOLogic.mk_Trueprop + (HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred)); - val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct})); + val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct}); val induct = Skip_Proof.prove ctxt'' [] ind_prems ind_concl (fn {prems, ...} => EVERY @@ -701,7 +719,7 @@ REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1), atac 1, rewrite_goals_tac simp_thms', - atac 1])]) + atac 1])]); in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end; @@ -717,10 +735,12 @@ val argTs = fold (combine (op =) o arg_types_of (length params)) cs []; val k = log 2 1 (length cs); val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT; - val p :: xs = map Free (Variable.variant_frees lthy intr_ts - (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs))); - val bs = map Free (Variable.variant_frees lthy (p :: xs @ intr_ts) - (map (rpair HOLogic.boolT) (mk_names "b" k))); + val p :: xs = + map Free (Variable.variant_frees lthy intr_ts + (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs))); + val bs = + map Free (Variable.variant_frees lthy (p :: xs @ intr_ts) + (map (rpair HOLogic.boolT) (mk_names "b" k))); fun subst t = (case dest_predicate cs params t of @@ -746,23 +766,24 @@ fun transform_rule r = let - val SOME (_, i, ts, (Ts, _)) = dest_predicate cs params - (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); - val ps = make_bool_args HOLogic.mk_not I bs i @ + val SOME (_, i, ts, (Ts, _)) = + dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); + val ps = + make_bool_args HOLogic.mk_not I bs i @ map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @ - map (subst o HOLogic.dest_Trueprop) - (Logic.strip_assums_hyp r) + map (subst o HOLogic.dest_Trueprop) (Logic.strip_assums_hyp r); in fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P)) (Logic.strip_params r) (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps) - end + end; (* make a disjunction of all introduction rules *) - val fp_fun = fold_rev lambda (p :: bs @ xs) - (if null intr_ts then HOLogic.false_const - else foldr1 HOLogic.mk_disj (map transform_rule intr_ts)); + val fp_fun = + fold_rev lambda (p :: bs @ xs) + (if null intr_ts then HOLogic.false_const + else foldr1 HOLogic.mk_disj (map transform_rule intr_ts)); (* add definiton of recursive predicates to theory *) @@ -779,16 +800,17 @@ fold_rev lambda params (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) ||> Local_Theory.restore_naming lthy; - val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def]) - (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params))); + val fp_def' = + Simplifier.rewrite (HOL_basic_ss addsimps [fp_def]) + (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params))); val specs = if length cs < 2 then [] else map_index (fn (i, (name_mx, c)) => let val Ts = arg_types_of (length params) c; - val xs = map Free (Variable.variant_frees lthy intr_ts - (mk_names "x" (length Ts) ~~ Ts)) + val xs = + map Free (Variable.variant_frees lthy intr_ts (mk_names "x" (length Ts) ~~ Ts)); in (name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs) (list_comb (rec_const, params @ make_bool_args' bs i @ @@ -849,7 +871,7 @@ ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); - val (eqs', lthy3) = lthy2 |> + val (eqs', lthy3) = lthy2 |> fold_map (fn (name, eq) => Local_Theory.note ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), [Attrib.internal (K add_equation)]), [eq]) @@ -913,13 +935,14 @@ 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 + if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1; - val elims' = map (fn (th, ns, i) => (rulify th, ns, i)) elims - val intrs' = map rulify intrs + 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 (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, @@ -1033,10 +1056,9 @@ (* read off parameters of inductive predicate from raw induction rule *) fun params_of induct = let - val (_ $ t $ u :: _) = - HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)); + val (_ $ t $ u :: _) = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)); val (_, ts) = strip_comb t; - val (_, us) = strip_comb u + val (_, us) = strip_comb u; in List.take (ts, length ts - length us) end; @@ -1065,13 +1087,15 @@ fun mtch (t, u) = let val params = Logic.strip_params t; - val vars = map (Var o apfst (rpair 0)) - (Name.variant_list used (map fst params) ~~ map snd params); - val ts = map (curry subst_bounds (rev vars)) - (List.drop (Logic.strip_assums_hyp t, arity)); + val vars = + map (Var o apfst (rpair 0)) + (Name.variant_list used (map fst params) ~~ map snd params); + val ts = + map (curry subst_bounds (rev vars)) + (List.drop (Logic.strip_assums_hyp t, arity)); val us = Logic.strip_imp_prems u; - val tab = fold (Pattern.first_order_match thy) (ts ~~ us) - (Vartab.empty, Vartab.empty); + val tab = + fold (Pattern.first_order_match thy) (ts ~~ us) (Vartab.empty, Vartab.empty); in map (Envir.subst_term tab) vars end