author  krauss 
Sun, 08 Sep 2013 23:28:27 +0200  
changeset 53605  462151f900ea 
parent 53603  59ef06cda7b9 
child 53606  c3f7070dd05a 
permissions  rwrr 
31775  1 
(* Title: HOL/Tools/Function/mutual.ML 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

2 
Author: Alexander Krauss, TU Muenchen 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

3 

41114  4 
Mutual recursive function definitions. 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

5 
*) 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

6 

33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset

7 
signature FUNCTION_MUTUAL = 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

8 
sig 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

9 

33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset

10 
val prepare_function_mutual : Function_Common.function_config 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

11 
> string (* defname *) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

12 
> ((string * typ) * mixfix) list 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

13 
> term list 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

14 
> local_theory 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

15 
> ((thm (* goalstate *) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

16 
* (thm > Function_Common.function_result) (* proof continuation *) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

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

18 

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

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

20 

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

21 

33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset

22 
structure Function_Mutual: FUNCTION_MUTUAL = 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

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

24 

33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset

25 
open Function_Lib 
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset

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

27 

22166  28 
type qgar = string * (string * typ) list * term list * term list * term 
29 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

30 
datatype mutual_part = MutualPart of 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

31 
{i : int, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

32 
i' : int, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

33 
fvar : string * typ, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

34 
cargTs: typ list, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

35 
f_def: term, 
22166  36 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

37 
f: term option, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

38 
f_defthm : thm option} 
22166  39 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

40 
datatype mutual_info = Mutual of 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

41 
{n : int, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

42 
n' : int, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

43 
fsum_var : string * typ, 
22166  44 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

45 
ST: typ, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

46 
RST: typ, 
22166  47 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

48 
parts: mutual_part list, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

49 
fqgars: qgar list, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

50 
qglrs: ((string * typ) list * term list * term * term) list, 
22166  51 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

52 
fsum : term option} 
22166  53 

20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

54 
fun mutual_induct_Pnames n = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

55 
if n < 5 then fst (chop n ["P","Q","R","S"]) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

56 
else map (fn i => "P" ^ string_of_int i) (1 upto n) 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

57 

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

58 
fun get_part fname = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

59 
the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

60 

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

61 
(* FIXME *) 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

62 
fun mk_prod_abs e (t1, t2) = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

63 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

64 
val bTs = rev (map snd e) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

65 
val T1 = fastype_of1 (bTs, t1) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

66 
val T2 = fastype_of1 (bTs, t2) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

67 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

68 
HOLogic.pair_const T1 T2 $ t1 $ t2 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

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

70 

22166  71 
fun analyze_eqs ctxt defname fs eqs = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

72 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

73 
val num = length fs 
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
36945
diff
changeset

74 
val fqgars = map (split_def ctxt (K true)) eqs 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

75 
val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

76 
> AList.lookup (op =) #> the 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

77 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

78 
fun curried_types (fname, fT) = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

79 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

80 
val (caTs, uaTs) = chop (arity_of fname) (binder_types fT) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

81 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

82 
(caTs, uaTs > body_type fT) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

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

84 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

85 
val (caTss, resultTs) = split_list (map curried_types fs) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

86 
val argTs = map (foldr1 HOLogic.mk_prodT) caTss 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

87 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

88 
val dresultTs = distinct (op =) resultTs 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

89 
val n' = length dresultTs 
23494  90 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

91 
val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

92 
val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

93 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

94 
val fsum_type = ST > RST 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

95 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

96 
val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

97 
val fsum_var = (fsum_var_name, fsum_type) 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

98 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

99 
fun define (fvar as (n, _)) caTs resultT i = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

100 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

101 
val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

102 
val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

103 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

104 
val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

105 
val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

106 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

107 
val rew = (n, fold_rev lambda vars f_exp) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

108 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

109 
(MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

110 
end 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

111 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

112 
val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num)) 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

113 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

114 
fun convert_eqs (f, qs, gs, args, rhs) = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

115 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

116 
val MutualPart {i, i', ...} = get_part f parts 
42497
89acb654d8eb
inlined Function_Lib.replace_frees, which is used only once
krauss
parents:
42361
diff
changeset

117 
val rhs' = rhs 
89acb654d8eb
inlined Function_Lib.replace_frees, which is used only once
krauss
parents:
42361
diff
changeset

118 
> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n)  t => t) 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

119 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

120 
(qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), 
42497
89acb654d8eb
inlined Function_Lib.replace_frees, which is used only once
krauss
parents:
42361
diff
changeset

