equal
deleted
inserted
replaced
5 TFL: recursive function definitions. |
5 TFL: recursive function definitions. |
6 *) |
6 *) |
7 |
7 |
8 theory Recdef = WF_Rel + Datatype |
8 theory Recdef = WF_Rel + Datatype |
9 files |
9 files |
10 (*establish a base of common and/or helpful functions*) |
|
11 "../TFL/utils.sig" |
|
12 |
|
13 "../TFL/usyntax.sig" |
|
14 "../TFL/rules.sig" |
|
15 "../TFL/thry.sig" |
|
16 "../TFL/thms.sig" |
|
17 "../TFL/tfl.sig" |
|
18 "../TFL/utils.sml" |
10 "../TFL/utils.sml" |
19 |
|
20 (*supply implementations*) |
|
21 "../TFL/usyntax.sml" |
11 "../TFL/usyntax.sml" |
22 "../TFL/thms.sml" |
12 "../TFL/thms.sml" |
23 "../TFL/dcterm.sml" |
13 "../TFL/dcterm.sml" |
24 "../TFL/rules.sml" |
14 "../TFL/rules.sml" |
25 "../TFL/thry.sml" |
15 "../TFL/thry.sml" |
26 |
|
27 (*link system and specialize for Isabelle*) |
|
28 "../TFL/tfl.sml" |
16 "../TFL/tfl.sml" |
29 "../TFL/post.sml" |
17 "../TFL/post.sml" |
30 |
|
31 (*theory extender wrapper module*) |
|
32 "Tools/recdef_package.ML": |
18 "Tools/recdef_package.ML": |
33 |
19 |
34 setup RecdefPackage.setup |
20 setup RecdefPackage.setup |
35 |
21 |
|
22 lemmas [recdef_simp] = |
|
23 inv_image_def |
|
24 measure_def |
|
25 lex_prod_def |
|
26 less_Suc_eq [THEN iffD2] |
|
27 |
|
28 lemmas [recdef_cong] = |
|
29 if_cong |
|
30 |
|
31 lemma let_cong [recdef_cong]: |
|
32 "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g" |
|
33 by (unfold Let_def) blast |
|
34 |
|
35 lemmas [recdef_wf] = |
|
36 wf_trancl |
|
37 wf_less_than |
|
38 wf_lex_prod |
|
39 wf_inv_image |
|
40 wf_measure |
|
41 wf_pred_nat |
|
42 wf_empty |
|
43 |
36 end |
44 end |