Moment.thy
author zhangx
Wed, 13 Jan 2016 23:39:59 +0800
changeset 73 b0054fb0d1ce
parent 72 3fa70b12c117
child 74 83ba2d8c859a
permissions -rw-r--r--
Moment.thy further improved.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
theory Moment
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
imports Main
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
69
1dc801552dfd simplified Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 67
diff changeset
     5
definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
1dc801552dfd simplified Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 67
diff changeset
     6
where "moment n s = rev (take n (rev s))"
67
25fd656667a7 Correctness simplified a great deal.
zhangx
parents: 35
diff changeset
     7
70
92ca2410b3d9 further simplificaton of Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 69
diff changeset
     8
value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
92ca2410b3d9 further simplificaton of Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 69
diff changeset
     9
value "moment 2 [5, 4, 3, 2, 1, 0::int]"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
71
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
    11
(*
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
lemma length_moment_le:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
  assumes le_k: "k \<le> length s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
  shows "length (moment k s) = k"
69
1dc801552dfd simplified Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 67
diff changeset
    15
using le_k unfolding moment_def by auto
71
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
    16
*)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
71
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
    18
(*
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
lemma length_moment_ge:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
  assumes le_k: "length s \<le> k"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
  shows "length (moment k s) = (length s)"
69
1dc801552dfd simplified Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 67
diff changeset
    22
using assms unfolding moment_def by simp
71
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
    23
*)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
lemma moment_app [simp]:
69
1dc801552dfd simplified Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 67
diff changeset
    26
  assumes ile: "i \<le> length s"
70
92ca2410b3d9 further simplificaton of Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 69
diff changeset
    27
  shows "moment i (s' @ s) = moment i s"
69
1dc801552dfd simplified Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 67
diff changeset
    28
using assms unfolding moment_def by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
70
92ca2410b3d9 further simplificaton of Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 69
diff changeset
    30
lemma moment_eq [simp]: "moment (length s) (s' @ s) = s"
69
1dc801552dfd simplified Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 67
diff changeset
    31
  unfolding moment_def by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
  by (unfold moment_def, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
lemma moment_zero [simp]: "moment 0 s = []"
69
1dc801552dfd simplified Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 67
diff changeset
    37
  by (simp add:moment_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
lemma p_split_gen: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
  "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
  (\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
proof (induct s, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
  fix a s
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
  assume ih: "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
           \<Longrightarrow> \<exists>i<length s. k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall>i'>i. Q (moment i' s))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
    and nq: "\<not> Q (moment k (a # s))" and qa: "Q (a # s)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    47
  have le_k: "k \<le> length s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
  proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
    { assume "length s < k"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
      hence "length (a#s) \<le> k" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
      from moment_ge [OF this] and nq and qa
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
      have "False" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
    } thus ?thesis by arith
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    54
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
  have nq_k: "\<not> Q (moment k s)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
  proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
    have "moment k (a#s) = moment k s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
    proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
      from moment_app [OF le_k, of "[a]"] show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
    with nq show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
  show "\<exists>i<length (a # s). k \<le> i \<and> \<not> Q (moment i (a # s)) \<and> (\<forall>i'>i. Q (moment i' (a # s)))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
  proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
    { assume "Q s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
      from ih [OF this nq_k]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
      obtain i where lti: "i < length s" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
        and nq: "\<not> Q (moment i s)" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
        and rst: "\<forall>i'>i. Q (moment i' s)" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
        and lki: "k \<le> i" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    71
      have ?thesis 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    72
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    73
        from lti have "i < length (a # s)" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    74
        moreover have " \<not> Q (moment i (a # s))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
        proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
          from lti have "i \<le> (length s)" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    77
          from moment_app [OF this, of "[a]"]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    78
          have "moment i (a # s) = moment i s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    79
          with nq show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    80
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    81
        moreover have " (\<forall>i'>i. Q (moment i' (a # s)))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    82
        proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    83
          {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    84
            fix i'
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    85
            assume lti': "i < i'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    86
            have "Q (moment i' (a # s))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
            proof(cases "length (a#s) \<le> i'")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
              case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    89
              from True have "moment i' (a#s) = a#s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
              with qa show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    91
            next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
              case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    93
              from False have "i' \<le> length s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    94
              from moment_app [OF this, of "[a]"]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    95
              have "moment i' (a#s) = moment i' s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    96
              with rst lti' show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    97
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    98
          } thus ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    99
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   100
        moreover note lki
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   101
        ultimately show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   102
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   103
    } moreover {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   104
      assume ns: "\<not> Q s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   105
      have ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   106
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   107
        let ?i = "length s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   108
        have "\<not> Q (moment ?i (a#s))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   109
        proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   110
          have "?i \<le> length s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   111
          from moment_app [OF this, of "[a]"]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   112
          have "moment ?i (a#s) = moment ?i s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   113
          moreover have "\<dots> = s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   114
          ultimately show ?thesis using ns by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   115
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   116
        moreover have "\<forall> i' > ?i. Q (moment i' (a#s))" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   117
        proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   118
          { fix i'
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   119
            assume "i' > ?i"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   120
            hence "length (a#s) \<le> i'" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   121
            from moment_ge [OF this] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   122
            have " moment i' (a # s) = a # s" .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   123
            with qa have "Q (moment i' (a#s))" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   124
          } thus ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   125
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   126
        moreover have "?i < length (a#s)" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   127
        moreover note le_k
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   128
        ultimately show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   129
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   130
    } ultimately show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   131
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   132
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   133
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   134
lemma p_split: 
70
92ca2410b3d9 further simplificaton of Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 69
diff changeset
   135
  "\<lbrakk>Q s; \<not> Q []\<rbrakk> \<Longrightarrow> 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   136
       (\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   137
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   138
  fix s Q
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   139
  assume qs: "Q s" and nq: "\<not> Q []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   140
  from nq have "\<not> Q (moment 0 s)" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   141
  from p_split_gen [of Q s 0, OF qs this]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   142
  show "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   143
    by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   144
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   145
71
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   146
lemma moment_Suc_tl:
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   147
  assumes "Suc i \<le> length s"
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   148
  shows "tl (moment (Suc i) s) = moment i s"
72
3fa70b12c117 another simplification
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 71
diff changeset
   149
  using assms unfolding moment_def rev_take
73
b0054fb0d1ce Moment.thy further improved.
zhangx
parents: 72
diff changeset
   150
  by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop)
b0054fb0d1ce Moment.thy further improved.
zhangx
parents: 72
diff changeset
   151
  
71
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   152
lemma moment_plus:
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   153
  assumes "Suc i \<le> length s"
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   154
  shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)"
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   155
proof -
73
b0054fb0d1ce Moment.thy further improved.
zhangx
parents: 72
diff changeset
   156
  have "(moment (Suc i) s) \<noteq> []" using assms 
b0054fb0d1ce Moment.thy further improved.
zhangx
parents: 72
diff changeset
   157
    by (simp add:moment_def rev_take)
71
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   158
  hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) #  tl (moment (Suc i) s)"
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   159
    by auto
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   160
  with moment_Suc_tl[OF assms]
04caf0ccb3ae some small change
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 70
diff changeset
   161
  show ?thesis by metis
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   162
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   163
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   164
end
70
92ca2410b3d9 further simplificaton of Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 69
diff changeset
   165