author  krauss 
Tue, 07 Aug 2007 17:01:35 +0200  
changeset 24171  25381ce95316 
parent 24170  33f055a0f3a1 
child 24920  2a45e400fdad 
permissions  rwrr 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

1 
(* Title: HOL/Tools/function_package/fundef_common.ML 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

2 
ID: $Id$ 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

3 
Author: Alexander Krauss, TU Muenchen 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

4 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

5 
A package for general recursive function definitions. 
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

6 
Common definitions and other infrastructure. 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

7 
*) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

8 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

9 
structure FundefCommon = 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

10 
struct 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

11 

23215  12 
local open FundefLib in 
13 

22498
62cdd4b3e96b
made function syntax strict, requiring  to separate equations; cleanup
krauss
parents:
22279
diff
changeset

14 
(* Profiling *) 
21255
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

15 
val profile = ref false; 
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

16 

617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

17 
fun PROFILE msg = if !profile then timeap_msg msg else I 
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

18 

22498
62cdd4b3e96b
made function syntax strict, requiring  to separate equations; cleanup
krauss
parents:
22279
diff
changeset

19 

23766  20 
val acc_const_name = "Accessible_Part.accp" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset

21 
fun mk_acc domT R = 
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

22 
Const (acc_const_name, (domT > domT > HOLogic.boolT) > domT > HOLogic.boolT) $ R 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

23 

21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset

24 
val function_name = suffix "C" 
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset

25 
val graph_name = suffix "_graph" 
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset

26 
val rel_name = suffix "_rel" 
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset

27 
val dom_name = suffix "_dom" 
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset

28 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

29 

19583
c5fa77b03442
functionpackage: Changed record usage to make sml/nj happy...
krauss
parents:
19564
diff
changeset

30 
datatype fundef_result = 
c5fa77b03442
functionpackage: Changed record usage to make sml/nj happy...
krauss
parents:
19564
diff
changeset

31 
FundefResult of 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

32 
{ 
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

33 
fs: term list, 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset

34 
G: term, 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset

35 
R: term, 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

36 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset

37 
psimps : thm list, 
22166  38 
trsimps : thm list option, 
39 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

40 
subset_pinducts : thm list, 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

41 
simple_pinducts : thm list, 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

42 
cases : thm, 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

43 
termination : thm, 
22166  44 
domintros : thm list option 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

45 
} 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

46 

22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

47 

21255
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

48 
datatype fundef_context_data = 
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

49 
FundefCtxData of 
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

50 
{ 
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

51 
defname : string, 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

52 

23819  53 
(* contains no logical entities: invariant under morphisms *) 
22166  54 
add_simps : string > Attrib.src list > thm list > local_theory > thm list * local_theory, 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

55 

22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

56 
fs : term list, 
21255
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

57 
R : term, 
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

58 

617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

59 
psimps: thm list, 
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

60 
pinducts: thm list, 
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

61 
termination: thm 
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

62 
} 
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset

63 

22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

64 
fun morph_fundef_data phi (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) = 
22623  65 
let 
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

66 
val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

67 
val name = Morphism.name phi 
22623  68 
in 
23819  69 
FundefCtxData { add_simps = add_simps, 
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

70 
fs = map term fs, R = term R, psimps = fact psimps, 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

71 
pinducts = fact pinducts, termination = thm termination, 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

72 
defname = name defname } 
22623  73 
end 
74 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset

75 
structure FundefData = GenericDataFun 
22846  76 
( 
77 
type T = (term * fundef_context_data) NetRules.T; 

22760  78 
val empty = NetRules.init 
79 
(op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) > bool) 

80 
fst; 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

81 
val copy = I; 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

82 
val extend = I; 
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

83 
fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2) 
22846  84 
); 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

85 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

86 

22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

87 
(* Generally useful?? *) 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

88 
fun lift_morphism thy f = 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

89 
let 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

90 
val term = Drule.term_rule thy f 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

91 
in 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

92 
Morphism.thm_morphism f $> Morphism.term_morphism term $> Morphism.typ_morphism (Logic.type_map term) 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

93 
end 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

94 

0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

95 
fun import_fundef_data t ctxt = 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

96 
let 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

97 
val thy = Context.theory_of ctxt 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

98 
val ct = cterm_of thy t 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

99 
val inst_morph = lift_morphism thy o Thm.instantiate 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

100 

22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

101 
fun match data = 
22903  102 
SOME (morph_fundef_data (inst_morph (Thm.match (cterm_of thy (fst data), ct))) (snd data)) 
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

103 
handle Pattern.MATCH => NONE 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

104 
in 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

105 
get_first match (NetRules.retrieve (FundefData.get ctxt) t) 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

106 
end 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

107 

22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

108 
fun import_last_fundef ctxt = 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

109 
case NetRules.rules (FundefData.get ctxt) of 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

110 
[] => NONE 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

111 
 (t, data) :: _ => 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

112 
let 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

