src/HOL/thy_data.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2562 d571d6660240
child 3040 7d48671753da
permissions -rw-r--r--
Dep. on Provers/nat_transitive
clasohm@1465
     1
(*  Title:      HOL/thy_data.ML
clasohm@1455
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Carsten Clasohm
clasohm@1455
     4
    Copyright   1995 TU Muenchen
clasohm@1455
     5
clasohm@1455
     6
Definitions that have to be reread after init_thy_reader has been invoked
clasohm@1455
     7
*)
clasohm@1455
     8
clasohm@1455
     9
fun simpset_of tname =
clasohm@1657
    10
  case get_thydata tname "simpset" of
clasohm@1455
    11
      None => empty_ss
clasohm@1455
    12
    | Some (SS_DATA ss) => ss;
clasohm@1455
    13
berghofe@1726
    14
fun claset_of tname =
berghofe@1726
    15
  case get_thydata tname "claset" of
berghofe@1726
    16
      None => empty_cs
berghofe@1726
    17
    | Some (CS_DATA cs) => cs;
berghofe@1726
    18
clasohm@1668
    19
clasohm@1668
    20
(** Information about datatypes **)
clasohm@1668
    21
clasohm@1668
    22
(* Retrieve information for a specific datatype *)
clasohm@1668
    23
fun datatype_info thy tname =
clasohm@1668
    24
  case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
clasohm@1668
    25
      None => None
clasohm@1668
    26
    | Some (DT_DATA ds) => assoc (ds, tname);
clasohm@1668
    27
clasohm@1668
    28
fun match_info thy tname =
clasohm@1668
    29
  case datatype_info thy tname of
clasohm@1668
    30
      Some {case_const, constructors, ...} =>
clasohm@1668
    31
        {case_const=case_const, constructors=constructors}
clasohm@1668
    32
    | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
clasohm@1668
    33
clasohm@1668
    34
fun induct_info thy tname =
clasohm@1668
    35
  case datatype_info thy tname of
clasohm@1668
    36
      Some {constructors, nchotomy, ...} =>
clasohm@1668
    37
        {constructors=constructors, nchotomy=nchotomy}
clasohm@1668
    38
    | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
clasohm@1668
    39
clasohm@1668
    40
clasohm@1668
    41
(* Retrieve information for all datatypes defined in a theory and its
clasohm@1668
    42
   ancestors *)
clasohm@1668
    43
fun extract_info thy =
clasohm@1668
    44
  let val (congs, rewrites) =
clasohm@1668
    45
        case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
clasohm@1668
    46
            None => ([], [])
clasohm@1668
    47
          | Some (DT_DATA ds) =>
clasohm@1668
    48
              let val info = map snd ds
clasohm@1668
    49
              in (map #case_cong info, flat (map #case_rewrites info)) end;
clasohm@1668
    50
  in {case_congs = congs, case_rewrites = rewrites} end;
paulson@2562
    51
paulson@2562
    52
paulson@2562
    53
(*Must be redefined in order to refer to the new instance of bind_thm
paulson@2562
    54
  created by init_thy_reader.*)
paulson@2562
    55
paulson@2562
    56
fun qed_spec_mp name =
paulson@2562
    57
  let val thm = normalize_thm [RSspec,RSmp] (result())
paulson@2562
    58
  in bind_thm(name, thm) end;
paulson@2562
    59
paulson@2562
    60
fun qed_goal_spec_mp name thy s p = 
paulson@2562
    61
	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
paulson@2562
    62
paulson@2562
    63
fun qed_goalw_spec_mp name thy defs s p = 
paulson@2562
    64
	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
paulson@2562
    65