author  haftmann 
Mon, 30 Nov 2009 11:42:49 +0100  
changeset 33968  f94fb13ecbb3 
parent 33963  src/HOL/Tools/Datatype/datatype.ML@977b94b64905 
permissions  rwrr 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

1 
(* Title: HOL/Tools/Datatype/datatype_data.ML 
11539  2 
Author: Stefan Berghofer, TU Muenchen 
5177  3 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

4 
Datatype package: bookkeeping; interpretation of existing types as datatypes. 
5177  5 
*) 
6 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

7 
signature DATATYPE_DATA = 
6360  8 
sig 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

9 
include DATATYPE_COMMON 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

10 
val derive_datatype_props : config > string list > string list option 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

11 
> descr list > (string * sort) list > thm > thm list list > thm list list 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

12 
> theory > string list * theory 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

13 
val rep_datatype : config > (string list > Proof.context > Proof.context) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

14 
> string list option > term list > theory > Proof.state 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

15 
val rep_datatype_cmd : string list option > string list > theory > Proof.state 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

16 
val get_info : theory > string > info option 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

17 
val the_info : theory > string > info 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

18 
val the_descr : theory > string list 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

19 
> descr * (string * sort) list * string list 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

20 
* string * (string list * string list) * (typ list * typ list) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

21 
val the_spec : theory > string > (string * sort) list * (string * typ list) list 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

22 
val all_distincts : theory > typ list > thm list list 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

23 
val get_constrs : theory > string > (string * typ) list option 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

24 
val get_all : theory > info Symtab.table 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

25 
val info_of_constr : theory > string * typ > info option 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

26 
val info_of_case : theory > string > info option 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

27 
val interpretation : (config > string list > theory > theory) > theory > theory 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

28 
val make_case : Proof.context > Datatype_Case.config > string list > term > 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

29 
(term * term) list > term * (term * (int * bool)) list 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

30 
val strip_case : Proof.context > bool > term > (term * (term * term) list) option 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

31 
val read_typ: theory > string > (string * sort) list > typ * (string * sort) list 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

32 
val cert_typ: theory > typ > (string * sort) list > typ * (string * sort) list 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

33 
val mk_case_names_induct: descr > attribute 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

34 
val setup: theory > theory 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

35 
end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

36 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

37 
structure Datatype_Data: DATATYPE_DATA = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

38 
struct 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

39 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

40 
open Datatype_Aux; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

41 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

42 
(** theory data **) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

43 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

44 
(* data management *) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

45 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

46 
structure DatatypesData = Theory_Data 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

47 
( 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

48 
type T = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

49 
{types: info Symtab.table, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

50 
constrs: (string * info) list Symtab.table, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

51 
cases: info Symtab.table}; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

52 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

53 
val empty = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

54 
{types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty}; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

55 
val extend = I; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

56 
fun merge 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

57 
({types = types1, constrs = constrs1, cases = cases1}, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

58 
{types = types2, constrs = constrs2, cases = cases2}) : T = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

59 
{types = Symtab.merge (K true) (types1, types2), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

60 
constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

61 
cases = Symtab.merge (K true) (cases1, cases2)}; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

62 
); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

63 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

64 
val get_all = #types o DatatypesData.get; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

65 
val get_info = Symtab.lookup o get_all; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

66 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

67 
fun the_info thy name = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

68 
(case get_info thy name of 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

69 
SOME info => info 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

70 
 NONE => error ("Unknown datatype " ^ quote name)); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

71 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

72 
fun info_of_constr thy (c, T) = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

73 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

74 
val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

75 
val hint = case strip_type T of (_, Type (tyco, _)) => SOME tyco  _ => NONE; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

76 
val default = if null tab then NONE 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

77 
else SOME (snd (Library.last_elem tab)) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

78 
(*conservative wrt. overloaded constructors*); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

79 
in case hint 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

80 
of NONE => default 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

81 
 SOME tyco => case AList.lookup (op =) tab tyco 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

82 
of NONE => default (*permissive*) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

83 
 SOME info => SOME info 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

84 
end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

85 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

