--- a/src/HOL/Tools/inductive_package.ML Sat Dec 23 22:51:01 2000 +0100
+++ b/src/HOL/Tools/inductive_package.ML Sat Dec 23 22:51:34 2000 +0100
@@ -1,7 +1,8 @@
(* Title: HOL/Tools/inductive_package.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Stefan Berghofer, TU Muenchen
+ Author: Stefan Berghofer, TU Muenchen
+ Author: Markus Wenzel, TU Muenchen
Copyright 1994 University of Cambridge
1998 TU Muenchen
@@ -39,6 +40,10 @@
val mono_add_global: theory attribute
val mono_del_global: theory attribute
val get_monos: theory -> thm list
+ val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
+ -> theory -> theory
+ val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
+ -> theory -> theory
val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
theory attribute list -> ((bstring * term) * theory attribute list) list ->
thm list -> thm list -> theory -> theory *
@@ -49,10 +54,6 @@
(xstring * Args.src list) list -> theory -> theory *
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
- val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
- -> theory -> theory
- val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
- -> theory -> theory
val setup: (theory -> theory) list
end;
@@ -62,7 +63,13 @@
(** theory context references **)
-val mk_inductive_conj = HOLogic.mk_binop "Inductive.conj";
+val mono_name = "Ord.mono";
+val gfp_name = "Gfp.gfp";
+val lfp_name = "Lfp.lfp";
+val vimage_name = "Inverse_Image.vimage";
+val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
+
+val inductive_conj_name = "Inductive.conj";
val inductive_conj_def = thm "conj_def";
val inductive_conj = thms "inductive_conj";
val inductive_atomize = thms "inductive_atomize";
@@ -71,7 +78,7 @@
-(*** theory data ***)
+(** theory data **)
(* data kind 'HOL/inductive' *)
@@ -150,20 +157,18 @@
-(** utilities **)
-
-(* messages *)
+(** misc utilities **)
val quiet_mode = ref false;
-fun message s = if !quiet_mode then () else writeln s;
+fun message s = if ! quiet_mode then () else writeln s;
+fun clean_message s = if ! quick_and_dirty then () else message s;
fun coind_prefix true = "co"
| coind_prefix false = "";
-(* the following code ensures that each recursive set *)
-(* always has the same type in all introduction rules *)
-
+(*the following code ensures that each recursive set always has the
+ same type in all introduction rules*)
fun unify_consts sign cs intr_ts =
(let
val {tsig, ...} = Sign.rep_sg sign;
@@ -192,15 +197,7 @@
(warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
-(* misc *)
-
-val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
-
-val vimage_name = Sign.intern_const (Theory.sign_of Inverse_Image.thy) "vimage";
-val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
-
-(* make injections needed in mutually recursive definitions *)
-
+(*make injections used in mutually recursive definitions*)
fun mk_inj cs sumT c x =
let
fun mk_inj' T n i =
@@ -216,8 +213,7 @@
in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
end;
-(* make "vimage" terms for selecting out components of mutually rec.def. *)
-
+(*make "vimage" terms for selecting out components of mutually rec.def*)
fun mk_vimage cs sumT t c = if length cs < 2 then t else
let
val cT = HOLogic.dest_setT (fastype_of c);
@@ -274,20 +270,13 @@
full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
full_simplify inductive_conj;
-fun rulified x = Drule.rule_attribute (K rulify) x;
-
end;
-fun try' f msg sign t = (case (try f t) of
- Some x => x
- | None => error (msg ^ Sign.string_of_term sign t));
-
+(** properties of (co)inductive sets **)
-(*** properties of (co)inductive sets ***)
-
-(** elimination rules **)
+(* elimination rules *)
fun mk_elims cs cTs params intr_ts intr_names =
let
@@ -319,8 +308,7 @@
end;
-
-(** premises and conclusions of induction rules **)
+(* premises and conclusions of induction rules *)
fun mk_indrule cs cTs params intr_ts =
let
@@ -343,7 +331,7 @@
fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
(case pred_of u of
None => (m $ fst (subst t) $ fst (subst u), None)
- | Some P => (mk_inductive_conj (s, P $ t), Some (s, P $ t)))
+ | Some P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), Some (s, P $ t)))
| subst s =
(case pred_of s of
Some P => (HOLogic.mk_binop "op Int"
@@ -388,8 +376,7 @@
end;
-
-(** prepare cases and induct rules **)
+(* prepare cases and induct rules *)
(*
transform mutual rule:
@@ -424,27 +411,23 @@
-(*** proofs for (co)inductive sets ***)
+(** proofs for (co)inductive sets **)
-(** prove monotonicity **)
+(* prove monotonicity -- NOT subject to quick_and_dirty! *)
fun prove_mono setT fp_fun monos thy =
- let
- val _ = message " Proving monotonicity ...";
-
- val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
+ (message " Proving monotonicity ...";
+ Goals.prove_goalw_cterm [] (*NO SkipProof.prove_goalw_cterm here!*)
+ (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
(Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
- (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
-
- in mono end;
+ (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]));
-
-(** prove introduction rules **)
+(* prove introduction rules *)
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
let
- val _ = message " Proving the introduction rules ...";
+ val _ = clean_message " Proving the introduction rules ...";
val unfold = standard (mono RS (fp_def RS
(if coind then def_gfp_unfold else def_lfp_unfold)));
@@ -453,8 +436,8 @@
| select_disj _ 1 = [rtac disjI1]
| select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
- val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
- (cterm_of (Theory.sign_of thy) intr) (fn prems =>
+ val intrs = map (fn (i, intr) => SkipProof.prove_goalw_cterm thy rec_sets_defs
+ (Thm.cterm_of (Theory.sign_of thy) intr) (fn prems =>
[(*insert prems and underlying sets*)
cut_facts_tac prems 1,
stac unfold 1,
@@ -463,7 +446,7 @@
EVERY1 (select_disj (length intr_ts) i),
(*Not ares_tac, since refl must be tried before any equality assumptions;
backtracking may occur if the premises have extra variables!*)
- DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
+ DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
(*Now solve the equations like Inl 0 = Inl ?b2*)
rewrite_goals_tac con_defs,
REPEAT (rtac refl 1)])
@@ -472,41 +455,37 @@
in (intrs, unfold) end;
-
-(** prove elimination rules **)
+(* prove elimination rules *)
fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
let
- val _ = message " Proving the elimination rules ...";
+ val _ = clean_message " Proving the elimination rules ...";
val rules1 = [CollectE, disjE, make_elim vimageD, exE];
- val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
- map make_elim [Inl_inject, Inr_inject];
+ val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
in
- map (fn (t, cases) => prove_goalw_cterm rec_sets_defs
- (cterm_of (Theory.sign_of thy) t) (fn prems =>
+ map (fn (t, cases) => SkipProof.prove_goalw_cterm thy rec_sets_defs
+ (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
[cut_facts_tac [hd prems] 1,
dtac (unfold RS subst) 1,
REPEAT (FIRSTGOAL (eresolve_tac rules1)),
REPEAT (FIRSTGOAL (eresolve_tac rules2)),
- EVERY (map (fn prem =>
- DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
+ EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
|> rulify
|> RuleCases.name cases)
(mk_elims cs cTs params intr_ts intr_names)
end;
-(** derivation of simplified elimination rules **)
+(* derivation of simplified elimination rules *)
(*Applies freeness of the given constructors, which *must* be unfolded by
the given defs. Cannot simply use the local con_defs because con_defs=[]
- for inference systems.
- *)
+ for inference systems. (??) *)
(*cprop should have the form t:Si where Si is an inductive set*)
-val mk_cases_err = "mk_cases: proposition not of form 't : S_i'";
+val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
fun mk_cases_i elims ss cprop =
let
@@ -561,13 +540,12 @@
val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
-
-(** prove induction rule **)
+(* prove induction rule *)
fun prove_indrule cs cTs sumT rec_const params intr_ts mono
fp_def rec_sets_defs thy =
let
- val _ = message " Proving the induction rule ...";
+ val _ = clean_message " Proving the induction rule ...";
val sign = Theory.sign_of thy;
@@ -597,15 +575,14 @@
(* simplification rules for vimage and Collect *)
val vimage_simps = if length cs < 2 then [] else
- map (fn c => prove_goalw_cterm [] (cterm_of sign
+ map (fn c => SkipProof.prove_goalw_cterm thy [] (Thm.cterm_of sign
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
nth_elem (find_index_eq c cs, preds)))))
- (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
- rtac refl 1])) cs;
+ (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
- val induct = prove_goalw_cterm [inductive_conj_def] (cterm_of sign
+ val induct = SkipProof.prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
(Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
[rtac (impI RS allI) 1,
DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
@@ -620,7 +597,7 @@
EVERY (map (fn prem =>
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
- val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
+ val lemma = SkipProof.prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
[cut_facts_tac prems 1,
REPEAT (EVERY
@@ -633,9 +610,7 @@
-(*** specification of (co)inductive sets ****)
-
-(** definitional introduction of (co)inductive sets **)
+(** specification of (co)inductive sets **)
fun cond_declare_consts declare_consts cs paramTs cnames =
if declare_consts then
@@ -648,8 +623,7 @@
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
val setT = HOLogic.mk_setT sumT;
- val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
- else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
+ val fp_name = if coind then gfp_name else lfp_name;
val used = foldr add_term_names (intr_ts, []);
val [sname, xname] = variantlist (["S", "x"], used);
@@ -688,7 +662,7 @@
(Const (full_rec_name, paramTs ---> setT), params);
val fp_def_term = Logic.mk_equals (rec_const,
- Const (fp_name, (setT --> setT) --> setT) $ fp_fun)
+ Const (fp_name, (setT --> setT) --> setT) $ fp_fun);
val def_terms = fp_def_term :: (if length cs < 2 then [] else
map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
@@ -703,15 +677,14 @@
val mono = prove_mono setT fp_fun monos thy'
- in
- (thy', mono, fp_def, rec_sets_defs, rec_const, sumT)
- end;
+ in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
let
- val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
- commas_quote cnames) else ();
+ val _ =
+ if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
+ commas_quote cnames) else ();
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
@@ -735,17 +708,14 @@
val (thy2, intrs') =
thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
- val (thy3, [intrs'']) =
- thy2
- |> PureThy.add_thmss [(("intros", intrs'), atts)]
- |>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])])
- |>> (if no_ind then I else #1 o PureThy.add_thms
- [((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])])
+ val (thy3, ([intrs'', elims'], [induct'])) =
+ thy2
+ |> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])]
+ |>>> PureThy.add_thms
+ [((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])]
|>> Theory.parent_path;
- val elims' = if no_elim then elims else PureThy.get_thms thy3 "elims"; (* FIXME improve *)
- val induct' = if no_ind then induct else PureThy.get_thm thy3 (coind_prefix coind ^ "induct"); (* FIXME improve *)
in (thy3,
- {defs = fp_def::rec_sets_defs,
+ {defs = fp_def :: rec_sets_defs,
mono = mono,
unfold = unfold,
intrs = intrs'',
@@ -756,59 +726,12 @@
end;
-
-(** axiomatic introduction of (co)inductive sets **)
-
-fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
- atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
- let
- val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames);
-
- val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
- val (thy1, _, fp_def, rec_sets_defs, _, _) =
- mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
- params paramTs cTs cnames;
- val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names);
- val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
- val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
-
- val (thy2, [intrs, raw_elims]) =
- thy1
- |> PureThy.add_axiomss_i
- [(("raw_intros", intr_ts), [rulified]),
- (("raw_elims", elim_ts), [rulified])]
- |>> (if coind then I else
- #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
+(* external interfaces *)
- val elims = map2 (fn (th, cases) => RuleCases.name cases th) (raw_elims, elim_cases);
- val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy2 "raw_induct";
- val induct = if coind orelse length cs > 1 then raw_induct
- else standard (raw_induct RSN (2, rev_mp));
-
- val (thy3, intrs') =
- thy2 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
- val (thy4, [intrs'', elims']) =
- thy3
- |> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])]
- |>> (if coind then I
- else #1 o PureThy.add_thms [(("induct", rulify induct),
- [RuleCases.case_names induct_cases])])
- |>> Theory.parent_path;
- val induct' = if coind then raw_induct else PureThy.get_thm thy4 "induct";
- in (thy4,
- {defs = fp_def :: rec_sets_defs,
- mono = Drule.asm_rl,
- unfold = Drule.asm_rl,
- intrs = intrs'',
- elims = elims',
- mk_cases = mk_cases elims',
- raw_induct = rulify raw_induct,
- induct = induct'})
- end;
-
-
-
-(** introduction of (co)inductive sets **)
+fun try_term f msg sign t =
+ (case Library.try f t of
+ Some x => x
+ | None => error (msg ^ Sign.string_of_term sign t));
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
atts pre_intros monos con_defs thy =
@@ -818,13 +741,13 @@
(*parameters should agree for all mutually recursive components*)
val (_, params) = strip_comb (hd cs);
- val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
+ val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
\ component is not a free variable: " sign) params;
- val cTs = map (try' (HOLogic.dest_setT o fastype_of)
+ val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
"Recursive component not of type set: " sign) cs;
- val full_cnames = map (try' (fst o dest_Const o head_of)
+ val full_cnames = map (try_term (fst o dest_Const o head_of)
"Recursive set not previously declared as constant: " sign) cs;
val cnames = map Sign.base_name full_cnames;
@@ -834,18 +757,13 @@
val induct_cases = map (#1 o #1) intros;
val (thy1, result as {elims, induct, ...}) =
- (if ! quick_and_dirty andalso not coind (* FIXME *) then add_ind_axm else add_ind_def)
- verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
+ add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
con_defs thy params paramTs cTs cnames induct_cases;
val thy2 = thy1
|> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
|> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases;
in (thy2, result) end;
-
-
-(** external interface **)
-
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
let
val sign = Theory.sign_of thy;
@@ -915,5 +833,4 @@
end;
-
end;