src/HOL/ex/Landau.thy
author blanchet
Wed, 15 Dec 2010 11:26:28 +0100
changeset 41140 9c68004b8c9d
parent 39302 d7728f65b353
child 41413 64cd30d6b0b8
permissions -rw-r--r--
added Sledgehammer support for higher-order propositional reasoning
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31381
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
     1
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
     2
(* Author: Florian Haftmann, TU Muenchen *)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
     3
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
     4
header {* Comparing growth of functions on natural numbers by a preorder relation *}
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
     5
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
     6
theory Landau
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
     7
imports Main Preorder
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
     8
begin
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
     9
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    10
text {*
36809
haftmann
parents: 36635
diff changeset
    11
  We establish a preorder releation @{text "\<lesssim>"} on functions from
haftmann
parents: 36635
diff changeset
    12
  @{text "\<nat>"} to @{text "\<nat>"} such that @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.
31381
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    13
*}
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    14
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    15
subsection {* Auxiliary *}
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    16
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    17
lemma Ex_All_bounded:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    18
  fixes n :: nat
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    19
  assumes "\<exists>n. \<forall>m\<ge>n. P m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    20
  obtains m where "m \<ge> n" and "P m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    21
proof -
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    22
  from assms obtain q where m_q: "\<forall>m\<ge>q. P m" ..
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    23
  let ?m = "max q n"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    24
  have "?m \<ge> n" by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    25
  moreover from m_q have "P ?m" by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    26
  ultimately show thesis ..
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    27
qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    28
    
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    29
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    30
subsection {* The @{text "\<lesssim>"} relation *}
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    31
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    32
definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50) where
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    33
  "f \<lesssim> g \<longleftrightarrow> (\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m)"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    34
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    35
lemma less_eq_fun_intro:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    36
  assumes "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    37
  shows "f \<lesssim> g"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    38
  unfolding less_eq_fun_def by (rule assms)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    39
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    40
lemma less_eq_fun_not_intro:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    41
  assumes "\<And>c n. \<exists>m\<ge>n. Suc c * g m < f m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    42
  shows "\<not> f \<lesssim> g"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    43
  using assms unfolding less_eq_fun_def linorder_not_le [symmetric]
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    44
  by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    45
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    46
lemma less_eq_fun_elim:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    47
  assumes "f \<lesssim> g"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    48
  obtains n c where "\<And>m. m \<ge> n \<Longrightarrow> f m \<le> Suc c * g m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    49
  using assms unfolding less_eq_fun_def by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    50
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    51
lemma less_eq_fun_not_elim:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    52
  assumes "\<not> f \<lesssim> g"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    53
  obtains m where "m \<ge> n" and "Suc c * g m < f m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    54
  using assms unfolding less_eq_fun_def linorder_not_le [symmetric]
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    55
  by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    56
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    57
lemma less_eq_fun_refl:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    58
  "f \<lesssim> f"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    59
proof (rule less_eq_fun_intro)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    60
  have "\<exists>n. \<forall>m\<ge>n. f m \<le> Suc 0 * f m" by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    61
  then show "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * f m" by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    62
qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    63
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    64
lemma less_eq_fun_trans:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    65
  assumes f_g: "f \<lesssim> g" and g_h: "g \<lesssim> h"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    66
  shows f_h: "f \<lesssim> h"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    67
proof -
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    68
  from f_g obtain n\<^isub>1 c\<^isub>1
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    69
    where P1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c\<^isub>1 * g m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    70
  by (erule less_eq_fun_elim)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    71
  moreover from g_h obtain n\<^isub>2 c\<^isub>2
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    72
    where P2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc c\<^isub>2 * h m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    73
  by (erule less_eq_fun_elim)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    74
  ultimately have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> Suc c\<^isub>1 * g m \<and> g m \<le> Suc c\<^isub>2 * h m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    75
  by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    76
  moreover {
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    77
    fix k l r :: nat
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    78
    assume k_l: "k \<le> Suc c\<^isub>1 * l" and l_r: "l \<le> Suc c\<^isub>2 * r"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    79
    from l_r have "Suc c\<^isub>1 * l \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    80
    by (auto simp add: mult_le_cancel_left mult_assoc simp del: times_nat.simps mult_Suc_right)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    81
    with k_l have "k \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r" by (rule preorder_class.order_trans)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    82
  }
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    83
  ultimately have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * h m" by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    84
  then have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> Suc ((Suc c\<^isub>1 * Suc c\<^isub>2) - 1) * h m" by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    85
  then show ?thesis unfolding less_eq_fun_def by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    86
qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    87
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    88
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    89
subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    90
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    91
definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50) where
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    92
  "f \<cong> g \<longleftrightarrow> (\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m)"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    93
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    94
lemma equiv_fun_intro:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    95
  assumes "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    96
  shows "f \<cong> g"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    97
  unfolding equiv_fun_def by (rule assms)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    98
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
    99
lemma equiv_fun_not_intro:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   100
  assumes "\<And>d c n. \<exists>m\<ge>n. Suc d * f m < g m \<or> Suc c * g m < f m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   101
  shows "\<not> f \<cong> g"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   102
  unfolding equiv_fun_def
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   103
  by (auto simp add: assms linorder_not_le
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   104
    simp del: times_nat.simps mult_Suc_right)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   105
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   106
lemma equiv_fun_elim:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   107
  assumes "f \<cong> g"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   108
  obtains n d c
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   109
    where "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   110
  using assms unfolding equiv_fun_def by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   111
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   112
lemma equiv_fun_not_elim:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   113
  fixes n d c
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   114
  assumes "\<not> f \<cong> g"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   115
  obtains m where "m \<ge> n"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   116
    and "Suc d * f m < g m \<or> Suc c * g m < f m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   117
  using assms unfolding equiv_fun_def
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   118
  by (auto simp add: linorder_not_le, blast)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   119
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   120
lemma equiv_fun_less_eq_fun:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   121
  "f \<cong> g \<longleftrightarrow> f \<lesssim> g \<and> g \<lesssim> f"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   122
