author | wenzelm |
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04) | |
changeset 24850 | 0cfd722ab579 |
parent 23742 | d6349ac8b153 |
child 26748 | 4d51ddd6aa5c |
permissions | -rw-r--r-- |
wenzelm@7701 | 1 |
(* Title: HOL/Recdef.thy |
wenzelm@7701 | 2 |
ID: $Id$ |
wenzelm@10773 | 3 |
Author: Konrad Slind and Markus Wenzel, TU Muenchen |
wenzelm@12023 | 4 |
*) |
wenzelm@5123 | 5 |
|
wenzelm@12023 | 6 |
header {* TFL: recursive function definitions *} |
wenzelm@7701 | 7 |
|
nipkow@15131 | 8 |
theory Recdef |
krauss@22622 | 9 |
imports Wellfounded_Relations FunDef |
haftmann@16417 | 10 |
uses |
wenzelm@23150 | 11 |
("Tools/TFL/casesplit.ML") |
wenzelm@23150 | 12 |
("Tools/TFL/utils.ML") |
wenzelm@23150 | 13 |
("Tools/TFL/usyntax.ML") |
wenzelm@23150 | 14 |
("Tools/TFL/dcterm.ML") |
wenzelm@23150 | 15 |
("Tools/TFL/thms.ML") |
wenzelm@23150 | 16 |
("Tools/TFL/rules.ML") |
wenzelm@23150 | 17 |
("Tools/TFL/thry.ML") |
wenzelm@23150 | 18 |
("Tools/TFL/tfl.ML") |
wenzelm@23150 | 19 |
("Tools/TFL/post.ML") |
nipkow@15131 | 20 |
("Tools/recdef_package.ML") |
nipkow@15131 | 21 |
begin |
wenzelm@10773 | 22 |
|
wenzelm@10773 | 23 |
lemma tfl_eq_True: "(x = True) --> x" |
wenzelm@10773 | 24 |
by blast |
wenzelm@10773 | 25 |
|
wenzelm@10773 | 26 |
lemma tfl_rev_eq_mp: "(x = y) --> y --> x"; |
wenzelm@10773 | 27 |
by blast |
wenzelm@10773 | 28 |
|
wenzelm@10773 | 29 |
lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)" |
wenzelm@10773 | 30 |
by blast |
wenzelm@6438 | 31 |
|
wenzelm@10773 | 32 |
lemma tfl_P_imp_P_iff_True: "P ==> P = True" |
wenzelm@10773 | 33 |
by blast |
wenzelm@10773 | 34 |
|
wenzelm@10773 | 35 |
lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)" |
wenzelm@10773 | 36 |
by blast |
wenzelm@10773 | 37 |
|
wenzelm@12023 | 38 |
lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)" |
wenzelm@10773 | 39 |
by simp |
wenzelm@10773 | 40 |
|
wenzelm@12023 | 41 |
lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R" |
wenzelm@10773 | 42 |
by blast |
wenzelm@10773 | 43 |
|
wenzelm@12023 | 44 |
lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q" |
wenzelm@10773 | 45 |
by blast |
wenzelm@10773 | 46 |
|
wenzelm@23150 | 47 |
use "Tools/TFL/casesplit.ML" |
wenzelm@23150 | 48 |
use "Tools/TFL/utils.ML" |
wenzelm@23150 | 49 |
use "Tools/TFL/usyntax.ML" |
wenzelm@23150 | 50 |
use "Tools/TFL/dcterm.ML" |
wenzelm@23150 | 51 |
use "Tools/TFL/thms.ML" |
wenzelm@23150 | 52 |
use "Tools/TFL/rules.ML" |
wenzelm@23150 | 53 |
use "Tools/TFL/thry.ML" |
wenzelm@23150 | 54 |
use "Tools/TFL/tfl.ML" |
wenzelm@23150 | 55 |
use "Tools/TFL/post.ML" |
wenzelm@10773 | 56 |
use "Tools/recdef_package.ML" |
wenzelm@6438 | 57 |
setup RecdefPackage.setup |
wenzelm@6438 | 58 |
|
wenzelm@9855 | 59 |
lemmas [recdef_simp] = |
wenzelm@9855 | 60 |
inv_image_def |
wenzelm@9855 | 61 |
measure_def |
wenzelm@9855 | 62 |
lex_prod_def |
nipkow@11284 | 63 |
same_fst_def |
wenzelm@9855 | 64 |
less_Suc_eq [THEN iffD2] |
wenzelm@9855 | 65 |
|
wenzelm@23150 | 66 |
lemmas [recdef_cong] = |
krauss@22622 | 67 |
if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong |
wenzelm@9855 | 68 |
|
wenzelm@9855 | 69 |
lemmas [recdef_wf] = |
wenzelm@9855 | 70 |
wf_trancl |
wenzelm@9855 | 71 |
wf_less_than |
wenzelm@9855 | 72 |
wf_lex_prod |
wenzelm@9855 | 73 |
wf_inv_image |
wenzelm@9855 | 74 |
wf_measure |
wenzelm@9855 | 75 |
wf_pred_nat |
nipkow@10653 | 76 |
wf_same_fst |
wenzelm@9855 | 77 |
wf_empty |
wenzelm@9855 | 78 |
|
wenzelm@6438 | 79 |
end |