author  krauss 
Fri, 25 Apr 2008 15:30:33 +0200  
changeset 26748  4d51ddd6aa5c 
parent 23742  d6349ac8b153 
child 29654  24e73987bfe2 
permissions  rwrr 
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 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

9 
imports FunDef 
16417  10 
uses 
23150  11 
("Tools/TFL/casesplit.ML") 
12 
("Tools/TFL/utils.ML") 

13 
("Tools/TFL/usyntax.ML") 

14 
("Tools/TFL/dcterm.ML") 

15 
("Tools/TFL/thms.ML") 

16 
("Tools/TFL/rules.ML") 

17 
("Tools/TFL/thry.ML") 

18 
("Tools/TFL/tfl.ML") 

19 
("Tools/TFL/post.ML") 

15131  20 
("Tools/recdef_package.ML") 
21 
begin 

10773  22 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

23 
text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

24 
lemma def_wfrec: "[ f==wfrec r H; wf(r) ] ==> f(a) = H (cut f r a) a" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

25 
apply auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

26 
apply (blast intro: wfrec) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

27 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

28 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

29 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

30 
lemma tfl_wf_induct: "ALL R. wf R > 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

31 
(ALL P. (ALL x. (ALL y. (y,x):R > P y) > P x) > (ALL x. P x))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

32 
apply clarify 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

33 
apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

34 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

35 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

36 
lemma tfl_cut_apply: "ALL f R. (x,a):R > (cut f R a)(x) = f(x)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

37 
apply clarify 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

38 
apply (rule cut_apply, assumption) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

39 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

40 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

41 
lemma tfl_wfrec: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

42 
"ALL M R f. (f=wfrec R M) > wf R > (ALL x. f x = M (cut f R x) x)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

43 
apply clarify 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

44 
apply (erule wfrec) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

45 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

46 

10773  47 
lemma tfl_eq_True: "(x = True) > x" 
48 
by blast 

49 

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

51 
by blast 

52 

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

54 
by blast 

6438  55 

10773  56 
lemma tfl_P_imp_P_iff_True: "P ==> P = True" 
57 
by blast 

58 

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

60 
by blast 

61 

12023  62 
lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)" 
10773  63 
by simp 
64 

12023  65 
lemma tfl_disjE: "P \<or> Q ==> P > R ==> Q > R ==> R" 
10773  66 
by blast 
67 

12023  68 
lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x > Q ==> Q" 
10773  69 
by blast 
70 

23150  71 
use "Tools/TFL/casesplit.ML" 
72 
use "Tools/TFL/utils.ML" 

73 
use "Tools/TFL/usyntax.ML" 

74 
use "Tools/TFL/dcterm.ML" 

75 
use "Tools/TFL/thms.ML" 

76 
use "Tools/TFL/rules.ML" 

77 
use "Tools/TFL/thry.ML" 

78 
use "Tools/TFL/tfl.ML" 

79 
use "Tools/TFL/post.ML" 

10773  80 
use "Tools/recdef_package.ML" 
6438  81 
setup RecdefPackage.setup 
82 

9855  83 
lemmas [recdef_simp] = 
84 
inv_image_def 

85 
measure_def 

86 
lex_prod_def 

11284  87 
same_fst_def 
9855  88 
less_Suc_eq [THEN iffD2] 
89 

23150  90 
lemmas [recdef_cong] = 
22622
25693088396b
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
krauss
parents:
22399
diff
changeset

91 
if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong 
9855  92 

93 
lemmas [recdef_wf] = 

94 
wf_trancl 

95 
wf_less_than 

96 
wf_lex_prod 

97 
wf_inv_image 

98 
wf_measure 

99 
wf_pred_nat 

10653  100 
wf_same_fst 
9855  101 
wf_empty 
102 

6438  103 
end 