86 
val info_of_case = Symtab.lookup o #cases o DatatypesData.get; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

87 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

88 
fun register (dt_infos : (string * info) list) = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

89 
DatatypesData.map (fn {types, constrs, cases} => 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

90 
{types = types > fold Symtab.update dt_infos, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

91 
constrs = constrs > fold (fn (constr, dtname_info) => 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

92 
Symtab.map_default (constr, []) (cons dtname_info)) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

93 
(maps (fn (dtname, info as {descr, index, ...}) => 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

94 
map (rpair (dtname, info) o fst) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

95 
(#3 (the (AList.lookup op = descr index)))) dt_infos), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

96 
cases = cases > fold Symtab.update 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

97 
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

98 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

99 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

100 
(* complex queries *) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

101 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

102 
fun the_spec thy dtco = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

103 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

104 
val info as { descr, index, sorts = raw_sorts, ... } = the_info thy dtco; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

105 
val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

106 
val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v)) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

107 
o Datatype_Aux.dest_DtTFree) dtys; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

108 
val cos = map 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

109 
(fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr sorts) tys)) raw_cos; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

110 
in (sorts, cos) end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

111 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

112 
fun the_descr thy (raw_tycos as raw_tyco :: _) = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

113 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

114 
val info = the_info thy raw_tyco; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

115 
val descr = #descr info; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

116 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

117 
val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

118 
val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v)) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

119 
o dest_DtTFree) dtys; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

120 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

121 
fun is_DtTFree (DtTFree _) = true 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

122 
 is_DtTFree _ = false 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

123 
val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

124 
val protoTs as (dataTs, _) = chop k descr 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

125 
> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs)); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

126 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

127 
val tycos = map fst dataTs; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

128 
val _ = if eq_set (op =) (tycos, raw_tycos) then () 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

129 
else error ("Type constructors " ^ commas (map quote raw_tycos) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

130 
^ " do not belong exhaustively to one mutual recursive datatype"); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

131 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

132 
val (Ts, Us) = (pairself o map) Type protoTs; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

133 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

134 
val names = map Long_Name.base_name (the_default tycos (#alt_names info)); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

135 
val (auxnames, _) = Name.make_context names 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

136 
> fold_map (yield_singleton Name.variants o name_of_typ) Us; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

137 
val prefix = space_implode "_" names; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

138 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

139 
in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

140 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

141 
fun all_distincts thy Ts = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

142 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

143 
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

144 
 add_tycos _ = I; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

145 
val tycos = fold add_tycos Ts []; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

146 
in map_filter (Option.map #distinct o get_info thy) tycos end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

147 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

148 
fun get_constrs thy dtco = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

149 
case try (the_spec thy) dtco 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

150 
of SOME (sorts, cos) => 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

151 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

152 
fun subst (v, sort) = TVar ((v, 0), sort); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

153 
fun subst_ty (TFree v) = subst v 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

154 
 subst_ty ty = ty; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

155 
val dty = Type (dtco, map subst sorts); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

156 
fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys > dty); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

157 
in SOME (map mk_co cos) end 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

158 
 NONE => NONE; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

159 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

160 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

161 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

162 
(** various auxiliary **) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

163 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

164 
(* prepare datatype specifications *) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

165 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

166 
fun read_typ thy str sorts = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

167 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

168 
val ctxt = ProofContext.init thy 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

169 
> fold (Variable.declare_typ o TFree) sorts; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

170 
val T = Syntax.read_typ ctxt str; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

171 
in (T, Term.add_tfreesT T sorts) end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

172 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

173 
fun cert_typ sign raw_T sorts = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

174 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

175 
val T = Type.no_tvars (Sign.certify_typ sign raw_T) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

176 
handle TYPE (msg, _, _) => error msg; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

177 
val sorts' = Term.add_tfreesT T sorts; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

178 
val _ = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

179 
case duplicates (op =) (map fst sorts') of 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

180 
[] => () 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

181 
 dups => error ("Inconsistent sort constraints for " ^ commas dups) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

182 
in (T, sorts') end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

183 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

184 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

185 
(* case names *) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

186 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

187 
local 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

188 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

189 
fun dt_recs (DtTFree _) = [] 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

190 
 dt_recs (DtType (_, dts)) = maps dt_recs dts 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

191 
 dt_recs (DtRec i) = [i]; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

192 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

193 
fun dt_cases (descr: descr) (_, args, constrs) = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

194 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

195 
fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i))); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

196 
val bnames = map the_bname (distinct (op =) (maps dt_recs args)); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

197 
in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

198 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

199 
fun induct_cases descr = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

200 
Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr)); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

