equal
deleted
inserted
replaced
6 header {* TFL: recursive function definitions *} |
6 header {* TFL: recursive function definitions *} |
7 |
7 |
8 theory Recdef |
8 theory Recdef |
9 imports Wellfounded_Relations FunDef |
9 imports Wellfounded_Relations FunDef |
10 uses |
10 uses |
11 ("../TFL/casesplit.ML") |
11 ("Tools/TFL/casesplit.ML") |
12 ("../TFL/utils.ML") |
12 ("Tools/TFL/utils.ML") |
13 ("../TFL/usyntax.ML") |
13 ("Tools/TFL/usyntax.ML") |
14 ("../TFL/dcterm.ML") |
14 ("Tools/TFL/dcterm.ML") |
15 ("../TFL/thms.ML") |
15 ("Tools/TFL/thms.ML") |
16 ("../TFL/rules.ML") |
16 ("Tools/TFL/rules.ML") |
17 ("../TFL/thry.ML") |
17 ("Tools/TFL/thry.ML") |
18 ("../TFL/tfl.ML") |
18 ("Tools/TFL/tfl.ML") |
19 ("../TFL/post.ML") |
19 ("Tools/TFL/post.ML") |
20 ("Tools/recdef_package.ML") |
20 ("Tools/recdef_package.ML") |
21 begin |
21 begin |
22 |
22 |
23 lemma tfl_eq_True: "(x = True) --> x" |
23 lemma tfl_eq_True: "(x = True) --> x" |
24 by blast |
24 by blast |
42 by blast |
42 by blast |
43 |
43 |
44 lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q" |
44 lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q" |
45 by blast |
45 by blast |
46 |
46 |
47 use "../TFL/casesplit.ML" |
47 use "Tools/TFL/casesplit.ML" |
48 use "../TFL/utils.ML" |
48 use "Tools/TFL/utils.ML" |
49 use "../TFL/usyntax.ML" |
49 use "Tools/TFL/usyntax.ML" |
50 use "../TFL/dcterm.ML" |
50 use "Tools/TFL/dcterm.ML" |
51 use "../TFL/thms.ML" |
51 use "Tools/TFL/thms.ML" |
52 use "../TFL/rules.ML" |
52 use "Tools/TFL/rules.ML" |
53 use "../TFL/thry.ML" |
53 use "Tools/TFL/thry.ML" |
54 use "../TFL/tfl.ML" |
54 use "Tools/TFL/tfl.ML" |
55 use "../TFL/post.ML" |
55 use "Tools/TFL/post.ML" |
56 use "Tools/recdef_package.ML" |
56 use "Tools/recdef_package.ML" |
57 setup RecdefPackage.setup |
57 setup RecdefPackage.setup |
58 |
58 |
59 lemmas [recdef_simp] = |
59 lemmas [recdef_simp] = |
60 inv_image_def |
60 inv_image_def |
61 measure_def |
61 measure_def |
62 lex_prod_def |
62 lex_prod_def |
63 same_fst_def |
63 same_fst_def |
64 less_Suc_eq [THEN iffD2] |
64 less_Suc_eq [THEN iffD2] |
65 |
65 |
66 lemmas [recdef_cong] = |
66 lemmas [recdef_cong] = |
67 if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong |
67 if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong |
68 |
68 |
69 lemmas [recdef_wf] = |
69 lemmas [recdef_wf] = |
70 wf_trancl |
70 wf_trancl |
71 wf_less_than |
71 wf_less_than |