equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* TFL: recursive function definitions *} |
6 header {* TFL: recursive function definitions *} |
7 |
7 |
8 theory Recdef |
8 theory Recdef |
9 imports Wellfounded_Relations |
9 imports Wellfounded_Relations FunDef |
10 uses |
10 uses |
11 ("../TFL/casesplit.ML") |
11 ("../TFL/casesplit.ML") |
12 ("../TFL/utils.ML") |
12 ("../TFL/utils.ML") |
13 ("../TFL/usyntax.ML") |
13 ("../TFL/usyntax.ML") |
14 ("../TFL/dcterm.ML") |
14 ("../TFL/dcterm.ML") |
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 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 |
|
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 |
68 |
73 lemmas [recdef_wf] = |
69 lemmas [recdef_wf] = |
74 wf_trancl |
70 wf_trancl |
75 wf_less_than |
71 wf_less_than |
76 wf_lex_prod |
72 wf_lex_prod |