proof
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   123
  assume x_y: "f \<cong> g"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   124
  then obtain n d c
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   125
    where interv: "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   126
  by (erule equiv_fun_elim)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   127
  from interv have "\<exists>c n. \<forall>m \<ge> n. f m \<le> Suc c * g m" by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   128
  then have f_g: "f \<lesssim> g" by (rule less_eq_fun_intro)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   129
  from interv have "\<exists>d n. \<forall>m \<ge> n. g m \<le> Suc d * f m" by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   130
  then have g_f: "g \<lesssim> f" by (rule less_eq_fun_intro)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   131
  from f_g g_f show "f \<lesssim> g \<and> g \<lesssim> f" by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   132
next
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   133
  assume assm: "f \<lesssim> g \<and> g \<lesssim> f"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   134
  from assm less_eq_fun_elim obtain c n\<^isub>1 where
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   135
    bound1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c * g m" 
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   136
    by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   137
  from assm less_eq_fun_elim obtain d n\<^isub>2 where
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   138
    bound2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   139
    by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   140
  from bound2 have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   141
  by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   142
  with bound1
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   143
    have "\<forall>m \<ge> max n\<^isub>1 n\<^isub>2. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   144
    by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   145
  then
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   146
    have "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   147
    by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   148
  then show "f \<cong> g" by (rule equiv_fun_intro)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   149
qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   150
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   151
subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   152
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   153
definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50) where
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   154
  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   155
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   156
lemma less_fun_intro:
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   157
  assumes "\<And>c. \<exists>n. \<forall>m\<ge>n. Suc c * f m < g m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   158
  shows "f \<prec> g"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   159
proof (unfold less_fun_def, rule conjI)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   160
  from assms obtain n
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   161
    where "\<forall>m\<ge>n. Suc 0 * f m < g m" ..
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   162
  then have "\<forall>m\<ge>n. f m \<le> Suc 0 * g m" by auto
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   163
  then have "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m" by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   164
  then show "f \<lesssim> g" by (rule less_eq_fun_intro)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   165
next
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   166
  show "\<not> g \<lesssim> f"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   167
  proof (rule less_eq_fun_not_intro)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   168
    fix c n :: nat
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   169
    from assms have "\<exists>n. \<forall>m\<ge>n. Suc c * f m < g m" by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   170
    then obtain m where "m \<ge> n" and "Suc c * f m < g m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   171
      by (rule Ex_All_bounded)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   172
    then show "\<exists>m\<ge>n. Suc c * f m < g m" by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   173
  qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   174
qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   175
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   176
text {*
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   177
  We would like to show (or refute) that @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"},
36809
haftmann
parents: 36635
diff changeset
   178
  i.e.~@{prop "f \<prec> g \<longleftrightarrow> (\<forall>c. \<exists>n. \<forall>m>n. f m < Suc c * g m)"} but did not
haftmann
parents: 36635
diff changeset
   179
  manage to do so.
31381
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   180
*}
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   181
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   182
36809
haftmann
parents: 36635
diff changeset
   183
subsection {* Assert that @{text "\<lesssim>"} is indeed a preorder *}
31381
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   184
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   185
interpretation fun_order: preorder_equiv less_eq_fun less_fun
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   186
  where "preorder_equiv.equiv less_eq_fun = equiv_fun"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   187
proof -
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   188
  interpret preorder_equiv less_eq_fun less_fun proof
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   189
  qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
36635
080b755377c0 locale predicates of classes carry a mandatory "class" prefix
haftmann
parents: 31381
diff changeset
   190
  show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
31381
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   191
  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   192
    by (simp add: fun_eq_iff equiv_def equiv_fun_less_eq_fun)
31381
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   193
qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   194
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   195
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   196
subsection {* Simple examples *}
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   197
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   198
lemma "(\<lambda>_. n) \<lesssim> (\<lambda>n. n)"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   199
proof (rule less_eq_fun_intro)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   200
  show "\<exists>c q. \<forall>m\<ge>q. n \<le> Suc c * m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   201
  proof -
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   202
    have "\<forall>m\<ge>n. n \<le> Suc 0 * m" by simp
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   203
    then show ?thesis by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   204
  qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   205
qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   206
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   207
lemma "(\<lambda>n. n) \<cong> (\<lambda>n. Suc k * n)"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   208
proof (rule equiv_fun_intro)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   209
  show "\<exists>d c n. \<forall>m\<ge>n. Suc k * m \<le> Suc d * m \<and> m \<le> Suc c * (Suc k * m)"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   210
  proof -
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   211
    have "\<forall>m\<ge>n. Suc k * m \<le> Suc k * m \<and> m \<le> Suc c * (Suc k * m)" by simp
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   212
    then show ?thesis by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   213
  qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   214
qed  
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   215
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   216
lemma "(\<lambda>_. n) \<prec> (\<lambda>n. n)"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   217
proof (rule less_fun_intro)
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   218
  fix c
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   219
  show "\<exists>q. \<forall>m\<ge>q. Suc c * n < m"
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   220
  proof -
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   221
    have "\<forall>m\<ge>Suc c * n + 1. Suc c * n < m" by simp
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   222
    then show ?thesis by blast
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   223
  qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   224
qed
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   225
b3a785a69538 added Landau theory
haftmann
parents:
diff changeset
   226
end