src/HOLCF/Eventual.thy
author huffman
Mon May 11 08:28:09 2009 -0700 (2009-05-11)
changeset 31095 b79d140f6d0b
parent 27408 22a515a55bf5
child 35771 2b75230f272f
permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman@27408
     1
theory Eventual
huffman@27408
     2
imports Infinite_Set
huffman@27408
     3
begin
huffman@27408
     4
huffman@27408
     5
subsection {* Lemmas about MOST *}
huffman@27408
     6
huffman@27408
     7
lemma MOST_INFM:
huffman@27408
     8
  assumes inf: "infinite (UNIV::'a set)"
huffman@27408
     9
  shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
huffman@27408
    10
  unfolding Alm_all_def Inf_many_def
huffman@27408
    11
  apply (auto simp add: Collect_neg_eq)
huffman@27408
    12
  apply (drule (1) finite_UnI)
huffman@27408
    13
  apply (simp add: Compl_partition2 inf)
huffman@27408
    14
  done
huffman@27408
    15
huffman@27408
    16
lemma MOST_comp: "\<lbrakk>inj f; MOST x. P x\<rbrakk> \<Longrightarrow> MOST x. P (f x)"
huffman@27408
    17
unfolding MOST_iff_finiteNeg
huffman@27408
    18
by (drule (1) finite_vimageI, simp)
huffman@27408
    19
huffman@27408
    20
lemma INFM_comp: "\<lbrakk>inj f; INFM x. P (f x)\<rbrakk> \<Longrightarrow> INFM x. P x"
huffman@27408
    21
unfolding Inf_many_def
huffman@27408
    22
by (clarify, drule (1) finite_vimageI, simp)
huffman@27408
    23
huffman@27408
    24
lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
huffman@27408
    25
by (rule MOST_comp [OF inj_Suc])
huffman@27408
    26
huffman@27408
    27
lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
huffman@27408
    28
unfolding MOST_nat
huffman@27408
    29
apply (clarify, rule_tac x="Suc m" in exI, clarify)
huffman@27408
    30
apply (erule Suc_lessE, simp)
huffman@27408
    31
done
huffman@27408
    32
huffman@27408
    33
lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
huffman@27408
    34
by (rule iffI [OF MOST_SucD MOST_SucI])
huffman@27408
    35
huffman@27408
    36
lemma INFM_finite_Bex_distrib:
huffman@27408
    37
  "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)"
huffman@27408
    38
by (induct set: finite, simp, simp add: INFM_disj_distrib)
huffman@27408
    39
huffman@27408
    40
lemma MOST_finite_Ball_distrib:
huffman@27408
    41
  "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)"
huffman@27408
    42
by (induct set: finite, simp, simp add: MOST_conj_distrib)
huffman@27408
    43
huffman@27408
    44
lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
huffman@27408
    45
unfolding MOST_nat_le by fast
huffman@27408
    46
huffman@27408
    47
subsection {* Eventually constant sequences *}
huffman@27408
    48
huffman@27408
    49
definition
huffman@27408
    50
  eventually_constant :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
huffman@27408
    51
where
huffman@27408
    52
  "eventually_constant S = (\<exists>x. MOST i. S i = x)"
huffman@27408
    53
huffman@27408
    54
lemma eventually_constant_MOST_MOST:
huffman@27408
    55
  "eventually_constant S \<longleftrightarrow> (MOST m. MOST n. S n = S m)"
huffman@27408
    56
unfolding eventually_constant_def MOST_nat
huffman@27408
    57
apply safe
huffman@27408
    58
apply (rule_tac x=m in exI, clarify)
huffman@27408
    59
apply (rule_tac x=m in exI, clarify)
huffman@27408
    60
apply simp
huffman@27408
    61
apply fast
huffman@27408
    62
done
huffman@27408
    63
huffman@27408
    64
lemma eventually_constantI: "MOST i. S i = x \<Longrightarrow> eventually_constant S"
huffman@27408
    65
unfolding eventually_constant_def by fast
huffman@27408
    66
huffman@27408
    67
lemma eventually_constant_comp:
huffman@27408
    68
  "eventually_constant (\<lambda>i. S i) \<Longrightarrow> eventually_constant (\<lambda>i. f (S i))"
huffman@27408
    69
unfolding eventually_constant_def
huffman@27408
    70
apply (erule exE, rule_tac x="f x" in exI)
huffman@27408
    71
apply (erule MOST_mono, simp)
huffman@27408
    72
done
huffman@27408
    73
huffman@27408
    74
lemma eventually_constant_Suc_iff:
huffman@27408
    75
  "eventually_constant (\<lambda>i. S (Suc i)) \<longleftrightarrow> eventually_constant (\<lambda>i. S i)"
huffman@27408
    76
unfolding eventually_constant_def
huffman@27408
    77
by (subst MOST_Suc_iff, rule refl)
huffman@27408
    78
