author  krauss 
Tue, 07 Aug 2007 17:01:35 +0200  
changeset 24171  25381ce95316 
parent 24170  33f055a0f3a1 
child 24977  9f98751c9628 
permissions  rwrr 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

1 
(* Title: HOL/Tools/function_package/mutual.ML 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

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

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

4 

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

5 
A package for general recursive function definitions. 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

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

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

8 

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

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

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

11 

22166  12 
val prepare_fundef_mutual : FundefCommon.fundef_config 
13 
> string (* defname *) 

14 
> ((string * typ) * mixfix) list 

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

15 
> term list 
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

16 
> local_theory 
22166  17 
> ((thm (* goalstate *) 
18 
* (thm > FundefCommon.fundef_result) (* proof continuation *) 

19 
) * local_theory) 

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

20 

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

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

22 

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

23 

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

24 
structure FundefMutual: FUNDEF_MUTUAL = 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

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

26 

21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20949
diff
changeset

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

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

29 

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

30 
(* Theory dependencies *) 
22622
25693088396b
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
krauss
parents:
22620
diff
changeset

31 
val sum_case_rules = thms "Sum_Type.sum_cases" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

32 
val split_apply = thm "Product_Type.split" 
23494  33 
val projl_inl = thm "Sum_Type.Projl_Inl" 
34 
val projr_inr = thm "Sum_Type.Projr_Inr" 

35 

23528  36 
(* topdown access in balanced tree *) 
37 
fun access_top_down {left, right, init} len i = 

38 
BalancedTree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init 

23494  39 

40 
(* Sum types *) 

41 
fun mk_sumT LT RT = Type ("+", [LT, RT]) 

42 
fun mk_sumcase TL TR T l r = Const (@{const_name "Sum_Type.sum_case"}, (TL > T) > (TR > T) > mk_sumT TL TR > T) $ l $ r 

43 

44 
val App = curry op $ 

45 

46 
fun mk_inj ST n i = 

23528  47 
access_top_down 
23494  48 
{ init = (ST, I : term > term), 
23528  49 
left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name "Inl"}, LT > T)))), 
50 
right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name "Inr"}, RT > T))))} n i 

23494  51 
> snd 
52 

53 
fun mk_proj ST n i = 

23528  54 
access_top_down 
23494  55 
{ init = (ST, I : term > term), 
23528  56 
left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name "Projl"}, T > LT)) o proj)), 
57 
right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name "Projr"}, T > RT)) o proj))} n i 

23494  58 
> snd 
59 

60 
fun mk_sumcases T fs = 

61 
BalancedTree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 

62 
(map (fn f => (f, domain_type (fastype_of f))) fs) 

63 
> fst 

64 

65 

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

66 

22166  67 
type qgar = string * (string * typ) list * term list * term list * term 
68 

23217  69 
fun name_of_fqgar ((f, _, _, _, _): qgar) = f 
22166  70 

71 
datatype mutual_part = 

72 
MutualPart of 

73 
{ 

23494  74 
i : int, 
75 
i' : int, 

22166  76 
fvar : string * typ, 
77 
cargTs: typ list, 

78 
f_def: term, 

79 

80 
f: term option, 

81 
f_defthm : thm option 

82 
} 

83 

84 

85 
datatype mutual_info = 

86 
Mutual of 

87 
{ 

23494  88 
n : int, 
89 
n' : int, 

22166  90 
fsum_var : string * typ, 
91 

92 
ST: typ, 

93 
RST: typ, 

94 

95 
parts: mutual_part list, 

96 
fqgars: qgar list, 

97 
qglrs: ((string * typ) list * term list * term * term) list, 

98 

99 
fsum : term option 

100 
} 

101 

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

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

103 
if n < 5 then fst (chop n ["P","Q","R","S"]) 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

104 
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

105 

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

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

107 
the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname) 
21237  108 

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

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

110 
fun mk_prod_abs e (t1, t2) = 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

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

112 
val bTs = rev (map snd e) 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

113 
val T1 = fastype_of1 (bTs, t1) 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

114 
val T2 = fastype_of1 (bTs, t2) 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

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

116 
HOLogic.pair_const T1 T2 $ t1 $ t2 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

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

118 

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

119 

22166  120 
fun analyze_eqs ctxt defname fs eqs = 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

121 
let 
23494  122 
val num = length fs 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

