author  wenzelm 
Sat, 01 Apr 2000 20:21:39 +0200  
changeset 8657  b9475dad85ed 
parent 8625  93a11ebacf32 
child 8711  00ec2ba9174d 
permissions  rwrr 
6429  1 
(* Title: HOL/Tools/recdef_package.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Wrapper module for Konrad Slind's TFL package. 

6 
*) 

7 

8 
signature RECDEF_PACKAGE = 

9 
sig 

10 
val quiet_mode: bool ref 

6439  11 
val print_recdefs: theory > unit 
8657  12 
val get_recdef: theory > string 
13 
> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option 

14 
val add_recdef: xstring > string > ((bstring * string) * Args.src list) list 

15 
> simpset option > (xstring * Args.src list) list > theory 

16 
> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} 

17 
val add_recdef_i: xstring > term > ((bstring * term) * theory attribute list) list 

18 
> simpset option > (thm * theory attribute list) list 

19 
> theory > theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} 

6557  20 
val defer_recdef: xstring > string list > (xstring * Args.src list) list 
21 
> theory > theory * {induct_rules: thm} 

22 
val defer_recdef_i: xstring > term list > (thm * theory attribute list) list 

23 
> theory > theory * {induct_rules: thm} 

6439  24 
val setup: (theory > theory) list 
6429  25 
end; 
26 

27 
structure RecdefPackage: RECDEF_PACKAGE = 

28 
struct 

29 

30 
val quiet_mode = Tfl.quiet_mode; 

31 
val message = Tfl.message; 

32 

33 

6439  34 

35 
(** theory data **) 

36 

37 
(* data kind 'HOL/recdef' *) 

38 

8657  39 
type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list}; 
6439  40 

41 
structure RecdefArgs = 

42 
struct 

43 
val name = "HOL/recdef"; 

44 
type T = recdef_info Symtab.table; 

45 

46 
val empty = Symtab.empty; 

6557  47 
val copy = I; 
6439  48 
val prep_ext = I; 
49 
val merge: T * T > T = Symtab.merge (K true); 

50 

51 
fun print sg tab = 

52 
Pretty.writeln (Pretty.strs ("recdefs:" :: 

6851  53 
map #1 (Sign.cond_extern_table sg Sign.constK tab))); 
6439  54 
end; 
55 

56 
structure RecdefData = TheoryDataFun(RecdefArgs); 

57 
val print_recdefs = RecdefData.print; 

6429  58 

6439  59 

60 
(* get and put data *) 

61 

8481
89d498a8d3f6
get_recdef now returns None instead of raising ERROR.
berghofe
parents:
8430
diff
changeset

62 
fun get_recdef thy name = Symtab.lookup (RecdefData.get thy, name); 
6439  63 

64 
fun put_recdef name info thy = 

6429  65 
let 
6439  66 
val tab = Symtab.update_new ((name, info), RecdefData.get thy) 
67 
handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name); 

68 
in RecdefData.put tab thy end; 

69 

70 

71 

72 
(** add_recdef(_i) **) 

73 

6557  74 
fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions"; 
75 

8657  76 
fun gen_add_recdef tfl_fn prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy = 
6439  77 
let 
78 
val name = Sign.intern_const (Theory.sign_of thy) raw_name; 

79 
val bname = Sign.base_name name; 

80 

6557  81 
val _ = requires_recdef thy; 
6429  82 
val _ = message ("Defining recursive function " ^ quote name ^ " ..."); 
83 

8657  84 
val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs); 
85 
val eq_atts = map (map (prep_att thy)) raw_eq_atts; 

6429  86 
val ss = (case raw_ss of None => Simplifier.simpset_of thy  Some x => prep_ss x); 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

87 
val (thy, congs) = thy > app_thms raw_congs; 
8657  88 

89 
val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs; 

90 
val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx); 

91 
val simp_att = if null tcs then [Simplifier.simp_add_global] else []; 

92 

8430  93 
val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct); 
8657  94 
val (thy, (simps' :: rules', [induct'])) = 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

95 
thy 
6439  96 
> Theory.add_path bname 
8657  97 
> PureThy.add_thmss ((("simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) 
8430  98 
>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])]; 
8657  99 
val result = {simps = simps', rules = rules', induct = induct', tcs = tcs}; 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

100 
val thy = 
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

101 
thy 
6439  102 
> put_recdef name result 
6429  103 
> Theory.parent_path; 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

104 
in (thy, result) end; 
6429  105 

8657  106 
val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute I IsarThy.apply_theorems; 
107 
val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute 

108 
(Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems; 

109 
val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i; 

6429  110 

111 

6557  112 

113 
(** defer_recdef(_i) **) 

114 

115 
fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy = 

116 
let 

117 
val name = Sign.intern_const (Theory.sign_of thy) raw_name; 

118 
val bname = Sign.base_name name; 

119 

120 
val _ = requires_recdef thy; 

121 
val _ = message ("Deferred recursive function " ^ quote name ^ " ..."); 

122 

123 
val (thy1, congs) = thy > app_thms raw_congs; 

124 
val (thy2, induct_rules) = tfl_fn thy1 name congs eqs; 

8430  125 
val (thy3, [induct_rules']) = 
6557  126 
thy2 
127 
> Theory.add_path bname 

128 
> PureThy.add_thms [(("induct_rules", induct_rules), [])] 

8430  129 
>> Theory.parent_path; 
130 
in (thy3, {induct_rules = induct_rules'}) end; 

6557  131 

132 
val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems; 

133 
val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i; 

134 

135 

136 

6439  137 
(** package setup **) 
138 

139 
(* setup theory *) 

140 

141 
val setup = [RecdefData.init]; 

142 

143 

6429  144 
(* outer syntax *) 
145 

6723  146 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6429  147 

148 
val recdef_decl = 

8657  149 
P.name  P.term  Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)  
6723  150 
Scan.optional (P.$$$ "("  P.$$$ "congs"  P.!!! (P.xthms1  P.$$$ ")")) []  
151 
Scan.option (P.$$$ "("  P.$$$ "simpset"  P.!!! (P.name  P.$$$ ")")) 

8657  152 
>> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R (map P.triple_swap eqs) ss congs); 
6429  153 

154 
val recdefP = 

6723  155 
OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl 
6429  156 
(recdef_decl >> Toplevel.theory); 
157 

6557  158 

159 
val defer_recdef_decl = 

8657  160 
P.name  Scan.repeat1 P.prop  
6723  161 
Scan.optional (P.$$$ "("  P.$$$ "congs"  P.!!! (P.xthms1  P.$$$ ")")) [] 
6557  162 
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs); 
163 

164 
val defer_recdefP = 

6723  165 
OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl 
6557  166 
(defer_recdef_decl >> Toplevel.theory); 
167 

6429  168 
val _ = OuterSyntax.add_keywords ["congs", "simpset"]; 
6557  169 
val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP]; 
6429  170 

171 
end; 

172 

173 

174 
end; 