# HG changeset patch # User berghofe # Date 870822826 -7200 # Node ID e5322197cfea433a726fc0ea2194efaee48edbbb # Parent 21c06e95ec395514979a460624a0f953817e9037 Moved some functions which used to be part of thy_data.ML diff -r 21c06e95ec39 -r e5322197cfea src/HOL/HOL.ML --- 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.*) diff -r 21c06e95ec39 -r e5322197cfea src/HOL/cladata.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!*) diff -r 21c06e95ec39 -r e5322197cfea src/HOL/datatype.ML --- 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 diff -r 21c06e95ec39 -r e5322197cfea src/HOL/simpdata.ML --- 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 ***)