author  hoelzl 
Thu, 04 Sep 2014 14:02:37 +0200  
changeset 58184  db1381d811ab 
parent 56248  67dc9549fa15 
child 58825  2065f49da190 
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 
55017  8 
imports Main 
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 

58184
db1381d811ab
cleanup Wfrec; introduce dependent_wf/wellorder_choice
hoelzl
parents:
56248
diff
changeset

23 
lemma tfl_cut_def: "cut f r x \<equiv> (\<lambda>y. if (y,x) \<in> r then f y else undefined)" 
db1381d811ab
cleanup Wfrec; introduce dependent_wf/wellorder_choice
hoelzl
parents:
56248
diff
changeset

24 
unfolding cut_def . 
db1381d811ab
cleanup Wfrec; introduce dependent_wf/wellorder_choice
hoelzl
parents:
56248
diff
changeset

25 

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

26 
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

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

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

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

30 

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

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

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

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

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

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

36 

10773  37 
lemma tfl_eq_True: "(x = True) > x" 
38 
by blast 

39 

46947  40 
lemma tfl_rev_eq_mp: "(x = y) > y > x" 
10773  41 
by blast 
42 

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

44 
by blast 

6438  45 

10773  46 
lemma tfl_P_imp_P_iff_True: "P ==> P = True" 
47 
by blast 

48 

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

50 
by blast 

51 

12023  52 
lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)" 
10773  53 
by simp 
54 

12023  55 
lemma tfl_disjE: "P \<or> Q ==> P > R ==> Q > R ==> R" 
10773  56 
by blast 
57 

12023  58 
lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x > Q ==> Q" 
10773  59 
by blast 
60 

48891  61 
ML_file "~~/src/HOL/Tools/TFL/casesplit.ML" 
62 
ML_file "~~/src/HOL/Tools/TFL/utils.ML" 

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

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

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

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

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

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

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

70 
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

71 
setup Recdef.setup 
6438  72 

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

73 
subsection {* Rule setup *} 
32244  74 

9855  75 
lemmas [recdef_simp] = 
76 
inv_image_def 

77 
measure_def 

78 
lex_prod_def 

11284  79 
same_fst_def 
9855  80 
less_Suc_eq [THEN iffD2] 
81 

23150  82 
lemmas [recdef_cong] = 
56248
67dc9549fa15
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents:
55017
diff
changeset

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

84 
map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong 
9855  85 

86 
lemmas [recdef_wf] = 

87 
wf_trancl 

88 
wf_less_than 

89 
wf_lex_prod 

90 
wf_inv_image 

91 
wf_measure 

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

92 
wf_measures 
9855  93 
wf_pred_nat 
10653  94 
wf_same_fst 
9855  95 
wf_empty 
96 

6438  97 
end 