huffman@27408
    79
lemma eventually_constant_SucD:
huffman@27408
    80
  "eventually_constant (\<lambda>i. S (Suc i)) \<Longrightarrow> eventually_constant (\<lambda>i. S i)"
huffman@27408
    81
by (rule eventually_constant_Suc_iff [THEN iffD1])
huffman@27408
    82
huffman@27408
    83
subsection {* Limits of eventually constant sequences *}
huffman@27408
    84
huffman@27408
    85
definition
huffman@27408
    86
  eventual :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
huffman@27408
    87
  "eventual S = (THE x. MOST i. S i = x)"
huffman@27408
    88
huffman@27408
    89
lemma eventual_eqI: "MOST i. S i = x \<Longrightarrow> eventual S = x"
huffman@27408
    90
unfolding eventual_def
huffman@27408
    91
apply (rule the_equality, assumption)
huffman@27408
    92
apply (rename_tac y)
huffman@27408
    93
apply (subgoal_tac "MOST i::nat. y = x", simp)
huffman@27408
    94
apply (erule MOST_rev_mp)
huffman@27408
    95
apply (erule MOST_rev_mp)
huffman@27408
    96
apply simp
huffman@27408
    97
done
huffman@27408
    98
huffman@27408
    99
lemma MOST_eq_eventual:
huffman@27408
   100
  "eventually_constant S \<Longrightarrow> MOST i. S i = eventual S"
huffman@27408
   101
unfolding eventually_constant_def
huffman@27408
   102
by (erule exE, simp add: eventual_eqI)
huffman@27408
   103
huffman@27408
   104
lemma eventual_mem_range:
huffman@27408
   105
  "eventually_constant S \<Longrightarrow> eventual S \<in> range S"
huffman@27408
   106
apply (drule MOST_eq_eventual)
huffman@27408
   107
apply (simp only: MOST_nat_le, clarify)
huffman@27408
   108
apply (drule spec, drule mp, rule order_refl)
huffman@27408
   109
apply (erule range_eqI [OF sym])
huffman@27408
   110
done
huffman@27408
   111
huffman@27408
   112
lemma eventually_constant_MOST_iff:
huffman@27408
   113
  assumes S: "eventually_constant S"
huffman@27408
   114
  shows "(MOST n. P (S n)) \<longleftrightarrow> P (eventual S)"
huffman@27408
   115
apply (subgoal_tac "(MOST n. P (S n)) \<longleftrightarrow> (MOST n::nat. P (eventual S))")
huffman@27408
   116
apply simp
huffman@27408
   117
apply (rule iffI)
huffman@27408
   118
apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
huffman@27408
   119
apply (erule MOST_mono, force)
huffman@27408
   120
apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
huffman@27408
   121
apply (erule MOST_mono, simp)
huffman@27408
   122
done
huffman@27408
   123
huffman@27408
   124
lemma MOST_eventual:
huffman@27408
   125
  "\<lbrakk>eventually_constant S; MOST n. P (S n)\<rbrakk> \<Longrightarrow> P (eventual S)"
huffman@27408
   126
proof -
huffman@27408
   127
  assume "eventually_constant S"
huffman@27408
   128
  hence "MOST n. S n = eventual S"
huffman@27408
   129
    by (rule MOST_eq_eventual)
huffman@27408
   130
  moreover assume "MOST n. P (S n)"
huffman@27408
   131
  ultimately have "MOST n. S n = eventual S \<and> P (S n)"
huffman@27408
   132
    by (rule MOST_conj_distrib [THEN iffD2, OF conjI])
huffman@27408
   133
  hence "MOST n::nat. P (eventual S)"
huffman@27408
   134
    by (rule MOST_mono) auto
huffman@27408
   135
  thus ?thesis by simp
huffman@27408
   136
qed
huffman@27408
   137
huffman@27408
   138
lemma eventually_constant_MOST_Suc_eq:
huffman@27408
   139
  "eventually_constant S \<Longrightarrow> MOST n. S (Suc n) = S n"
huffman@27408
   140
apply (drule MOST_eq_eventual)
huffman@27408
   141
apply (frule MOST_Suc_iff [THEN iffD2])
huffman@27408
   142
apply (erule MOST_rev_mp)
huffman@27408
   143
apply (erule MOST_rev_mp)
huffman@27408
   144
apply simp
huffman@27408
   145
done
huffman@27408
   146
huffman@27408
   147
lemma eventual_comp:
huffman@27408
   148
  "eventually_constant S \<Longrightarrow> eventual (\<lambda>i. f (S i)) = f (eventual (\<lambda>i. S i))"
huffman@27408
   149
apply (rule eventual_eqI)
huffman@27408
   150
apply (rule MOST_mono)
huffman@27408
   151
apply (erule MOST_eq_eventual)
huffman@27408
   152
apply simp
huffman@27408
   153
done
huffman@27408
   154
huffman@27408
   155
end