201 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

202 
fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i)); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

203 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

204 
in 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

205 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

206 
fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

207 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

208 
fun mk_case_names_exhausts descr new = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

209 
map (Rule_Cases.case_names o exhaust_cases descr o #1) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

210 
(filter (fn ((_, (name, _, _))) => member (op =) new name) descr); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

211 

32717
0e787c721fa3
reestablished reasonable inner outline for module
haftmann
parents:
32712
diff
changeset

212 
end; 
0e787c721fa3
reestablished reasonable inner outline for module
haftmann
parents:
32712
diff
changeset

213 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

214 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

215 
(* translation rules for case *) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

216 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

217 
fun make_case ctxt = Datatype_Case.make_case 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

218 
(info_of_constr (ProofContext.theory_of ctxt)) ctxt; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

219 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

220 
fun strip_case ctxt = Datatype_Case.strip_case 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

221 
(info_of_case (ProofContext.theory_of ctxt)); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

222 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

223 
fun add_case_tr' case_names thy = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

224 
Sign.add_advanced_trfuns ([], [], 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

225 
map (fn case_name => 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

226 
let val case_name' = Sign.const_syntax_name thy case_name 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

227 
in (case_name', Datatype_Case.case_tr' info_of_case case_name') 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

228 
end) case_names, []) thy; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

229 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

230 
val trfun_setup = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

231 
Sign.add_advanced_trfuns ([], 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

232 
[("_case_syntax", Datatype_Case.case_tr true info_of_constr)], 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

233 
[], []); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

234 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

235 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

236 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

237 
(** document antiquotation **) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

238 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

239 
val _ = ThyOutput.antiquotation "datatype" Args.tyname 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

240 
(fn {source = src, context = ctxt, ...} => fn dtco => 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

241 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

242 
val thy = ProofContext.theory_of ctxt; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

243 
val (vs, cos) = the_spec thy dtco; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

244 
val ty = Type (dtco, map TFree vs); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

245 
fun pretty_typ_bracket (ty as Type (_, _ :: _)) = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

246 
Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty] 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

247 
 pretty_typ_bracket ty = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

248 
Syntax.pretty_typ ctxt ty; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

249 
fun pretty_constr (co, tys) = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

250 
(Pretty.block o Pretty.breaks) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

251 
(Syntax.pretty_term ctxt (Const (co, tys > ty)) :: 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

252 
map pretty_typ_bracket tys); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

253 
val pretty_datatype = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

254 
Pretty.block 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

255 
(Pretty.command "datatype" :: Pretty.brk 1 :: 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

256 
Syntax.pretty_typ ctxt ty :: 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

257 
Pretty.str " =" :: Pretty.brk 1 :: 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

258 
flat (separate [Pretty.brk 1, Pretty.str " "] 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

259 
(map (single o pretty_constr) cos))); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

260 
in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

261 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

262 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

263 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

264 
(** abstract theory extensions relative to a datatype characterisation **) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

265 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

266 
structure Datatype_Interpretation = Interpretation 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

267 
(type T = config * string list val eq: T * T > bool = eq_snd op =); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

268 
fun interpretation f = Datatype_Interpretation.interpretation (uncurry f); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

269 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

270 
fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

271 
(index, (((((((((((_, (tname, _, _))), inject), distinct), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

272 
exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

273 
(split, split_asm))) = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

274 
(tname, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

275 
{index = index, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

276 
alt_names = alt_names, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

277 
descr = descr, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

278 
sorts = sorts, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

279 
inject = inject, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

280 
distinct = distinct, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

281 
induct = induct, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

282 
inducts = inducts, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

283 
exhaust = exhaust, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

284 
nchotomy = nchotomy, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

285 
rec_names = rec_names, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

286 
rec_rewrites = rec_rewrites, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

287 
case_name = case_name, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

288 
case_rewrites = case_rewrites, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

289 
case_cong = case_cong, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

290 
weak_case_cong = weak_case_cong, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

291 
split = split, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

292 
split_asm = split_asm}); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

293 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

294 
fun derive_datatype_props config dt_names alt_names descr sorts 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

295 
induct inject distinct thy1 = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

296 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

297 
val thy2 = thy1 > Theory.checkpoint; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

298 
val flat_descr = flat descr; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

299 
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

300 
val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

301 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

302 
val (exhaust, thy3) = Datatype_Abs_Proofs.prove_casedist_thms config new_type_names 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

303 
descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

304 
val (nchotomys, thy4) = Datatype_Abs_Proofs.prove_nchotomys config new_type_names 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

305 
descr sorts exhaust thy3; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

306 
val ((rec_names, rec_rewrites), thy5) = Datatype_Abs_Proofs.prove_primrec_thms 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

307 
config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4)) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

308 
inject (distinct, all_distincts thy2 (get_rec_types flat_descr sorts)) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

309 
induct thy4; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

310 
val ((case_rewrites, case_names), thy6) = Datatype_Abs_Proofs.prove_case_thms 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

311 
config new_type_names descr sorts rec_names rec_rewrites thy5; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

312 
val (case_congs, thy7) = Datatype_Abs_Proofs.prove_case_congs new_type_names 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

313 
descr sorts nchotomys case_rewrites thy6; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

314 
val (weak_case_congs, thy8) = Datatype_Abs_Proofs.prove_weak_case_congs new_type_names 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

315 
descr sorts thy7; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

316 
val (splits, thy9) = Datatype_Abs_Proofs.prove_split_thms 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

317 
config new_type_names descr sorts inject distinct exhaust case_rewrites thy8; 
5177  318 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

319 
val inducts = Project_Rule.projections (ProofContext.init thy2) induct; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

320 
val dt_infos = map_index 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

321 
(make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

322 
(hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~ 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

323 
case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

324 
val dt_names = map fst dt_infos; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

325 
val prfx = Binding.qualify true (space_implode "_" new_type_names); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

326 
val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

327 
val named_rules = flat (map_index (fn (index, tname) => 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

328 
[((Binding.empty, [nth inducts index]), [Induct.induct_type tname]), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

329 
((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

330 
val unnamed_rules = map (fn induct => 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

331 
((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""])) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

332 
(drop (length dt_names) inducts); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

333 
in 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

334 
thy9 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

335 
> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

336 
((prfx (Binding.name "inducts"), inducts), []), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

337 
((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

338 
((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

339 
[Simplifier.simp_add]), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

340 
((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

341 
((Binding.empty, flat inject), [iff_add]), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

342 
((Binding.empty, map (fn th => th RS notE) (flat distinct)), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

343 
[Classical.safe_elim NONE]), 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

344 
((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])] 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

345 
@ named_rules @ unnamed_rules) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

346 
> snd 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

347 
> add_case_tr' case_names 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

348 
> register dt_infos 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

349 
> Datatype_Interpretation.data (config, dt_names) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

350 
> pair dt_names 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

351 
end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

352 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

353 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

354 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

355 
(** declare existing type as datatype **) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

356 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

357 
fun prove_rep_datatype config dt_names alt_names descr sorts 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

358 
raw_inject half_distinct raw_induct thy1 = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

359 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

360 
val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

361 
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

362 
val (((inject, distinct), [induct]), thy2) = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

363 
thy1 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

364 
> store_thmss "inject" new_type_names raw_inject 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

365 
>> store_thmss "distinct" new_type_names raw_distinct 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

366 
> Sign.add_path (space_implode "_" new_type_names) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

367 
>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])] 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

368 
> Sign.restore_naming thy1; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

369 
in 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

370 
thy2 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

371 
> derive_datatype_props config dt_names alt_names [descr] sorts 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

372 
induct inject distinct 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

373 
end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

374 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

375 
fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

376 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

377 
fun constr_of_term (Const (c, T)) = (c, T) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

378 
 constr_of_term t = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

379 
error ("Not a constant: " ^ Syntax.string_of_term_global thy t); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

380 
fun no_constr (c, T) = error ("Bad constructor: " 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

381 
^ Sign.extern_const thy c ^ "::" 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

382 
^ Syntax.string_of_typ_global thy T); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

383 
fun type_of_constr (cT as (_, T)) = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

384 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

385 
val frees = OldTerm.typ_tfrees T; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

386 
val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

387 
handle TYPE _ => no_constr cT 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

388 
val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else (); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

389 
val _ = if length frees <> length vs then no_constr cT else (); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

390 
in (tyco, (vs, cT)) end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

391 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

392 
val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

393 
val _ = case map_filter (fn (tyco, _) => 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

394 
if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

395 
of [] => () 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

396 
 tycos => error ("Type(s) " ^ commas (map quote tycos) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

397 
^ " already represented inductivly"); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

398 
val raw_vss = maps (map (map snd o fst) o snd) raw_cs; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

399 
val ms = case distinct (op =) (map length raw_vss) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

400 
of [n] => 0 upto n  1 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

401 
 _ => error ("Different types in given constructors"); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

402 
fun inter_sort m = map (fn xs => nth xs m) raw_vss 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

403 
> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy)) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

404 
val sorts = map inter_sort ms; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

405 
val vs = Name.names Name.context Name.aT sorts; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

406 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

407 
fun norm_constr (raw_vs, (c, T)) = (c, map_atyps 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

408 
(TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

409 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

410 
val cs = map (apsnd (map norm_constr)) raw_cs; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

411 
val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

412 
o fst o strip_type; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

413 
val dt_names = map fst cs; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

414 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

415 
fun mk_spec (i, (tyco, constr)) = (i, (tyco, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

416 
map (DtTFree o fst) vs, 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

417 
(map o apsnd) dtyps_of_typ constr)) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

418 
val descr = map_index mk_spec cs; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

419 
val injs = Datatype_Prop.make_injs [descr] vs; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

420 
val half_distincts = map snd (Datatype_Prop.make_distincts [descr] vs); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

421 
val ind = Datatype_Prop.make_ind [descr] vs; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

422 
val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts]; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

423 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

424 
fun after_qed' raw_thms = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

425 
let 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

426 
val [[[raw_induct]], raw_inject, half_distinct] = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

427 
unflat rules (map Drule.zero_var_indexes_list raw_thms); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

428 
(*FIXME somehow dubious*) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

429 
in 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

430 
ProofContext.theory_result 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

431 
(prove_rep_datatype config dt_names alt_names descr vs 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

432 
raw_inject half_distinct raw_induct) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

433 
#> after_qed 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

434 
end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

435 
in 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

436 
thy 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

437 
> ProofContext.init 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

438 
> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules)) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

439 
end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

440 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

441 
val rep_datatype = gen_rep_datatype Sign.cert_term; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

442 
val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I); 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

443 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

444 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

445 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

446 
(** package setup **) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

447 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

448 
(* setup theory *) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

449 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

450 
val setup = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

451 
trfun_setup #> 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

452 
Datatype_Interpretation.init; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

453 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

454 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

455 
(* outer syntax *) 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

456 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

457 
local 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

458 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

459 
structure P = OuterParse and K = OuterKeyword 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

460 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

461 
in 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

462 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

463 
val _ = 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

464 
OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

465 
(Scan.option (P.$$$ "("  Scan.repeat1 P.name  P.$$$ ")")  Scan.repeat1 P.term 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

466 
>> (fn (alt_names, ts) => Toplevel.print 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

467 
o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts))); 
6385
5a6570458d9e
rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents:
6360
diff
changeset

468 

30391
d930432adb13
adapted to simplified ThyOutput.antiquotation interface;
wenzelm
parents:
30364
diff
changeset

469 
end; 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

470 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

471 
end; 