113 
val ([t'], ctxt') = Variable.import_terms true [t] (Context.proof_of ctxt) 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

114 
in 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

115 
import_fundef_data t' (Context.Proof ctxt') 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

116 
end 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

117 

22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

118 
val all_fundef_data = NetRules.rules o FundefData.get 
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset

119 

22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

120 
structure TerminationRule = GenericDataFun 
22846  121 
( 
122 
type T = thm list 

123 
val empty = [] 

124 
val extend = I 

24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23819
diff
changeset

125 
fun merge _ = Thm.merge_thms 
22846  126 
); 
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset

127 

22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

128 
val get_termination_rules = TerminationRule.get 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

129 
val store_termination_rule = TerminationRule.map o cons 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

130 
val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

131 

0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

132 
fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) = 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

133 
FundefData.map (fold (fn f => NetRules.insert (f, data)) fs) 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

134 
#> store_termination_rule termination 
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset

135 

20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

136 
(* Configuration management *) 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

137 
datatype fundef_opt 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

138 
= Sequential 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

139 
 Default of string 
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20874
diff
changeset

140 
 Target of xstring 
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset

141 
 DomIntros 
22166  142 
 Tailrec 
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

143 

d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

144 
datatype fundef_config 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

145 
= FundefConfig of 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

146 
{ 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

147 
sequential: bool, 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

148 
default: string, 
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset

149 
target: xstring option, 
22166  150 
domintros: bool, 
151 
tailrec: bool 

20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

152 
} 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

153 

23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

154 
fun apply_opt Sequential (FundefConfig {sequential, default, target, domintros,tailrec}) = 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

155 
FundefConfig {sequential=true, default=default, target=target, domintros=domintros, tailrec=tailrec} 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

156 
 apply_opt (Default d) (FundefConfig {sequential, default, target, domintros,tailrec}) = 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

157 
FundefConfig {sequential=sequential, default=d, target=target, domintros=domintros, tailrec=tailrec} 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

158 
 apply_opt (Target t) (FundefConfig {sequential, default, target, domintros,tailrec}) = 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

159 
FundefConfig {sequential=sequential, default=default, target=SOME t, domintros=domintros, tailrec=tailrec} 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

160 
 apply_opt DomIntros (FundefConfig {sequential, default, target, domintros,tailrec}) = 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

161 
FundefConfig {sequential=sequential, default=default, target=target, domintros=true,tailrec=tailrec} 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

162 
 apply_opt Tailrec (FundefConfig {sequential, default, target, domintros,tailrec}) = 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

163 
FundefConfig {sequential=sequential, default=default, target=target, domintros=domintros,tailrec=true} 
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset

164 

22498
62cdd4b3e96b
made function syntax strict, requiring  to separate equations; cleanup
krauss
parents:
22279
diff
changeset

165 
fun target_of (FundefConfig {target, ...}) = target 
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20874
diff
changeset

166 

23819  167 
val default_config = FundefConfig { sequential=false, default="%x. arbitrary", 
168 
target=NONE, domintros=false, tailrec=false } 

169 

170 

23189  171 
(* Common operations on equations *) 
172 

173 
fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b) 

174 
 open_all_all t = ([], t) 

175 

24170  176 
fun split_def ctxt geq = 
23189  177 
let 
24170  178 
fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq] 
23189  179 
val (qs, imp) = open_all_all geq 
180 

181 
val gs = Logic.strip_imp_prems imp 

182 
val eq = Logic.strip_imp_concl imp 

183 

184 
val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) 

24170  185 
handle TERM _ => error (input_error "Not an equation") 
23189  186 

187 
val (head, args) = strip_comb f_args 

188 

189 
val fname = fst (dest_Free head) 

24170  190 
handle TERM _ => error (input_error "Head symbol must not be a bound variable") 
23189  191 
in 
192 
(fname, qs, gs, args, rhs) 

193 
end 

194 

195 
exception ArgumentCount of string 

196 

197 
fun mk_arities fqgars = 

198 
let fun f (fname, _, _, args, _) arities = 

199 
let val k = length args 

200 
in 

201 
case Symtab.lookup arities fname of 

202 
NONE => Symtab.update (fname, k) arities 

203 
 SOME i => (if i = k then arities else raise ArgumentCount fname) 

204 
end 

205 
in 

206 
fold f fqgars Symtab.empty 

207 
end 

208 

209 

23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

210 
(* Check for all sorts of errors in the input *) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

211 
fun check_defs ctxt fixes eqs = 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

212 
let 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

213 
val fnames = map (fst o fst) fixes 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

214 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

215 
fun check geq = 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

216 
let 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

217 
fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq] 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

218 

24170  219 
val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq 
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

220 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

221 
val _ = fname mem fnames 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

222 
orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

223 
^ commas_quote fnames)) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

224 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

225 
fun add_bvs t is = add_loose_bnos (t, 0, is) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

226 
val rvs = (add_bvs rhs [] \\ fold add_bvs args []) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

227 
> map (fst o nth (rev qs)) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

228 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

