author  wenzelm 
Wed, 22 Aug 2012 22:55:41 +0200  
changeset 48891  c0eafbd55de3 
parent 46950  d0181abdbdac 
child 55017  2df6ad1dbd66 
permissions  rwrr 
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

1 
(* Title: HOL/Library/Old_Recdef.thy 
10773  2 
Author: Konrad Slind and Markus Wenzel, TU Muenchen 
12023  3 
*) 
5123  4 

12023  5 
header {* TFL: recursive function definitions *} 
7701  6 

44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

7 
theory Old_Recdef 
44014
88bd7d74a2c1
moved recursion combinator to HOL/Library/Wfrec.thy  it is so fundamental and wellknown that it should survive recdef
krauss
parents:
44013
diff
changeset

8 
imports Wfrec 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46947
diff
changeset

9 
keywords 
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46947
diff
changeset

10 
"recdef" "defer_recdef" :: thy_decl and 
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46947
diff
changeset

11 
"recdef_tc" :: thy_goal and 
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46947
diff
changeset

12 
"permissive" "congs" "hints" 
15131  13 
begin 
10773  14 

44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

15 
subsection {* Lemmas for TFL *} 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

16 

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

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

18 
(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

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

20 
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

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

22 

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

23 
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

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

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

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

27 

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

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

29 
"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

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

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

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

33 

10773  34 
lemma tfl_eq_True: "(x = True) > x" 
35 
by blast 

36 

46947  37 
lemma tfl_rev_eq_mp: "(x = y) > y > x" 
10773  38 
by blast 
39 

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

41 
by blast 

6438  42 

10773  43 
lemma tfl_P_imp_P_iff_True: "P ==> P = True" 
44 
by blast 

45 

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

47 
by blast 

48 

12023  49 
lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)" 
10773  50 
by simp 
51 

12023  52 
lemma tfl_disjE: "P \<or> Q ==> P > R ==> Q > R ==> R" 
10773  53 
by blast 
54 

12023  55 
lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x > Q ==> Q" 
10773  56 
by blast 
57 

48891  58 
ML_file "~~/src/HOL/Tools/TFL/casesplit.ML" 
59 
ML_file "~~/src/HOL/Tools/TFL/utils.ML" 

60 
ML_file "~~/src/HOL/Tools/TFL/usyntax.ML" 

61 
ML_file "~~/src/HOL/Tools/TFL/dcterm.ML" 

62 
ML_file "~~/src/HOL/Tools/TFL/thms.ML" 

63 
ML_file "~~/src/HOL/Tools/TFL/rules.ML" 

64 
ML_file "~~/src/HOL/Tools/TFL/thry.ML" 

65 
ML_file "~~/src/HOL/Tools/TFL/tfl.ML" 

66 
ML_file "~~/src/HOL/Tools/TFL/post.ML" 

67 
ML_file "~~/src/HOL/Tools/recdef.ML" 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
29654
diff
changeset

68 
setup Recdef.setup 
6438  69 

44014
88bd7d74a2c1
moved recursion combinator to HOL/Library/Wfrec.thy  it is so fundamental and wellknown that it should survive recdef
krauss
parents:
44013
diff
changeset

70 
subsection {* Rule setup *} 
32244  71 

9855  72 
lemmas [recdef_simp] = 
73 
inv_image_def 

74 
measure_def 

75 
lex_prod_def 

11284  76 
same_fst_def 
9855  77 
less_Suc_eq [THEN iffD2] 
78 

23150  79 
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

80 
if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong 
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

81 
map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong 
9855  82 

83 
lemmas [recdef_wf] = 

84 
wf_trancl 

85 
wf_less_than 

86 
wf_lex_prod 

87 
wf_inv_image 

88 
wf_measure 

44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

89 
wf_measures 
9855  90 
wf_pred_nat 
10653  91 
wf_same_fst 
9855  92 
wf_empty 
93 

6438  94 
end 