--- 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) *}
--- 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};
--- 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};
--- 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
--- 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)
--- 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
--- 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
--- 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)
--- 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)
--- 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
--- 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})
--- 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 *********************************)
--- 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)
--- 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)
--- 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,
--- 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)" *)
--- 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}
--- 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
--- 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
--- 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
--- 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
--- 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 *)
--- 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;