author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 60500  903bb1495239 
child 66447  a1f5c5c26fa6 
permissions  rwrr 
50087  1 
(* Author: Fabian Immler, TUM *) 
2 

60500  3 
section \<open>Sequence of Properties on Subsequences\<close> 
50087  4 

5 
theory Diagonal_Subsequence 

51526  6 
imports Complex_Main 
50087  7 
begin 
8 

9 
locale subseqs = 

10 
fixes P::"nat\<Rightarrow>(nat\<Rightarrow>nat)\<Rightarrow>bool" 

11 
assumes ex_subseq: "\<And>n s. subseq s \<Longrightarrow> \<exists>r'. subseq r' \<and> P n (s o r')" 

12 
begin 

13 

52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

14 
definition reduce where "reduce s n = (SOME r'. subseq r' \<and> P n (s o r'))" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

15 

8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

16 
lemma subseq_reduce[intro, simp]: 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

17 
"subseq s \<Longrightarrow> subseq (reduce s n)" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

18 
unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) auto 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

19 

8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

20 
lemma reduce_holds: 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

21 
"subseq s \<Longrightarrow> P n (s o reduce s n)" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

22 
unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) (auto simp: o_def) 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

23 

50087  24 
primrec seqseq where 
25 
"seqseq 0 = id" 

52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

26 
 "seqseq (Suc n) = seqseq n o reduce (seqseq n) n" 
50087  27 

52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

28 
lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)" 
50087  29 
proof (induct n) 
57862  30 
case 0 thus ?case by (simp add: subseq_def) 
31 
next 

32 
case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o) 

33 
qed 

52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

34 

8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

35 
lemma seqseq_holds: 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

36 
"P n (seqseq (Suc n))" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

37 
proof  
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

38 
have "P n (seqseq n o reduce (seqseq n) n)" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

39 
by (intro reduce_holds subseq_seqseq) 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

40 
thus ?thesis by simp 
50087  41 
qed 
42 

43 
definition diagseq where "diagseq i = seqseq i i" 

44 

52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

45 
lemma subseq_mono: "subseq f \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

46 
by (metis le_eq_less_or_eq subseq_mono) 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

47 

8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

48 
lemma subseq_strict_mono: "subseq f \<Longrightarrow> a < b \<Longrightarrow> f a < f b" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

49 
by (simp add: subseq_def) 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

50 

50087  51 
lemma diagseq_mono: "diagseq n < diagseq (Suc n)" 
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

52 
proof  
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

53 
have "diagseq n < seqseq n (Suc n)" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

54 
using subseq_seqseq[of n] by (simp add: diagseq_def subseq_def) 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

55 
also have "\<dots> \<le> seqseq n (reduce (seqseq n) n (Suc n))" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

56 
by (auto intro: subseq_mono seq_suble) 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

57 
also have "\<dots> = diagseq (Suc n)" by (simp add: diagseq_def) 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

58 
finally show ?thesis . 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

59 
qed 
50087  60 

61 
lemma subseq_diagseq: "subseq diagseq" 

62 
using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def) 

63 

64 
primrec fold_reduce where 

65 
"fold_reduce n 0 = id" 

52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

66 
 "fold_reduce n (Suc k) = fold_reduce n k o reduce (seqseq (n + k)) (n + k)" 
50087  67 

52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

68 
lemma subseq_fold_reduce[intro, simp]: "subseq (fold_reduce n k)" 
50087  69 
proof (induct k) 
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

70 
case (Suc k) from subseq_o[OF this subseq_reduce] show ?case by (simp add: o_def) 
50087  71 
qed (simp add: subseq_def) 
72 

73 
lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k" 

74 
by (induct k) simp_all 

75 

76 
lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n" 

77 
by (induct n) (simp_all) 

78 

79 
lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n" 

80 
using seqseq_fold_reduce by (simp add: diagseq_def) 

81 

82 
lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n" 

83 
by (induct n) simp_all 

84 

85 
lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)" 

86 
proof  

87 
have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)" 

88 
by (simp add: diagseq_fold_reduce) 

89 
also have "\<dots> = (seqseq k o fold_reduce k n) (k + n)" 

90 
unfolding fold_reduce_add seqseq_fold_reduce .. 

91 
finally show ?thesis . 

92 
qed 

93 

94 
lemma diagseq_sub: 

95 
assumes "m \<le> n" shows "diagseq n = (seqseq m o (fold_reduce m (n  m))) n" 

96 
using diagseq_add[of m "n  m"] assms by simp 

97 

98 
lemma subseq_diagonal_rest: "subseq (\<lambda>x. fold_reduce k x (k + x))" 

99 
unfolding subseq_Suc_iff fold_reduce.simps o_def 

52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

100 
proof 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

101 
fix n 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

102 
have "fold_reduce k n (k + n) < fold_reduce k n (k + Suc n)" (is "?lhs < _") 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

103 
by (auto intro: subseq_strict_mono) 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

104 
also have "\<dots> \<le> fold_reduce k n (reduce (seqseq (k + n)) (k + n) (k + Suc n))" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

105 
by (rule subseq_mono) (auto intro!: seq_suble subseq_mono) 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

106 
finally show "?lhs < \<dots>" . 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

107 
qed 
50087  108 

109 
lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (\<lambda>x. fold_reduce k x (k + x)))" 

110 
by (auto simp: o_def diagseq_add) 

111 

52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

112 
lemma diagseq_holds: 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

113 
assumes subseq_stable: "\<And>r s n. subseq r \<Longrightarrow> P n s \<Longrightarrow> P n (s o r)" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

114 
shows "P k (diagseq o (op + (Suc k)))" 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

115 
unfolding diagseq_seqseq by (intro subseq_stable subseq_diagonal_rest seqseq_holds) 
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset

116 

50087  117 
end 
118 

119 
end 