author | wenzelm |
Wed, 06 Dec 2006 01:12:43 +0100 | |
changeset 21672 | 29c346b165d4 |
parent 19770 | be5c23ebe1eb |
child 22264 | 6a65e9b2ae05 |
permissions | -rw-r--r-- |
7701 | 1 |
(* Title: HOL/Recdef.thy |
2 |
ID: $Id$ |
|
10773 | 3 |
Author: Konrad Slind and Markus Wenzel, TU Muenchen |
12023 | 4 |
*) |
5123 | 5 |
|
12023 | 6 |
header {* TFL: recursive function definitions *} |
7701 | 7 |
|
15131 | 8 |
theory Recdef |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
9 |
imports Wellfounded_Relations |
16417 | 10 |
uses |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
15140
diff
changeset
|
11 |
("../TFL/casesplit.ML") |
10773 | 12 |
("../TFL/utils.ML") |
13 |
("../TFL/usyntax.ML") |
|
14 |
("../TFL/dcterm.ML") |
|
15 |
("../TFL/thms.ML") |
|
16 |
("../TFL/rules.ML") |
|
17 |
("../TFL/thry.ML") |
|
18 |
("../TFL/tfl.ML") |
|
19 |
("../TFL/post.ML") |
|
15131 | 20 |
("Tools/recdef_package.ML") |
21 |
begin |
|
10773 | 22 |
|
23 |
lemma tfl_eq_True: "(x = True) --> x" |
|
24 |
by blast |
|
25 |
||
26 |
lemma tfl_rev_eq_mp: "(x = y) --> y --> x"; |
|
27 |
by blast |
|
28 |
||
29 |
lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)" |
|
30 |
by blast |
|
6438 | 31 |
|
10773 | 32 |
lemma tfl_P_imp_P_iff_True: "P ==> P = True" |
33 |
by blast |
|
34 |
||
35 |
lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)" |
|
36 |
by blast |
|
37 |
||
12023 | 38 |
lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)" |
10773 | 39 |
by simp |
40 |
||
12023 | 41 |
lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R" |
10773 | 42 |
by blast |
43 |
||
12023 | 44 |
lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q" |
10773 | 45 |
by blast |
46 |
||
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
15140
diff
changeset
|
47 |
use "../TFL/casesplit.ML" |
10773 | 48 |
use "../TFL/utils.ML" |
49 |
use "../TFL/usyntax.ML" |
|
50 |
use "../TFL/dcterm.ML" |
|
51 |
use "../TFL/thms.ML" |
|
52 |
use "../TFL/rules.ML" |
|
53 |
use "../TFL/thry.ML" |
|
54 |
use "../TFL/tfl.ML" |
|
55 |
use "../TFL/post.ML" |
|
56 |
use "Tools/recdef_package.ML" |
|
6438 | 57 |
setup RecdefPackage.setup |
58 |
||
9855 | 59 |
lemmas [recdef_simp] = |
60 |
inv_image_def |
|
61 |
measure_def |
|
62 |
lex_prod_def |
|
11284 | 63 |
same_fst_def |
9855 | 64 |
less_Suc_eq [THEN iffD2] |
65 |
||
18336
1a2e30b37ed3
Added recdef congruence rules for bounded quantifiers and commonly used
krauss
parents:
17040
diff
changeset
|
66 |
lemmas [recdef_cong] = |
1a2e30b37ed3
Added recdef congruence rules for bounded quantifiers and commonly used
krauss
parents:
17040
diff
changeset
|
67 |
if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong |
9855 | 68 |
|
69 |
lemma let_cong [recdef_cong]: |
|
70 |
"M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g" |
|
71 |
by (unfold Let_def) blast |
|
72 |
||
73 |
lemmas [recdef_wf] = |
|
74 |
wf_trancl |
|
75 |
wf_less_than |
|
76 |
wf_lex_prod |
|
77 |
wf_inv_image |
|
78 |
wf_measure |
|
79 |
wf_pred_nat |
|
10653 | 80 |
wf_same_fst |
9855 | 81 |
wf_empty |
82 |
||
17040 | 83 |
(* The following should really go into Datatype or Finite_Set, but |
84 |
each one lacks the other theory as a parent . . . *) |
|
85 |
||
86 |
lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV" |
|
87 |
by (rule set_ext, case_tac x, auto) |
|
88 |
||
89 |
instance option :: (finite) finite |
|
90 |
proof |
|
91 |
have "finite (UNIV :: 'a set)" by (rule finite) |
|
92 |
hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp |
|
93 |
also have "insert None (Some ` (UNIV :: 'a set)) = UNIV" |
|
94 |
by (rule insert_None_conv_UNIV) |
|
95 |
finally show "finite (UNIV :: 'a option set)" . |
|
96 |
qed |
|
97 |
||
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
18336
diff
changeset
|
98 |
|
6438 | 99 |
end |