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


9 
import Wellfounded_Relations Datatype

7701

10 
files

10773

11 
("../TFL/utils.ML")


12 
("../TFL/usyntax.ML")


13 
("../TFL/dcterm.ML")


14 
("../TFL/thms.ML")


15 
("../TFL/rules.ML")


16 
("../TFL/thry.ML")


17 
("../TFL/tfl.ML")


18 
("../TFL/post.ML")

15131

19 
("Tools/recdef_package.ML")


20 
begin

10773

21 


22 
lemma tfl_eq_True: "(x = True) > x"


23 
by blast


24 


25 
lemma tfl_rev_eq_mp: "(x = y) > y > x";


26 
by blast


27 


28 
lemma tfl_simp_thm: "(x > y) > (x = x') > (x' > y)"


29 
by blast

6438

30 

10773

31 
lemma tfl_P_imp_P_iff_True: "P ==> P = True"


32 
by blast


33 


34 
lemma tfl_imp_trans: "(A > B) ==> (B > C) ==> (A > C)"


35 
by blast


36 

12023

37 
lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"

10773

38 
by simp


39 

12023

40 
lemma tfl_disjE: "P \<or> Q ==> P > R ==> Q > R ==> R"

10773

41 
by blast


42 

12023

43 
lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x > Q ==> Q"

10773

44 
by blast


45 


46 
use "../TFL/utils.ML"


47 
use "../TFL/usyntax.ML"


48 
use "../TFL/dcterm.ML"


49 
use "../TFL/thms.ML"


50 
use "../TFL/rules.ML"


51 
use "../TFL/thry.ML"


52 
use "../TFL/tfl.ML"


53 
use "../TFL/post.ML"


54 
use "Tools/recdef_package.ML"

6438

55 
setup RecdefPackage.setup


56 

9855

57 
lemmas [recdef_simp] =


58 
inv_image_def


59 
measure_def


60 
lex_prod_def

11284

61 
same_fst_def

9855

62 
less_Suc_eq [THEN iffD2]


63 

11165

64 
lemmas [recdef_cong] = if_cong image_cong

9855

65 


66 
lemma let_cong [recdef_cong]:


67 
"M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"


68 
by (unfold Let_def) blast


69 


70 
lemmas [recdef_wf] =


71 
wf_trancl


72 
wf_less_than


73 
wf_lex_prod


74 
wf_inv_image


75 
wf_measure


76 
wf_pred_nat

10653

77 
wf_same_fst

9855

78 
wf_empty


79 

6438

80 
end
