--- a/src/HOL/HOL.ML Wed Aug 06 01:12:03 1997 +0200
+++ b/src/HOL/HOL.ML Wed Aug 06 01:13:46 1997 +0200
@@ -349,7 +349,7 @@
_ $ (Const("op -->",_)$_$_) => th RS mp
| _ => raise THM("RSmp",0,[th]));
-(*Used in qed_spec_mp, etc., which are declared in thy_data.ML*)
+(*Used in qed_spec_mp, etc.*)
fun normalize_thm funs =
let fun trans [] th = th
| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
@@ -357,6 +357,15 @@
end;
+fun qed_spec_mp name =
+ let val thm = normalize_thm [RSspec,RSmp] (result())
+ in bind_thm(name, thm) end;
+
+fun qed_goal_spec_mp name thy s p =
+ bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
+
+fun qed_goalw_spec_mp name thy defs s p =
+ bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
(*Thus, assignments to the references claset and simpset are recorded
with theory "HOL". These files cannot be loaded directly in ROOT.ML.*)
--- a/src/HOL/cladata.ML Wed Aug 06 01:12:03 1997 +0200
+++ b/src/HOL/cladata.ML Wed Aug 06 01:13:46 1997 +0200
@@ -59,6 +59,11 @@
("claset", ThyMethods {merge = merge, put = put, get = get})
end;
+fun claset_of tname =
+ case get_thydata tname "claset" of
+ None => empty_cs
+ | Some (CS_DATA cs) => cs;
+
claset := HOL_cs;
(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
--- a/src/HOL/datatype.ML Wed Aug 06 01:12:03 1997 +0200
+++ b/src/HOL/datatype.ML Wed Aug 06 01:13:46 1997 +0200
@@ -5,6 +5,91 @@
Copyright 1995 TU Muenchen
*)
+(** Information about datatypes **)
+
+(* Retrieve information for a specific datatype *)
+fun datatype_info thy tname =
+ case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
+ None => None
+ | Some (DT_DATA ds) => assoc (ds, tname);
+
+fun match_info thy tname =
+ case datatype_info thy tname of
+ Some {case_const, constructors, ...} =>
+ {case_const=case_const, constructors=constructors}
+ | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
+
+fun induct_info thy tname =
+ case datatype_info thy tname of
+ Some {constructors, nchotomy, ...} =>
+ {constructors=constructors, nchotomy=nchotomy}
+ | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
+
+
+(* Retrieve information for all datatypes defined in a theory and its
+ ancestors *)
+fun extract_info thy =
+ let val (congs, rewrites) =
+ case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
+ None => ([], [])
+ | Some (DT_DATA ds) =>
+ let val info = map snd ds
+ in (map #case_cong info, flat (map #case_rewrites info)) end;
+ in {case_congs = congs, case_rewrites = rewrites} end;
+
+local
+
+fun find_tname var Bi =
+ let val frees = map dest_Free (term_frees Bi)
+ val params = Logic.strip_params Bi;
+ in case assoc (frees@params, var) of
+ None => error("No such variable in subgoal: " ^ quote var)
+ | Some(Type(tn,_)) => tn
+ | _ => error("Cannot induct on type of " ^ quote var)
+ end;
+
+fun get_dt_info sign tn =
+ case get_thydata (thyname_of_sign sign) "datatypes" of
+ None => error ("No such datatype: " ^ quote tn)
+ | Some (DT_DATA ds) =>
+ case assoc (ds, tn) of
+ Some info => info
+ | None => error ("Not a datatype: " ^ quote tn)
+
+fun infer_tname state sign i aterm =
+let val (_, _, Bi, _) = dest_state (state, i)
+ val params = Logic.strip_params Bi (*params of subgoal i*)
+ val params = rev(rename_wrt_term Bi params) (*as they are printed*)
+ val (types,sorts) = types_sorts state
+ fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
+ | types'(ixn) = types ixn;
+ val (ct,_) = read_def_cterm (sign,types',sorts) [] false
+ (aterm,TVar(("",0),[]));
+in case #T(rep_cterm ct) of
+ Type(tn,_) => tn
+ | _ => error("Cannot induct on type of " ^ quote aterm)
+end;
+
+in
+
+(* generic induction tactic for datatypes *)
+fun induct_tac var i state = state |>
+ let val (_, _, Bi, _) = dest_state (state, i)
+ val sign = #sign(rep_thm state)
+ val tn = find_tname var Bi
+ val ind_tac = #induct_tac(get_dt_info sign tn)
+ in ind_tac var i end;
+
+(* generic exhaustion tactic for datatypes *)
+fun exhaust_tac aterm i state = state |>
+ let val sign = #sign(rep_thm state)
+ val tn = infer_tname state sign i aterm
+ val exh_tac = #exhaust_tac(get_dt_info sign tn)
+ in exh_tac aterm i end;
+
+end;
+
+
(* should go into Pure *)
fun ALLNEWSUBGOALS tac tacf i st0 = st0 |>
(tac i THEN
--- a/src/HOL/simpdata.ML Wed Aug 06 01:12:03 1997 +0200
+++ b/src/HOL/simpdata.ML Wed Aug 06 01:13:46 1997 +0200
@@ -401,6 +401,11 @@
("simpset", ThyMethods {merge = merge, put = put, get = get})
end;
+fun simpset_of tname =
+ case get_thydata tname "simpset" of
+ None => empty_ss
+ | Some (SS_DATA ss) => ss;
+
type dtype_info = {case_const:term,
case_rewrites:thm list,
constructors:term list,
@@ -426,10 +431,6 @@
end;
-add_thy_reader_file "thy_data.ML";
-
-
-
(*** Integration of simplifier with classical reasoner ***)