121 
Envir.beta_norm (SumTree.mk_inj RST n' i' rhs')) 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

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

123 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

124 
val qglrs = map convert_eqs fqgars 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

125 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

126 
Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

127 
parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

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

129 

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

130 
fun define_projections fixes mutual fsum lthy = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

131 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

132 
fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

133 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

134 
val ((f, (_, f_defthm)), lthy') = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

135 
Local_Theory.define 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

136 
((Binding.name fname, mixfix), 
46909  137 
((Binding.conceal (Binding.name (Thm.def_name fname)), []), 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

138 
Term.subst_bound (fsum, f_def))) lthy 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

139 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

140 
(MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

141 
f=SOME f, f_defthm=SOME f_defthm }, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

142 
lthy') 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

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

144 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

145 
val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

146 
val (parts', lthy') = fold_map def (parts ~~ fixes) lthy 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

147 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

148 
(Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts', 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

149 
fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

150 
lthy') 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

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

152 

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

153 
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

154 
let 
42361  155 
val thy = Proof_Context.theory_of ctxt 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

156 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

157 
val oqnames = map fst pre_qs 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

158 
val (qs, _) = Variable.variant_fixes oqnames ctxt 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

159 
>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

160 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

161 
fun inst t = subst_bounds (rev qs, t) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

162 
val gs = map inst pre_gs 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

163 
val args = map inst pre_args 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

164 
val rhs = inst pre_rhs 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

165 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

166 
val cqs = map (cterm_of thy) qs 
36945  167 
val ags = map (Thm.assume o cterm_of thy) gs 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

168 

36945  169 
val import = fold Thm.forall_elim cqs 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

170 
#> fold Thm.elim_implies ags 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

171 

36945  172 
val export = fold_rev (Thm.implies_intr o cprop_of) ags 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

173 
#> fold_rev forall_intr_rename (oqnames ~~ cqs) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

174 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

175 
F ctxt (f, qs, gs, args, rhs) import export 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

176 
end 
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset

177 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

178 
fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) 
45403  179 
import (export : thm > thm) sum_psimp_eq = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

180 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

181 
val (MutualPart {f=SOME f, ...}) = get_part fname parts 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

182 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

183 
val psimp = import sum_psimp_eq 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

184 
val (simp, restore_cond) = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

185 
case cprems_of psimp of 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

186 
[] => (psimp, I) 
36945  187 
 [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) 
40317
1eac228c52b3
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
40076
diff
changeset

188 
 _ => raise General.Fail "Too many conditions" 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

189 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

190 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

191 
Goal.prove ctxt [] [] 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

192 
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) 
45403  193 
(fn _ => 
194 
Local_Defs.unfold_tac ctxt all_orig_fdefs 

195 
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset

196 
THEN (simp_tac ctxt) 1) 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

197 
> restore_cond 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

198 
> export 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

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

200 

20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

201 
fun mk_applied_form ctxt caTs thm = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

202 
let 
42361  203 
val thy = Proof_Context.theory_of ctxt 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

204 
val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

205 
in 
36945  206 
fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

207 
> Conv.fconv_rule (Thm.beta_conversion true) 
36945  208 
> fold_rev Thm.forall_intr xs 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

209 
> Thm.forall_elim_vars 0 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

210 
end 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

211 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset

212 
fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

213 
let 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset

214 
val cert = cterm_of (Proof_Context.theory_of ctxt) 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

215 
val newPs = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

216 
map2 (fn Pname => fn MutualPart {cargTs, ...} => 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

217 
Free (Pname, cargTs > HOLogic.boolT)) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

218 
(mutual_induct_Pnames (length parts)) parts 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

219 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

220 
fun mk_P (MutualPart {cargTs, ...}) P = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

221 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

222 
val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

223 
val atup = foldr1 HOLogic.mk_prod avars 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

224 
in 
39756
6c8e83d94536
consolidated tupled_lambda; moved to structure HOLogic
krauss
parents:
39276
diff
changeset

225 
HOLogic.tupled_lambda atup (list_comb (P, avars)) 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

226 
end 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

227 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

228 
val Ps = map2 mk_P parts newPs 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

229 
val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

230 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

231 
val induct_inst = 
36945  232 
Thm.forall_elim (cert case_exp) induct 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset

233 
> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset

234 
> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs) 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

235 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

236 
fun project rule (MutualPart {cargTs, i, ...}) k = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

237 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

238 
val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

239 
val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

240 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

241 
(rule 
36945  242 
> Thm.forall_elim (cert inj) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset

243 
> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt) 
36945  244 
> fold_rev (Thm.forall_intr o cert) (afs @ newPs), 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

245 
k + length cargTs) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

246 
end 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

247 
in 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

248 
fst (fold_map (project induct_inst) parts 0) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

249 
end 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

250 

22623  251 
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

252 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

253 
val result = inner_cont proof 
41846
b368a7aee46a
removed support for tailrecursion from function package (now implemented by partial_function)
krauss
parents:
41114
diff
changeset

254 
val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], 
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

255 
termination, domintros, dom, pelims, ...} = result 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

256 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

257 
val (all_f_defs, fs) = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

