# HG changeset patch # User wenzelm # Date 1322431923 -3600 # Node ID 862d68ee10f3be11d794291e37d141c3919e2f7e # Parent 003a01272d280156e7f72915508f520bd7cbfb5c# Parent cf10bde35973a8c0e4e20e6052e852eff46bc043 merged diff -r 003a01272d28 -r 862d68ee10f3 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Sun Nov 27 13:32:20 2011 +0100 +++ b/src/FOL/FOL.thy Sun Nov 27 23:12:03 2011 +0100 @@ -337,12 +337,12 @@ (*intuitionistic simprules only*) val IFOL_ss = FOL_basic_ss - addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps}) + addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps} addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}] |> Simplifier.add_cong @{thm imp_cong}; (*classical simprules too*) -val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps}); +val FOL_ss = IFOL_ss addsimps @{thms cla_simps cla_ex_simps cla_all_simps}; *} setup {* Simplifier.map_simpset_global (K FOL_ss) *} diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Nov 27 23:12:03 2011 +0100 @@ -19,7 +19,7 @@ val nT = HOLogic.natT; val binarith = @{thms normalize_bin_simps}; -val comp_arith = binarith @ simp_thms +val comp_arith = binarith @ @{thms simp_thms}; val zdvd_int = @{thm zdvd_int}; val zdiff_int_split = @{thm zdiff_int_split}; diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sun Nov 27 23:12:03 2011 +0100 @@ -23,7 +23,7 @@ val binarith = @{thms normalize_bin_simps} @ @{thms pred_bin_simps} @ @{thms succ_bin_simps} @ @{thms add_bin_simps} @ @{thms minus_bin_simps} @ @{thms mult_bin_simps}; -val comp_arith = binarith @ simp_thms +val comp_arith = binarith @ @{thms simp_thms}; val zdvd_int = @{thm zdvd_int}; val zdiff_int_split = @{thm zdiff_int_split}; diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Nov 27 23:12:03 2011 +0100 @@ -163,7 +163,7 @@ qe)) [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th] val bex_conv = - Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)})) + Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms bex_simps(1-5)}) val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th) in result_th end @@ -200,8 +200,8 @@ let val ss = simpset val ss' = - merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps) - @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss) + merge_ss (HOL_basic_ss addsimps @{thms simp_thms ex_simps all_simps + not_all all_not_ex ex_disj_distrib}, ss) |> Simplifier.inherit_context ss val pcv = Simplifier.rewrite ss' val postcv = Simplifier.rewrite ss diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Decision_Procs/langford.ML Sun Nov 27 23:12:03 2011 +0100 @@ -26,7 +26,9 @@ (Thm.cprop_of th), SOME x] th1) th in fold ins u th0 end; -val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms)))); +val simp_rule = + Conv.fconv_rule + (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps @{thms ball_simps simp_thms}))); fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = case term_of ep of @@ -138,16 +140,14 @@ (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx)))) |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |> Conv.fconv_rule (Conv.arg_conv - (Simplifier.rewrite - (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) + (Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps}))) |> SOME end | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs)))) |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |> Conv.fconv_rule (Conv.arg_conv - (Simplifier.rewrite - (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) + (Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps}))) |> SOME end | _ => NONE; @@ -162,9 +162,9 @@ let val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc] val dnfex_conv = Simplifier.rewrite ss - val pcv = Simplifier.rewrite - (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps) - @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]) + val pcv = + Simplifier.rewrite + (dlo_ss addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib}) in fn p => Qelim.gen_qelim_conv pcv pcv dnfex_conv cons (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive) diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Nov 27 23:12:03 2011 +0100 @@ -37,7 +37,7 @@ @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"}, @{thm "diff_minus"}, @{thm "minus_divide_left"}] -val comp_ths = ths @ comp_arith @ simp_thms +val comp_ths = ths @ comp_arith @ @{thms simp_thms}; val zdvd_int = @{thm "zdvd_int"}; @@ -89,7 +89,7 @@ fun mir_tac ctxt q = Object_Logic.atomize_prems_tac - THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) + THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms}) THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]) THEN' SUBGOAL (fn (g, i) => let diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/HOL.thy Sun Nov 27 23:12:03 2011 +0100 @@ -2011,15 +2011,8 @@ fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]; end; -val all_conj_distrib = @{thm all_conj_distrib}; -val all_simps = @{thms all_simps}; -val atomize_not = @{thm atomize_not}; val case_split = @{thm case_split}; -val cases_simp = @{thm cases_simp}; -val choice_eq = @{thm choice_eq}; val cong = @{thm cong}; -val conj_comms = @{thms conj_comms}; -val conj_cong = @{thm conj_cong}; val de_Morgan_conj = @{thm de_Morgan_conj}; val de_Morgan_disj = @{thm de_Morgan_disj}; val disj_assoc = @{thm disj_assoc}; @@ -2045,15 +2038,11 @@ val imp_conjL = @{thm imp_conjL}; val imp_conjR = @{thm imp_conjR}; val imp_conv_disj = @{thm imp_conv_disj}; -val simp_implies_def = @{thm simp_implies_def}; -val simp_thms = @{thms simp_thms}; val split_if = @{thm split_if}; val the1_equality = @{thm the1_equality}; val theI = @{thm theI}; val theI' = @{thm theI'}; -val True_implies_equals = @{thm True_implies_equals}; -val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms @ @{thms "nnf_simps"}) - +val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps}); *} hide_const (open) eq equal diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/HOLCF/FOCUS/Buffer_adm.thy --- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy Sun Nov 27 23:12:03 2011 +0100 @@ -254,7 +254,7 @@ apply (clarsimp) apply (drule (1) fstream_lub_lemma) apply (clarsimp) -apply (tactic "simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1") +apply (simp only: ex_simps [symmetric] all_simps [symmetric]) apply (rule_tac x="Xa" in exI) apply (rule allI) apply (rotate_tac -1) diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Nov 27 23:12:03 2011 +0100 @@ -64,13 +64,13 @@ (************************** miscellaneous functions ***************************) -val simple_ss = HOL_basic_ss addsimps simp_thms +val simple_ss = HOL_basic_ss addsimps @{thms simp_thms} val beta_rules = @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair} -val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules) +val beta_ss = HOL_basic_ss addsimps (@{thms simp_thms} @ beta_rules) fun define_consts (specs : (binding * term * mixfix) list) diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Nov 27 23:12:03 2011 +0100 @@ -156,7 +156,7 @@ fun con_thm p (con, args) = let val subgoal = con_assm false p (con, args) - val rules = prems @ con_rews @ simp_thms + val rules = prems @ con_rews @ @{thms simp_thms} val simplify = asm_simp_tac (HOL_basic_ss addsimps rules) fun arg_tac (lazy, _) = rtac (if lazy then allI else case_UU_allI) 1 diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Nov 27 23:12:03 2011 +0100 @@ -36,7 +36,7 @@ struct val beta_ss = - HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}] + HOL_basic_ss addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}] fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo}) diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun Nov 27 23:12:03 2011 +0100 @@ -108,7 +108,7 @@ } val beta_ss = - HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}] + HOL_basic_ss addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}] (******************************************************************************) (******************************** theory data *********************************) diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Nov 27 23:12:03 2011 +0100 @@ -381,7 +381,7 @@ @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}; -val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); +val beta_ss = HOL_basic_ss addsimps (@{thms simp_thms} @ beta_rules); fun define_consts (specs : (binding * term * mixfix) list) diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Library/positivstellensatz.ML Sun Nov 27 23:12:03 2011 +0100 @@ -200,7 +200,7 @@ val pth_square = @{lemma "x * x >= (0::real)" by simp}; val weak_dnf_simps = - List.take (simp_thms, 34) @ + List.take (@{thms simp_thms}, 34) @ @{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and "(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+}; @@ -351,7 +351,8 @@ poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv, absconv1,absconv2,prover) = let - val pre_ss = HOL_basic_ss addsimps simp_thms@ ex_simps@ all_simps@[@{thm not_all},@{thm not_ex},ex_disj_distrib, all_conj_distrib, @{thm if_bool_eq_disj}] + val pre_ss = HOL_basic_ss addsimps + @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj} val prenex_ss = HOL_basic_ss addsimps prenex_simps val skolemize_ss = HOL_basic_ss addsimps [choice_iff] val presimp_conv = Simplifier.rewrite (Simplifier.context ctxt pre_ss) diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Sun Nov 27 23:12:03 2011 +0100 @@ -1018,7 +1018,7 @@ (fn _ => simp_tac (HOL_basic_ss addsimps (supp_def :: Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un :: - Collect_False_empty :: finite_emptyI :: simp_thms @ + Collect_False_empty :: finite_emptyI :: @{thms simp_thms} @ abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1) in (supp_thm, diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Prolog/prolog.ML Sun Nov 27 23:12:03 2011 +0100 @@ -62,7 +62,7 @@ (Simplifier.global_context @{theory} empty_ss |> Simplifier.set_mksimps (mksimps mksimps_pairs)) addsimps [ - all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) + @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *) imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *) imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *) diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Set.thy --- a/src/HOL/Set.thy Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Set.thy Sun Nov 27 23:12:03 2011 +0100 @@ -1797,7 +1797,6 @@ val bspec = @{thm bspec} val contra_subsetD = @{thm contra_subsetD} val distinct_lemma = @{thm distinct_lemma} -val eq_to_mono = @{thm eq_to_mono} val equalityCE = @{thm equalityCE} val equalityD1 = @{thm equalityD1} val equalityD2 = @{thm equalityD2} diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sun Nov 27 23:12:03 2011 +0100 @@ -38,7 +38,7 @@ (** special setup for simpset **) -val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}]) +val HOL_basic_ss' = HOL_basic_ss addsimps @{thms simp_thms Pair_eq} setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac)) setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI})) @@ -206,7 +206,7 @@ preds in simp_tac (HOL_basic_ss addsimps - (@{thms HOL.simp_thms} @ (@{thm eval_pred} :: defs))) 1 + (@{thms HOL.simp_thms eval_pred} @ defs)) 1 (* need better control here! *) end diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Tools/Qelim/qelim.ML Sun Nov 27 23:12:03 2011 +0100 @@ -55,8 +55,7 @@ local val pcv = Simplifier.rewrite - (HOL_basic_ss addsimps (@{thms simp_thms} @ @{thms ex_simps} @ @{thms all_simps} @ - [@{thm all_not_ex}, not_all, @{thm ex_disj_distrib}])); + (HOL_basic_ss addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib}); in fun standard_qelim_conv atcv ncv qcv p = gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p diff -r 003a01272d28 -r 862d68ee10f3 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/HOL/Tools/inductive.ML Sun Nov 27 23:12:03 2011 +0100 @@ -27,9 +27,9 @@ type inductive_info = {names: string list, coind: bool} * inductive_result val the_inductive: Proof.context -> string -> inductive_info val print_inductives: Proof.context -> unit + val get_monos: Proof.context -> thm list val mono_add: attribute val mono_del: attribute - val get_monos: Proof.context -> thm list val mk_cases: Proof.context -> term -> thm val inductive_forall_def: thm val rulify: thm -> thm @@ -88,7 +88,6 @@ structure Inductive: INDUCTIVE = struct - (** theory context references **) val inductive_forall_def = @{thm induct_forall_def}; @@ -99,116 +98,18 @@ val inductive_rulify = @{thms induct_rulify}; val inductive_rulify_fallback = @{thms induct_rulify_fallback}; -val notTrueE = TrueI RSN (2, notE); -val notFalseI = Seq.hd (atac 1 notI); - -val simp_thms' = map mk_meta_eq - @{lemma "(~True) = False" "(~False) = True" - "(True --> P) = P" "(False --> P) = True" - "(P & True) = P" "(True & P) = P" - by (fact simp_thms)+}; - -val simp_thms'' = map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms'; - -val simp_thms''' = map mk_meta_eq - [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}]; - - -(** context data **) - -type inductive_result = - {preds: term list, elims: thm list, raw_induct: thm, - induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}; - -fun transform_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, eqs = fact eqs} - end; - -type inductive_info = - {names: string list, coind: bool} * inductive_result; - -structure InductiveData = Generic_Data -( - type T = inductive_info Symtab.table * thm list; - val empty = (Symtab.empty, []); - val extend = I; - fun merge ((tab1, monos1), (tab2, monos2)) : T = - (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2)); -); - -val get_inductives = InductiveData.get o Context.Proof; - -fun print_inductives ctxt = - let - val (tab, monos) = get_inductives ctxt; - val space = Consts.space_of (Proof_Context.consts_of ctxt); - in - [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))), - Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)] - |> Pretty.chunks |> Pretty.writeln - end; +val simp_thms1 = + map mk_meta_eq + @{lemma "(~ True) = False" "(~ False) = True" + "(True --> P) = P" "(False --> P) = True" + "(P & True) = P" "(True & P) = P" + by (fact simp_thms)+}; - -(* get and put data *) - -fun the_inductive ctxt name = - (case Symtab.lookup (#1 (get_inductives ctxt)) name of - 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)); - - - -(** monotonicity rules **) - -val get_monos = #2 o get_inductives; -val map_monos = InductiveData.map o apsnd; +val simp_thms2 = + map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms1; -fun mk_mono ctxt thm = - let - fun eq2mono thm' = thm' RS (thm' RS eq_to_mono); - 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 - 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 - end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm); - -val mono_add = - Thm.declaration_attribute (fn thm => fn context => - map_monos (Thm.add_thm (mk_mono (Context.proof_of context) thm)) context); - -val mono_del = - Thm.declaration_attribute (fn thm => fn context => - map_monos (Thm.del_thm (mk_mono (Context.proof_of context) thm)) context); - - - -(** equations **) - -structure Equation_Data = Generic_Data -( - type T = thm Item_Net.T; - val empty = Item_Net.init (op aconv o pairself Thm.prop_of) - (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of); - val extend = I; - val merge = Item_Net.merge; -); - -val add_equation = Thm.declaration_attribute (Equation_Data.map o Item_Net.update) +val simp_thms3 = + map mk_meta_eq [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}]; @@ -220,7 +121,7 @@ fun coind_prefix true = "co" | coind_prefix false = ""; -fun log (b:int) m n = if m >= n then 0 else 1 + log b (b * m) n; +fun log (b: int) m n = if m >= n then 0 else 1 + log b (b * m) n; fun make_bool_args f g [] i = [] | make_bool_args f g (x :: xs) i = @@ -263,7 +164,119 @@ 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); + + + +(** context data **) + +type inductive_result = + {preds: term list, elims: thm list, raw_induct: thm, + induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}; + +fun transform_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, eqs = fact eqs} + end; + +type inductive_info = {names: string list, coind: bool} * inductive_result; + +val empty_equations = + Item_Net.init Thm.eq_thm_prop + (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of); + +datatype data = Data of + {infos: inductive_info Symtab.table, + monos: thm list, + equations: thm Item_Net.T}; + +fun make_data (infos, monos, equations) = + Data {infos = infos, monos = monos, equations = equations}; + +structure Data = Generic_Data +( + type T = data; + val empty = make_data (Symtab.empty, [], empty_equations); + val extend = I; + fun merge (Data {infos = infos1, monos = monos1, equations = equations1}, + Data {infos = infos2, monos = monos2, equations = equations2}) = + make_data (Symtab.merge (K true) (infos1, infos2), + Thm.merge_thms (monos1, monos2), + Item_Net.merge (equations1, equations2)); +); + +fun map_data f = + Data.map (fn Data {infos, monos, equations} => make_data (f (infos, monos, equations))); + +fun rep_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data rep => rep); + +fun print_inductives ctxt = + let + val {infos, monos, ...} = rep_data ctxt; + val space = Consts.space_of (Proof_Context.consts_of ctxt); + in + [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, infos))), + Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)] + |> Pretty.chunks |> Pretty.writeln + end; + + +(* inductive info *) + +fun the_inductive ctxt name = + (case Symtab.lookup (#infos (rep_data ctxt)) name of + NONE => error ("Unknown (co)inductive predicate " ^ quote name) + | SOME info => info); + +fun put_inductives names info = + map_data (fn (infos, monos, equations) => + (fold (fn name => Symtab.update (name, info)) names infos, monos, equations)); + + +(* monotonicity rules *) + +val get_monos = #monos o rep_data; + +fun mk_mono ctxt thm = + let + fun eq_to_mono thm' = thm' RS (thm' RS @{thm eq_to_mono}); + 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 + Const ("==", _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq) + | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm + | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) => + dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL + (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm)) + | _ => thm) + end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm); + +val mono_add = + Thm.declaration_attribute (fn thm => fn context => + map_data (fn (infos, monos, equations) => + (infos, Thm.add_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context); + +val mono_del = + Thm.declaration_attribute (fn thm => fn context => + map_data (fn (infos, monos, equations) => + (infos, Thm.del_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context); + + +(* equations *) + +val get_equations = #equations o rep_data; + +val equation_add_permissive = + Thm.declaration_attribute (fn thm => + map_data (fn (infos, monos, equations) => + (infos, monos, perhaps (try (Item_Net.update thm)) equations))); + (** process rules **) @@ -298,17 +311,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 +331,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; @@ -366,7 +383,7 @@ (mono RS (fp_def RS (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold}))); - val rules = [refl, TrueI, notFalseI, exI, conjI]; + val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI]; val intrs = map_index (fn (i, intr) => Skip_Proof.prove ctxt [] [] intr (fn _ => EVERY @@ -397,7 +414,7 @@ val intrs = map dest_intr intr_ts ~~ intr_names; val rules1 = [disjE, exE, FalseE]; - val rules2 = [conjE, FalseE, notTrueE]; + val rules2 = [conjE, FalseE, @{lemma "~ True ==> R" by (rule notE [OF _ TrueI])}]; fun prove_elim c = let @@ -428,16 +445,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 +467,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 +556,7 @@ end; + (* inductive_cases *) fun gen_inductive_cases prep_att prep_prop args lthy = @@ -560,31 +584,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 (get_equations 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 - cterm_instantiate inst eq - |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv - (Simplifier.full_rewrite (simpset_of ctxt)))) + ("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 + Drule.cterm_instantiate inst 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 = @@ -598,19 +626,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 +654,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 +667,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,34 +682,35 @@ (* 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 [rewrite_goals_tac [inductive_conj_def], DETERM (rtac raw_fp_induct 1), REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1), - rewrite_goals_tac simp_thms'', + rewrite_goals_tac simp_thms2, (*This disjE separates out the introduction rules*) REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])), (*Now break down the individual cases. No disjE here in case @@ -690,7 +719,7 @@ REPEAT (FIRSTGOAL (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))), EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule - (inductive_conj_def :: rec_preds_defs @ simp_thms'') prem, + (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem, conjI, refl] 1)) prems)]); val lemma = Skip_Proof.prove ctxt'' [] [] @@ -700,8 +729,8 @@ [REPEAT (resolve_tac [conjI, impI] 1), REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1), atac 1, - rewrite_goals_tac simp_thms', - atac 1])]) + rewrite_goals_tac simp_thms1, + atac 1])]); in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end; @@ -717,10 +746,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 +777,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 +811,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,10 +882,10 @@ ((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]) + [Attrib.internal (K equation_add_permissive)]), [eq]) #> apfst (hd o snd)) (if null eqs then [] else (cnames ~~ eqs)) val (inducts, lthy4) = @@ -907,19 +940,20 @@ singleton (Proof_Context.export lthy2 lthy1) (rotate_prems ~1 (Object_Logic.rulify (fold_rule rec_preds_defs - (rewrite_rule simp_thms''' + (rewrite_rule simp_thms3 (mono RS (fp_def RS @{thm def_coinduct})))))) 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 + 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 +1067,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 +1098,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 diff -r 003a01272d28 -r 862d68ee10f3 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/Pure/Isar/proof_context.ML Sun Nov 27 23:12:03 2011 +0100 @@ -188,8 +188,8 @@ (** Isar proof context information **) -datatype ctxt = - Ctxt of +datatype data = + Data of {mode: mode, (*inner syntax mode*) naming: Name_Space.naming, (*local naming conventions*) syntax: Local_Syntax.T, (*local syntax*) @@ -198,83 +198,83 @@ facts: Facts.T, (*local facts*) cases: (string * (Rule_Cases.T * bool)) list}; (*named case contexts*) -fun make_ctxt (mode, naming, syntax, tsig, consts, facts, cases) = - Ctxt {mode = mode, naming = naming, syntax = syntax, +fun make_data (mode, naming, syntax, tsig, consts, facts, cases) = + Data {mode = mode, naming = naming, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases}; val local_naming = Name_Space.default_naming |> Name_Space.add_path "local"; structure Data = Proof_Data ( - type T = ctxt; + type T = data; fun init thy = - make_ctxt (mode_default, local_naming, Local_Syntax.init thy, + make_data (mode_default, local_naming, Local_Syntax.init thy, (Sign.tsig_of thy, Sign.tsig_of thy), (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []); ); -fun rep_context ctxt = Data.get ctxt |> (fn Ctxt args => args); +fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); -fun map_context f = - Data.map (fn Ctxt {mode, naming, syntax, tsig, consts, facts, cases} => - make_ctxt (f (mode, naming, syntax, tsig, consts, facts, cases))); +fun map_data f = + Data.map (fn Data {mode, naming, syntax, tsig, consts, facts, cases} => + make_data (f (mode, naming, syntax, tsig, consts, facts, cases))); -fun set_mode mode = map_context (fn (_, naming, syntax, tsig, consts, facts, cases) => +fun set_mode mode = map_data (fn (_, naming, syntax, tsig, consts, facts, cases) => (mode, naming, syntax, tsig, consts, facts, cases)); fun map_mode f = - map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) => + map_data (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) => (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsig, consts, facts, cases)); fun map_naming f = - map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => (mode, f naming, syntax, tsig, consts, facts, cases)); fun map_syntax f = - map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => (mode, naming, f syntax, tsig, consts, facts, cases)); fun map_tsig f = - map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => (mode, naming, syntax, f tsig, consts, facts, cases)); fun map_consts f = - map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => (mode, naming, syntax, tsig, f consts, facts, cases)); fun map_facts f = - map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => (mode, naming, syntax, tsig, consts, f facts, cases)); fun map_cases f = - map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => (mode, naming, syntax, tsig, consts, facts, f cases)); -val get_mode = #mode o rep_context; +val get_mode = #mode o rep_data; val restore_mode = set_mode o get_mode; val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev); fun set_stmt stmt = map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev)); -val naming_of = #naming o rep_context; +val naming_of = #naming o rep_data; val restore_naming = map_naming o K o naming_of val full_name = Name_Space.full_name o naming_of; -val syntax_of = #syntax o rep_context; +val syntax_of = #syntax o rep_data; val syn_of = Local_Syntax.syn_of o syntax_of; val set_syntax_mode = map_syntax o Local_Syntax.set_mode; val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of; -val tsig_of = #1 o #tsig o rep_context; +val tsig_of = #1 o #tsig o rep_data; val set_defsort = map_tsig o apfst o Type.set_defsort; fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt; -val consts_of = #1 o #consts o rep_context; +val consts_of = #1 o #consts o rep_data; val the_const_constraint = Consts.the_constraint o consts_of; -val facts_of = #facts o rep_context; -val cases_of = #cases o rep_context; +val facts_of = #facts o rep_data; +val cases_of = #cases o rep_data; (* name spaces *) @@ -1134,7 +1134,7 @@ fun pretty_abbrevs show_globals ctxt = let val ((space, consts), (_, globals)) = - pairself (#constants o Consts.dest) (#consts (rep_context ctxt)); + pairself (#constants o Consts.dest) (#consts (rep_data ctxt)); fun add_abbr (_, (_, NONE)) = I | add_abbr (c, (T, SOME t)) = if not show_globals andalso Symtab.defined globals c then I diff -r 003a01272d28 -r 862d68ee10f3 src/Pure/assumption.ML --- a/src/Pure/assumption.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/Pure/assumption.ML Sun Nov 27 23:12:03 2011 +0100 @@ -67,7 +67,7 @@ ); fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems))); -fun rep_data ctxt = Data.get ctxt |> (fn Data args => args); +fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); (* all assumptions *) diff -r 003a01272d28 -r 862d68ee10f3 src/Pure/variable.ML --- a/src/Pure/variable.ML Sun Nov 27 13:32:20 2011 +0100 +++ b/src/Pure/variable.ML Sun Nov 27 23:12:03 2011 +0100 @@ -144,7 +144,7 @@ map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, f constraints)); -fun rep_data ctxt = Data.get ctxt |> (fn Data args => args); +fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); val is_body = #is_body o rep_data;