123 
val fnames = map fst fs 
24170  124 
val fqgars = map (split_def ctxt) eqs 
23189  125 
val arities = mk_arities fqgars 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

126 

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

127 
fun curried_types (fname, fT) = 
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

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

129 
val k = the_default 1 (Symtab.lookup arities fname) 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

130 
val (caTs, uaTs) = chop k (binder_types fT) 
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

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

132 
(caTs, uaTs > body_type fT) 
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

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

134 

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

135 
val (caTss, resultTs) = split_list (map curried_types fs) 
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

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

137 

23494  138 
val dresultTs = distinct (Type.eq_type Vartab.empty) resultTs 
139 
val n' = length dresultTs 

140 

141 
val RST = BalancedTree.make (uncurry mk_sumT) dresultTs 

142 
val ST = BalancedTree.make (uncurry mk_sumT) argTs 

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

143 

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

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

145 

22166  146 
val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

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

148 

23494  149 
fun define (fvar as (n, T)) caTs resultT i = 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

150 
let 
23494  151 
val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) 
152 
val i' = find_index (fn Ta => Type.eq_type Vartab.empty (Ta, resultT)) dresultTs + 1 

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

153 

23494  154 
val f_exp = mk_proj RST n' i' (Free fsum_var $ mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

155 
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

156 

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

157 
val rew = (n, fold_rev lambda vars f_exp) 
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

158 
in 
23494  159 
(MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew) 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

160 
end 
21237  161 

23494  162 
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

163 

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

164 
fun convert_eqs (f, qs, gs, args, rhs) = 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

165 
let 
23494  166 
val MutualPart {i, i', ...} = get_part f parts 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

167 
in 
23494  168 
(qs, gs, mk_inj ST num i (foldr1 (mk_prod_abs qs) args), 
169 
mk_inj RST n' i' (replace_frees rews rhs) 

170 
> Envir.beta_norm) 

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

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

172 

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

173 
val qglrs = map convert_eqs fqgars 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

174 
in 
23494  175 
Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

176 
parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

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

178 

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

179 

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

180 

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

181 

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

182 
fun define_projections fixes mutual fsum lthy = 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

183 
let 
23494  184 
fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

185 
let 
21436  186 
val ((f, (_, f_defthm)), lthy') = 
187 
LocalTheory.def Thm.internalK ((fname, mixfix), 

188 
((fname ^ "_def", []), Term.subst_bound (fsum, f_def))) 

189 
lthy 

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

190 
in 
23494  191 
(MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, 
21237  192 
f=SOME f, f_defthm=SOME f_defthm }, 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

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

194 
end 
21237  195 

23494  196 
val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

197 
val (parts', lthy') = fold_map def (parts ~~ fixes) lthy 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

198 
in 
23494  199 
(Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts', 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

200 
fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

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

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

203 

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

204 

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

205 
fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm 
21237  206 

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

207 
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

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

209 
val thy = ProofContext.theory_of ctxt 
21237  210 

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

211 
val oqnames = map fst pre_qs 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20654
diff
changeset

212 
val (qs, ctxt') = Variable.variant_fixes oqnames ctxt 
21237  213 
>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs 
214 

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

215 
fun inst t = subst_bounds (rev qs, t) 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

216 
val gs = map inst pre_gs 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

217 
val args = map inst pre_args 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

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

219 

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

220 
val cqs = map (cterm_of thy) qs 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

221 
val ags = map (assume o cterm_of thy) gs 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

222 

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

223 
val import = fold forall_elim cqs 
23494  224 
#> fold (flip implies_elim) ags 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

225 

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

226 
val export = fold_rev (implies_intr o cprop_of) ags 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

227 
#> fold_rev forall_intr_rename (oqnames ~~ cqs) 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

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

229 
F ctxt (f, qs, gs, args, rhs) import export 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

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

231 

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

232 
fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm > thm) sum_psimp_eq = 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

233 
let 
23494  234 
val (MutualPart {f=SOME f, f_defthm=SOME f_def, ...}) = get_part fname parts 
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset

235 

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

236 
val psimp = import sum_psimp_eq 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

237 
val (simp, restore_cond) = case cprems_of psimp of 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

238 
[] => (psimp, I) 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

239 
 [cond] => (implies_elim psimp (assume cond), implies_intr cond) 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

240 
 _ => sys_error "Too many conditions" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

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

242 
Goal.prove ctxt [] [] 
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset

243 
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) 
24171
25381ce95316
Issue a warning, when "function" encounters variables occuring in function position,
krauss
parents:
24170
diff
changeset

244 
(fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs) 
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset

245 
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 
23494  246 
THEN SIMPSET' (fn ss => simp_tac (ss addsimps [projl_inl, projr_inr])) 1) 
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset

247 
> restore_cond 
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset

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

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

250 

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

251 

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

252 
(* FIXME HACK *) 
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset

253 
fun mk_applied_form ctxt caTs thm = 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

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

255 
val thy = ProofContext.theory_of ctxt 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

256 
val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

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

258 
fold (fn x => fn thm => combination thm (reflexive x)) xs thm 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

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

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

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

262 
end 
23494  263 

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

264 

23494  265 
fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, RST, parts, ...}) = 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

266 
let 
22623  267 
val cert = cterm_of (ProofContext.theory_of lthy) 
20949  268 
val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
21237  269 
Free (Pname, cargTs > HOLogic.boolT)) 
20949  270 
(mutual_induct_Pnames (length parts)) 
271 
parts 