229 
val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

230 
^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

231 

23819  232 
val _ = forall (not o Term.exists_subterm (fn Free (n, _) => n mem fnames  _ => false)) gs 
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

233 
orelse error (input_error "Recursive Calls not allowed in premises") 
24171
25381ce95316
Issue a warning, when "function" encounters variables occuring in function position,
krauss
parents:
24170
diff
changeset

234 

25381ce95316
Issue a warning, when "function" encounters variables occuring in function position,
krauss
parents:
24170
diff
changeset

235 
val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args 
25381ce95316
Issue a warning, when "function" encounters variables occuring in function position,
krauss
parents:
24170
diff
changeset

236 
val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q'  _ => false)) freeargs) qs 
25381ce95316
Issue a warning, when "function" encounters variables occuring in function position,
krauss
parents:
24170
diff
changeset

237 
val _ = null funvars 
25381ce95316
Issue a warning, when "function" encounters variables occuring in function position,
krauss
parents:
24170
diff
changeset

238 
orelse (warning (cat_lines ["Bound variable" ^ plural " " "s " funvars ^ commas_quote (map fst funvars) ^ 
25381ce95316
Issue a warning, when "function" encounters variables occuring in function position,
krauss
parents:
24170
diff
changeset

239 
" occur" ^ plural "s" "" funvars ^ " in function position.", 
25381ce95316
Issue a warning, when "function" encounters variables occuring in function position,
krauss
parents:
24170
diff
changeset

240 
"Misspelled constructor???"]); true) 
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

241 
in 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

242 
fqgar 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

243 
end 
24170  244 

245 
fun check_sorts ((fname, fT), _) = 

246 
Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) 

247 
orelse error ("Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ".") 

248 

249 
val _ = map check_sorts fixes 

23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

250 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

251 
val _ = mk_arities (map check eqs) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

252 
handle ArgumentCount fname => 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

253 
error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations") 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

254 
in 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

255 
() 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

256 
end 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

257 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

258 
(* Preprocessors *) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

259 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

260 
type fixes = ((string * typ) * mixfix) list 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

261 
type 'a spec = ((bstring * Attrib.src list) * 'a list) list 
23819  262 
type preproc = fundef_config > bool list > Proof.context > fixes > term spec 
263 
> (term list * (thm list > thm spec) * (thm list > thm list list)) 

264 

265 
val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all 

23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

266 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

267 
fun empty_preproc check _ _ ctxt fixes spec = 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

268 
let 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

269 
val (nas,tss) = split_list spec 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

270 
val _ = check ctxt fixes (flat tss) 
23819  271 
val ts = flat tss 
272 
val fnames = map (fst o fst) fixes 

273 
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts 

274 

275 
fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames  1) (indices ~~ xs) 

276 
> map (map snd) 

23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

277 
in 
23819  278 
(ts, curry op ~~ nas o Library.unflat tss, sort) 
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

279 
end 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

280 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

281 
structure Preprocessor = GenericDataFun 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

282 
( 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

283 
type T = preproc 
23206  284 
val empty : T = empty_preproc check_defs 
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

285 
val extend = I 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

286 
fun merge _ (a, _) = a 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

287 
); 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

288 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

289 
val get_preproc = Preprocessor.get o Context.Proof 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

290 
val set_preproc = Preprocessor.map o K 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

291 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

292 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

293 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

294 
local 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

295 
structure P = OuterParse and K = OuterKeyword 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

296 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

297 
val opt_sequential = Scan.optional ((P.$$$ "("  P.$$$ "sequential"  P.$$$ ")") >> K true) false 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

298 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

299 
val option_parser = (P.$$$ "sequential" >> K Sequential) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

300 
 ((P.reserved "default"  P.term) >> Default) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

301 
 (P.reserved "domintros" >> K DomIntros) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

302 
 (P.reserved "tailrec" >> K Tailrec) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

303 
 ((P.$$$ "in"  P.xname) >> Target) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

304 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

305 
fun config_parser default = (Scan.optional (P.$$$ "("  P.!!! (P.list1 (P.group "option" option_parser))  P.$$$ ")") []) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

306 
>> (fn opts => fold apply_opt opts default) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

307 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

308 
val otherwise = P.$$$ "("  P.$$$ "otherwise"  P.$$$ ")" 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

309 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

310 
fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "", quote t]))) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

311 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

312 
val statement_ow = SpecParse.opt_thm_name ":"  (P.prop  Scan.optional (otherwise >> K true) false) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

313 
 Scan.ahead ((P.term : pipe_error)  Scan.succeed ("","")) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

314 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

315 
val statements_ow = P.enum1 "" statement_ow 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

316 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

317 
val flags_statements = statements_ow 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

318 
>> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow)) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

319 
in 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

320 
fun fundef_parser default_cfg = (config_parser default_cfg  P.fixes  P.$$$ "where"  flags_statements) 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

321 
end 
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

322 

a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset

323 

23215  324 
end 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

325 
end 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

326 