author  wenzelm 
Fri, 08 Oct 1999 15:08:23 +0200  
changeset 7798  42e94b618f34 
parent 7262  a05dc63ca29b 
child 8430  dbd897e0d804 
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 
12 
val get_recdef: theory > string > {rules: thm list, induct: thm, tcs: term list} 

6576  13 
val add_recdef: xstring > string > string list > simpset option 
14 
> (xstring * Args.src list) list > theory 

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

16 
val add_recdef_i: xstring > term > term list > simpset option 

17 
> (thm * theory attribute list) list 

6429  18 
> theory > theory * {rules: thm list, induct: thm, tcs: term list} 
6557  19 
val defer_recdef: xstring > string list > (xstring * Args.src list) list 
20 
> theory > theory * {induct_rules: thm} 

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

22 
> theory > theory * {induct_rules: thm} 

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

26 
structure RecdefPackage: RECDEF_PACKAGE = 

27 
struct 

28 

29 
val quiet_mode = Tfl.quiet_mode; 

30 
val message = Tfl.message; 

31 

32 

6439  33 

34 
(** theory data **) 

35 

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

37 

38 
type recdef_info = {rules: thm list, induct: thm, tcs: term list}; 

39 

40 
structure RecdefArgs = 

41 
struct 

42 
val name = "HOL/recdef"; 

43 
type T = recdef_info Symtab.table; 

44 

45 
val empty = Symtab.empty; 

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

49 

50 
fun print sg tab = 

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

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

55 
structure RecdefData = TheoryDataFun(RecdefArgs); 

56 
val print_recdefs = RecdefData.print; 

6429  57 

6439  58 

59 
(* get and put data *) 

60 

61 
fun get_recdef thy name = 

62 
(case Symtab.lookup (RecdefData.get thy, name) of 

63 
Some info => info 

64 
 None => error ("Unknown recursive function " ^ quote name)); 

65 

66 
fun put_recdef name info thy = 

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

70 
in RecdefData.put tab thy end; 

71 

72 

73 

74 
(** add_recdef(_i) **) 

75 

6557  76 
fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions"; 
77 

6576  78 
fun gen_add_recdef tfl_fn prep_ss app_thms raw_name R eqs raw_ss raw_congs thy = 
6439  79 
let 
80 
val name = Sign.intern_const (Theory.sign_of thy) raw_name; 

81 
val bname = Sign.base_name name; 

82 

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

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; 
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

88 
val (thy, {rules, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs; 
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

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

90 
thy 
6439  91 
> Theory.add_path bname 
6429  92 
> PureThy.add_thmss [(("rules", rules), [])] 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

93 
> PureThy.add_thms [(("induct", induct), [])]; 
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

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

95 
{rules = PureThy.get_thms thy "rules", 
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

96 
induct = PureThy.get_thm thy "induct", 
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

97 
tcs = tcs}; 
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset

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

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

102 
in (thy, result) end; 
6429  103 

6576  104 
val add_recdef = gen_add_recdef Tfl.define I IsarThy.apply_theorems; 
105 
val add_recdef_x = gen_add_recdef Tfl.define (Simplifier.simpset_of o ThyInfo.get_theory) 

106 
IsarThy.apply_theorems; 

107 
val add_recdef_i = gen_add_recdef Tfl.define_i I IsarThy.apply_theorems_i; 

6429  108 

109 

6557  110 

111 
(** defer_recdef(_i) **) 

112 

113 
fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy = 

114 
let 

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

116 
val bname = Sign.base_name name; 

117 

118 
val _ = requires_recdef thy; 

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

120 

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

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

123 
val thy3 = 

124 
thy2 

125 
> Theory.add_path bname 

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

127 
> Theory.parent_path; 

128 
in (thy3, {induct_rules = induct_rules}) end; 

129 

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

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

132 

133 

134 

6439  135 
(** package setup **) 
136 

137 
(* setup theory *) 

138 

139 
val setup = [RecdefData.init]; 

140 

141 

6429  142 
(* outer syntax *) 
143 

6723  144 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6429  145 

146 
val recdef_decl = 

6729  147 
P.name  P.term  Scan.repeat1 (P.term  P.marg_comment)  
6723  148 
Scan.optional (P.$$$ "("  P.$$$ "congs"  P.!!! (P.xthms1  P.$$$ ")")) []  
149 
Scan.option (P.$$$ "("  P.$$$ "simpset"  P.!!! (P.name  P.$$$ ")")) 

6576  150 
>> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs); 
6429  151 

152 
val recdefP = 

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

6557  156 

157 
val defer_recdef_decl = 

6723  158 
P.name  Scan.repeat1 P.term  
159 
Scan.optional (P.$$$ "("  P.$$$ "congs"  P.!!! (P.xthms1  P.$$$ ")")) [] 

6557  160 
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs); 
161 

162 
val defer_recdefP = 

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

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

169 
end; 

170 

171 

172 
end; 