21237  272 

273 
fun mk_P (MutualPart {cargTs, ...}) P = 

274 
let 

275 
val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs 

276 
val atup = foldr1 HOLogic.mk_prod avars 

277 
in 

278 
tupled_lambda atup (list_comb (P, avars)) 

279 
end 

280 

281 
val Ps = map2 mk_P parts newPs 

23494  282 
val case_exp = mk_sumcases HOLogic.boolT Ps 
21237  283 

284 
val induct_inst = 

22623  285 
forall_elim (cert case_exp) induct 
21237  286 
> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules)) 
287 
> full_simplify (HOL_basic_ss addsimps all_f_defs) 

288 

23494  289 
fun project rule (MutualPart {cargTs, i, ...}) = 
21237  290 
let 
23494  291 
val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int j, T)) cargTs 
292 
val inj = mk_inj ST n i (foldr1 HOLogic.mk_prod afs) 

21237  293 
in 
294 
rule 

22623  295 
> forall_elim (cert inj) 
21237  296 
> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules)) 
22623  297 
> fold_rev (forall_intr o cert) (afs @ newPs) 
21237  298 
end 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

299 
in 
23494  300 
map (project induct_inst) parts 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

301 
end 
21237  302 

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

303 

22623  304 
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset

305 
let 
22166  306 
val result = inner_cont proof 
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

307 
val FundefResult {fs=[f], G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct], 
22166  308 
termination,domintros} = result 
21237  309 

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

310 
val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

311 
(mk_applied_form lthy cargTs (symmetric f_def), f)) 
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset

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

313 
> split_list 
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset

314 

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

315 
val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts 
21237  316 

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

317 
fun mk_mpsimp fqgar sum_psimp = 
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset

318 
in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp 
21237  319 

23189  320 
val rew_ss = HOL_basic_ss addsimps all_f_defs 
22166  321 
val mpsimps = map2 mk_mpsimp fqgars psimps 
322 
val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps 

22623  323 
val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m 
23189  324 
val mtermination = full_simplify rew_ss termination 
325 
val mdomintros = map_option (map (full_simplify rew_ss)) domintros 

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

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

327 
FundefResult { fs=fs, G=G, R=R, 
22623  328 
psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts, 
329 
cases=cases, termination=mtermination, 

23189  330 
domintros=mdomintros, 
22623  331 
trsimps=mtrsimps} 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset

332 
end 
21237  333 

23189  334 
fun prepare_fundef_mutual config defname fixes eqss lthy = 
22166  335 
let 
22323
b8c227d8ca91
beta_eta_contract specification befor processing. These normal forms avoid unpleasant surprises later on.
krauss
parents:
22244
diff
changeset

336 
val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) 
22166  337 
val Mutual {fsum_var=(n, T), qglrs, ...} = mutual 
338 

339 
val ((fsum, goalstate, cont), lthy') = 

23189  340 
FundefCore.prepare_fundef config defname [((n, T), NoSyn)] qglrs lthy 
22166  341 

342 
val (mutual', lthy'') = define_projections fixes mutual fsum lthy' 

343 

344 
val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual' 

345 
in 

23819  346 
((goalstate, mutual_cont), lthy'') 
22166  347 
end 
348 

21237  349 

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

350 
end 