Moved some functions which used to be part of thy_data.ML
authorberghofe
Wed Aug 06 01:13:46 1997 +0200 (1997-08-06)
changeset 3615e5322197cfea
parent 3614 21c06e95ec39
child 3616 fcd7e70258f7
Moved some functions which used to be part of thy_data.ML
src/HOL/HOL.ML
src/HOL/cladata.ML
src/HOL/datatype.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL.ML	Wed Aug 06 01:12:03 1997 +0200
     1.2 +++ b/src/HOL/HOL.ML	Wed Aug 06 01:13:46 1997 +0200
     1.3 @@ -349,7 +349,7 @@
     1.4       _ $ (Const("op -->",_)$_$_) => th RS mp
     1.5    | _ => raise THM("RSmp",0,[th]));
     1.6  
     1.7 -(*Used in qed_spec_mp, etc., which are declared in thy_data.ML*)
     1.8 +(*Used in qed_spec_mp, etc.*)
     1.9  fun normalize_thm funs =
    1.10  let fun trans [] th = th
    1.11        | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
    1.12 @@ -357,6 +357,15 @@
    1.13  
    1.14  end;
    1.15  
    1.16 +fun qed_spec_mp name =
    1.17 +  let val thm = normalize_thm [RSspec,RSmp] (result())
    1.18 +  in bind_thm(name, thm) end;
    1.19 +
    1.20 +fun qed_goal_spec_mp name thy s p = 
    1.21 +	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
    1.22 +
    1.23 +fun qed_goalw_spec_mp name thy defs s p = 
    1.24 +	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
    1.25  
    1.26  (*Thus, assignments to the references claset and simpset are recorded
    1.27    with theory "HOL".  These files cannot be loaded directly in ROOT.ML.*)
     2.1 --- a/src/HOL/cladata.ML	Wed Aug 06 01:12:03 1997 +0200
     2.2 +++ b/src/HOL/cladata.ML	Wed Aug 06 01:13:46 1997 +0200
     2.3 @@ -59,6 +59,11 @@
     2.4       ("claset", ThyMethods {merge = merge, put = put, get = get})
     2.5  end;
     2.6  
     2.7 +fun claset_of tname =
     2.8 +  case get_thydata tname "claset" of
     2.9 +      None => empty_cs
    2.10 +    | Some (CS_DATA cs) => cs;
    2.11 +
    2.12  claset := HOL_cs;
    2.13  
    2.14  (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
     3.1 --- a/src/HOL/datatype.ML	Wed Aug 06 01:12:03 1997 +0200
     3.2 +++ b/src/HOL/datatype.ML	Wed Aug 06 01:13:46 1997 +0200
     3.3 @@ -5,6 +5,91 @@
     3.4     Copyright 1995 TU Muenchen
     3.5  *)
     3.6  
     3.7 +(** Information about datatypes **)
     3.8 +
     3.9 +(* Retrieve information for a specific datatype *)
    3.10 +fun datatype_info thy tname =
    3.11 +  case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
    3.12 +      None => None
    3.13 +    | Some (DT_DATA ds) => assoc (ds, tname);
    3.14 +
    3.15 +fun match_info thy tname =
    3.16 +  case datatype_info thy tname of
    3.17 +      Some {case_const, constructors, ...} =>
    3.18 +        {case_const=case_const, constructors=constructors}
    3.19 +    | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
    3.20 +
    3.21 +fun induct_info thy tname =
    3.22 +  case datatype_info thy tname of
    3.23 +      Some {constructors, nchotomy, ...} =>
    3.24 +        {constructors=constructors, nchotomy=nchotomy}
    3.25 +    | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
    3.26 +
    3.27 +
    3.28 +(* Retrieve information for all datatypes defined in a theory and its
    3.29 +   ancestors *)
    3.30 +fun extract_info thy =
    3.31 +  let val (congs, rewrites) =
    3.32 +        case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
    3.33 +            None => ([], [])
    3.34 +          | Some (DT_DATA ds) =>
    3.35 +              let val info = map snd ds
    3.36 +              in (map #case_cong info, flat (map #case_rewrites info)) end;
    3.37 +  in {case_congs = congs, case_rewrites = rewrites} end;
    3.38 +
    3.39 +local
    3.40 +
    3.41 +fun find_tname var Bi =
    3.42 +  let val frees = map dest_Free (term_frees Bi)
    3.43 +      val params = Logic.strip_params Bi;
    3.44 +  in case assoc (frees@params, var) of
    3.45 +       None => error("No such variable in subgoal: " ^ quote var)
    3.46 +     | Some(Type(tn,_)) => tn
    3.47 +     | _ => error("Cannot induct on type of " ^ quote var)
    3.48 +  end;
    3.49 +
    3.50 +fun get_dt_info sign tn =
    3.51 +      case get_thydata (thyname_of_sign sign) "datatypes" of
    3.52 +        None => error ("No such datatype: " ^ quote tn)
    3.53 +      | Some (DT_DATA ds) =>
    3.54 +          case assoc (ds, tn) of
    3.55 +            Some info => info
    3.56 +          | None => error ("Not a datatype: " ^ quote tn)
    3.57 +
    3.58 +fun infer_tname state sign i aterm =
    3.59 +let val (_, _, Bi, _) = dest_state (state, i)
    3.60 +    val params = Logic.strip_params Bi	        (*params of subgoal i*)
    3.61 +    val params = rev(rename_wrt_term Bi params) (*as they are printed*)
    3.62 +    val (types,sorts) = types_sorts state
    3.63 +    fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
    3.64 +      | types'(ixn) = types ixn;
    3.65 +    val (ct,_) = read_def_cterm (sign,types',sorts) [] false
    3.66 +                                (aterm,TVar(("",0),[]));
    3.67 +in case #T(rep_cterm ct) of
    3.68 +     Type(tn,_) => tn
    3.69 +   | _ => error("Cannot induct on type of " ^ quote aterm)
    3.70 +end;
    3.71 +
    3.72 +in
    3.73 +
    3.74 +(* generic induction tactic for datatypes *)
    3.75 +fun induct_tac var i state = state |>
    3.76 +        let val (_, _, Bi, _) = dest_state (state, i)
    3.77 +            val sign = #sign(rep_thm state)
    3.78 +            val tn = find_tname var Bi
    3.79 +            val ind_tac = #induct_tac(get_dt_info sign tn)
    3.80 +        in ind_tac var i end;
    3.81 +
    3.82 +(* generic exhaustion tactic for datatypes *)
    3.83 +fun exhaust_tac aterm i state = state |>
    3.84 +        let val sign = #sign(rep_thm state)
    3.85 +            val tn = infer_tname state sign i aterm
    3.86 +            val exh_tac = #exhaust_tac(get_dt_info sign tn)
    3.87 +        in exh_tac aterm i end;
    3.88 +
    3.89 +end;
    3.90 +
    3.91 +
    3.92  (* should go into Pure *)
    3.93  fun ALLNEWSUBGOALS tac tacf i st0 = st0 |>
    3.94    (tac i THEN
     4.1 --- a/src/HOL/simpdata.ML	Wed Aug 06 01:12:03 1997 +0200
     4.2 +++ b/src/HOL/simpdata.ML	Wed Aug 06 01:13:46 1997 +0200
     4.3 @@ -401,6 +401,11 @@
     4.4       ("simpset", ThyMethods {merge = merge, put = put, get = get})
     4.5  end;
     4.6  
     4.7 +fun simpset_of tname =
     4.8 +  case get_thydata tname "simpset" of
     4.9 +      None => empty_ss
    4.10 +    | Some (SS_DATA ss) => ss;
    4.11 +
    4.12  type dtype_info = {case_const:term,
    4.13                     case_rewrites:thm list,
    4.14                     constructors:term list,
    4.15 @@ -426,10 +431,6 @@
    4.16  end;
    4.17  
    4.18  
    4.19 -add_thy_reader_file "thy_data.ML";
    4.20 -
    4.21 -
    4.22 -
    4.23  
    4.24  (*** Integration of simplifier with classical reasoner ***)
    4.25