258 
map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => 
36945  259 
(mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

260 
parts 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

261 
> split_list 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

262 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

263 
val all_orig_fdefs = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

264 
map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

265 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

266 
fun mk_mpsimp fqgar sum_psimp = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

267 
in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp 
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset

268 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset

269 
val rew_simpset = put_simpset HOL_basic_ss lthy addsimps all_f_defs 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

270 
val mpsimps = map2 mk_mpsimp fqgars psimps 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

271 
val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset

272 
val mtermination = full_simplify rew_simpset termination 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset

273 
val mdomintros = Option.map (map (full_simplify rew_simpset)) domintros 
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

274 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

275 
in 
52384  276 
FunctionResult { fs=fs, G=G, R=R, dom=dom, 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

277 
psimps=mpsimps, simple_pinducts=minducts, 
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

278 
cases=cases, pelims=pelims, termination=mtermination, 
41846
b368a7aee46a
removed support for tailrecursion from function package (now implemented by partial_function)
krauss
parents:
41114
diff
changeset

279 
domintros=mdomintros} 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

280 
end 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

281 

53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

282 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

283 
fun postprocess_cases_rules ctxt cont proof = 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

284 
let val result = cont proof; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

285 
val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases, pelims, 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

286 
termination, domintros, ...} = result; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

287 
val n_fs = length fs; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

288 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

289 
fun postprocess_cases_rule (idx,f) = 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

290 
let fun dest_funprop (Const ("HOL.eq", _) $ lhs $ rhs) = (strip_comb lhs, rhs) 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

291 
 dest_funprop (Const ("HOL.Not", _) $ trm) = (strip_comb trm, @{term "False"}) 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

292 
 dest_funprop trm = (strip_comb trm, @{term "True"}); 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

293 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

294 
fun mk_fun_args 0 _ acc_vars = rev acc_vars 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

295 
 mk_fun_args n (Type("fun",[S,T])) acc_vars = 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

296 
let val xn = Free ("x" ^ Int.toString n,S) in 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

297 
mk_fun_args (n  1) T (xn :: acc_vars) 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

298 
end 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

299 
 mk_fun_args _ _ _ = raise (TERM ("Not a function.", [f])) 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

300 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

301 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

302 
val f_simps = filter (fn r => (prop_of r > Logic.strip_assums_concl 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

303 
> HOLogic.dest_Trueprop 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

304 
> dest_funprop > fst > fst) = f) 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

305 
psimps 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

306 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

307 
val arity = hd f_simps > prop_of > Logic.strip_assums_concl 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

308 
> HOLogic.dest_Trueprop 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

309 
> snd o fst o dest_funprop > length; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

310 
val arg_vars = mk_fun_args arity (fastype_of f) [] 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

311 
val argsT = fastype_of (HOLogic.mk_tuple arg_vars); 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

312 
val args = Free ("x", argsT); 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

313 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

314 
val thy = Proof_Context.theory_of ctxt; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

315 
val domT = R > dest_Free > snd > hd o snd o dest_Type 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

316 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

317 
val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

318 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

319 
val sum_elims = @{thms HOL.notE[OF Sum_Type.sum.distinct(1)] 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

320 
HOL.notE[OF Sum_Type.sum.distinct(2)]}; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

321 
fun prep_subgoal i = 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

322 
REPEAT (eresolve_tac @{thms Pair_inject Inl_inject[elim_format] 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

323 
Inr_inject[elim_format]} i) 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

324 
THEN REPEAT (Tactic.eresolve_tac sum_elims i); 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

325 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

326 
val tac = ALLGOALS prep_subgoal; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

327 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

328 
in 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

329 
hd cases 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

330 
> Thm.forall_elim @{cterm "P::bool"} 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

331 
> Thm.forall_elim (cterm_of thy sumtree_inj) 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

332 
> Tactic.rule_by_tactic ctxt tac 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

333 
> Thm.forall_intr (cterm_of thy args) 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

334 
> Thm.forall_intr @{cterm "P::bool"} 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

335 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

336 
end; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

337 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

338 
val cases' = map_index postprocess_cases_rule fs; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

339 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

340 
in 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

341 
FunctionResult {fs=fs, G=G, R=R, dom=dom, psimps=psimps, 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

342 
simple_pinducts=simple_pinducts, 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

343 
cases=cases', pelims=pelims, termination=termination, 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

344 
domintros=domintros} 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

345 
end; 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

346 

59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

347 

33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset

348 
fun prepare_function_mutual config defname fixes eqss lthy = 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

349 
let 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

350 
val mutual as Mutual {fsum_var=(n, T), qglrs, ...} = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

351 
analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

352 

36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

353 
val ((fsum, goalstate, cont), lthy') = 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

354 
Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy 
22166  355 

34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

356 
val (mutual', lthy'') = define_projections fixes mutual fsum lthy' 
22166  357 

53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

358 
val cont' = mk_partial_rules_mutual lthy'' cont mutual' 
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

359 
val cont'' = postprocess_cases_rules lthy'' cont' 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

360 
in 
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset

361 
((goalstate, cont''), lthy'') 
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

362 
end 
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset

363 

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

364 
end 