src/HOLCF/ex/Loop.thy
author huffman
Sat Oct 16 17:09:57 2010 -0700 (2010-10-16)
changeset 40028 9ee4e0ab2964
parent 39159 0dec18004e75
child 40322 707eb30e8a53
permissions -rw-r--r--
remove old uses of 'simp_tac HOLCF_ss'
clasohm@1479
     1
(*  Title:      HOLCF/ex/Loop.thy
clasohm@1479
     2
    Author:     Franz Regensburger
nipkow@244
     3
*)
nipkow@244
     4
wenzelm@17291
     5
header {* Theory for a loop primitive like while *}
nipkow@244
     6
wenzelm@17291
     7
theory Loop
wenzelm@17291
     8
imports HOLCF
wenzelm@17291
     9
begin
nipkow@244
    10
wenzelm@19763
    11
definition
wenzelm@21404
    12
  step  :: "('a -> tr)->('a -> 'a)->'a->'a" where
wenzelm@19763
    13
  "step = (LAM b g x. If b$x then g$x else x fi)"
wenzelm@19742
    14
wenzelm@21404
    15
definition
wenzelm@21404
    16
  while :: "('a -> tr)->('a -> 'a)->'a->'a" where
wenzelm@19763
    17
  "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))"
nipkow@244
    18
wenzelm@19742
    19
(* ------------------------------------------------------------------------- *)
wenzelm@19742
    20
(* access to definitions                                                     *)
wenzelm@19742
    21
(* ------------------------------------------------------------------------- *)
wenzelm@19742
    22
wenzelm@19742
    23
wenzelm@19742
    24
lemma step_def2: "step$b$g$x = If b$x then g$x else x fi"
wenzelm@19742
    25
apply (unfold step_def)
wenzelm@19742
    26
apply simp
wenzelm@19742
    27
done
wenzelm@19742
    28
wenzelm@19742
    29
lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)"
wenzelm@19742
    30
apply (unfold while_def)
wenzelm@19742
    31
apply simp
wenzelm@19742
    32
done
wenzelm@19742
    33
wenzelm@19742
    34
wenzelm@19742
    35
(* ------------------------------------------------------------------------- *)
wenzelm@19742
    36
(* rekursive properties of while                                             *)
wenzelm@19742
    37
(* ------------------------------------------------------------------------- *)
wenzelm@19742
    38
wenzelm@19742
    39
lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x fi"
wenzelm@19742
    40
apply (rule trans)
wenzelm@19742
    41
apply (rule while_def2 [THEN fix_eq5])
wenzelm@19742
    42
apply simp
wenzelm@19742
    43
done
wenzelm@19742
    44
wenzelm@19742
    45
lemma while_unfold2: "ALL x. while$b$g$x = while$b$g$(iterate k$(step$b$g)$x)"
wenzelm@19742
    46
apply (induct_tac k)
wenzelm@19742
    47
apply simp
wenzelm@19742
    48
apply (rule allI)
wenzelm@19742
    49
apply (rule trans)
wenzelm@19742
    50
apply (subst while_unfold)
wenzelm@19742
    51
apply (rule_tac [2] refl)
wenzelm@19742
    52
apply (subst iterate_Suc2)
wenzelm@19742
    53
apply (rule trans)
wenzelm@19742
    54
apply (erule_tac [2] spec)
wenzelm@19742
    55
apply (subst step_def2)
wenzelm@19742
    56
apply (rule_tac p = "b$x" in trE)
wenzelm@19742
    57
apply simp
wenzelm@19742
    58
apply (subst while_unfold)
wenzelm@19742
    59
apply (rule_tac s = "UU" and t = "b$UU" in ssubst)
wenzelm@19742
    60
apply (erule flat_codom [THEN disjE])
wenzelm@19742
    61
apply assumption
wenzelm@19742
    62
apply (erule spec)
wenzelm@19742
    63
apply simp
wenzelm@19742
    64
apply simp
wenzelm@19742
    65
apply simp
wenzelm@19742
    66
apply (subst while_unfold)
wenzelm@19742
    67
apply simp
wenzelm@19742
    68
done
wenzelm@19742
    69
wenzelm@19742
    70
lemma while_unfold3: "while$b$g$x = while$b$g$(step$b$g$x)"
wenzelm@19742
    71
apply (rule_tac s = "while$b$g$ (iterate (Suc 0) $ (step$b$g) $x) " in trans)
wenzelm@19742
    72
apply (rule while_unfold2 [THEN spec])
wenzelm@19742
    73
apply simp
wenzelm@19742
    74
done
wenzelm@19742
    75
wenzelm@19742
    76
wenzelm@19742
    77
(* ------------------------------------------------------------------------- *)
wenzelm@19742
    78
(* properties of while and iterations                                        *)
wenzelm@19742
    79
(* ------------------------------------------------------------------------- *)
wenzelm@19742
    80
wenzelm@19742
    81
lemma loop_lemma1: "[| EX y. b$y=FF; iterate k$(step$b$g)$x = UU |]
wenzelm@19742
    82
     ==>iterate(Suc k)$(step$b$g)$x=UU"
wenzelm@19742
    83
apply (simp (no_asm))
wenzelm@19742
    84
apply (rule trans)
wenzelm@19742
    85
apply (rule step_def2)
wenzelm@19742
    86
apply simp
wenzelm@19742
    87
apply (erule exE)
wenzelm@19742
    88
apply (erule flat_codom [THEN disjE])
wenzelm@19742
    89
apply simp_all
wenzelm@19742
    90
done
wenzelm@19742
    91
wenzelm@19742
    92
lemma loop_lemma2: "[|EX y. b$y=FF;iterate (Suc k)$(step$b$g)$x ~=UU |]==>
wenzelm@19742
    93
      iterate k$(step$b$g)$x ~=UU"
wenzelm@19742
    94
apply (blast intro: loop_lemma1)
wenzelm@19742
    95
done
wenzelm@19742
    96
wenzelm@19742
    97
lemma loop_lemma3 [rule_format (no_asm)]:
wenzelm@19742
    98
  "[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);
wenzelm@19742
    99
         EX y. b$y=FF; INV x |]
wenzelm@19742
   100
      ==> iterate k$(step$b$g)$x ~=UU --> INV (iterate k$(step$b$g)$x)"
wenzelm@19742
   101
apply (induct_tac "k")
wenzelm@19742
   102
apply (simp (no_asm_simp))
wenzelm@19742
   103
apply (intro strip)
wenzelm@19742
   104
apply (simp (no_asm) add: step_def2)
wenzelm@19742
   105
apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
wenzelm@19742
   106
apply (erule notE)
huffman@40028
   107
apply (simp add: step_def2)
huffman@40028
   108
apply (simp (no_asm_simp))
wenzelm@19742
   109
apply (rule mp)
wenzelm@19742
   110
apply (erule spec)
huffman@40028
   111
apply (simp (no_asm_simp) del: iterate_Suc add: loop_lemma2)
wenzelm@19742
   112
apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
wenzelm@19742
   113
  and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
wenzelm@19742
   114
prefer 2 apply (assumption)
wenzelm@19742
   115
apply (simp add: step_def2)
huffman@35170
   116
apply (drule (1) loop_lemma2, simp)
wenzelm@19742
   117
done
wenzelm@19742
   118
wenzelm@19742
   119
lemma loop_lemma4 [rule_format]:
wenzelm@19742
   120
  "ALL x. b$(iterate k$(step$b$g)$x)=FF --> while$b$g$x= iterate k$(step$b$g)$x"
wenzelm@19742
   121
apply (induct_tac k)
wenzelm@19742
   122
apply (simp (no_asm))
wenzelm@19742
   123
apply (intro strip)
wenzelm@19742
   124
apply (simplesubst while_unfold)
wenzelm@19742
   125
apply simp
wenzelm@19742
   126
apply (rule allI)
wenzelm@19742
   127
apply (simplesubst iterate_Suc2)
wenzelm@19742
   128
apply (intro strip)
wenzelm@19742
   129
apply (rule trans)
wenzelm@19742
   130
apply (rule while_unfold3)
wenzelm@19742
   131
apply simp
wenzelm@19742
   132
done
wenzelm@19742
   133
wenzelm@19742
   134
lemma loop_lemma5 [rule_format (no_asm)]:
wenzelm@19742
   135
  "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==>
wenzelm@19742
   136
    ALL m. while$b$g$(iterate m$(step$b$g)$x)=UU"
wenzelm@19742
   137
apply (simplesubst while_def2)
wenzelm@19742
   138
apply (rule fix_ind)
huffman@35948
   139
apply simp
huffman@35948
   140
apply simp
wenzelm@19742
   141
apply (rule allI)
wenzelm@19742
   142
apply (simp (no_asm))
wenzelm@19742
   143
apply (rule_tac p = "b$ (iterate m$ (step$b$g) $x) " in trE)
wenzelm@19742
   144
apply (simp (no_asm_simp))
wenzelm@19742
   145
apply (simp (no_asm_simp))
wenzelm@19742
   146
apply (rule_tac s = "xa$ (iterate (Suc m) $ (step$b$g) $x) " in trans)
wenzelm@19742
   147
apply (erule_tac [2] spec)
wenzelm@19742
   148
apply (rule cfun_arg_cong)
wenzelm@19742
   149
apply (rule trans)
wenzelm@19742
   150
apply (rule_tac [2] iterate_Suc [symmetric])
wenzelm@19742
   151
apply (simp add: step_def2)
wenzelm@19742
   152
apply blast
wenzelm@19742
   153
done
wenzelm@19742
   154
wenzelm@19742
   155
lemma loop_lemma6: "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==> while$b$g$x=UU"
wenzelm@19742
   156
apply (rule_tac t = "x" in iterate_0 [THEN subst])
wenzelm@19742
   157
apply (erule loop_lemma5)
wenzelm@19742
   158
done
wenzelm@19742
   159
wenzelm@19742
   160
lemma loop_lemma7: "while$b$g$x ~= UU ==> EX k. b$(iterate k$(step$b$g)$x) = FF"
wenzelm@19742
   161
apply (blast intro: loop_lemma6)
wenzelm@19742
   162
done
wenzelm@19742
   163
wenzelm@19742
   164
wenzelm@19742
   165
(* ------------------------------------------------------------------------- *)
wenzelm@19742
   166
(* an invariant rule for loops                                               *)
wenzelm@19742
   167
(* ------------------------------------------------------------------------- *)
wenzelm@19742
   168
wenzelm@19742
   169
lemma loop_inv2:
wenzelm@19742
   170
"[| (ALL y. INV y & b$y=TT & g$y ~= UU --> INV (g$y));
wenzelm@19742
   171
    (ALL y. INV y & b$y=FF --> Q y);
wenzelm@19742
   172
    INV x; while$b$g$x~=UU |] ==> Q (while$b$g$x)"
wenzelm@19742
   173
apply (rule_tac P = "%k. b$ (iterate k$ (step$b$g) $x) =FF" in exE)
wenzelm@19742
   174
apply (erule loop_lemma7)
wenzelm@19742
   175
apply (simplesubst loop_lemma4)
wenzelm@19742
   176
apply assumption
wenzelm@19742
   177
apply (drule spec, erule mp)
wenzelm@19742
   178
apply (rule conjI)
wenzelm@19742
   179
prefer 2 apply (assumption)
wenzelm@19742
   180
apply (rule loop_lemma3)
wenzelm@19742
   181
apply assumption
wenzelm@19742
   182
apply (blast intro: loop_lemma6)
wenzelm@19742
   183
apply assumption
wenzelm@19742
   184
apply (rotate_tac -1)
wenzelm@19742
   185
apply (simp add: loop_lemma4)
wenzelm@19742
   186
done
wenzelm@19742
   187
wenzelm@19742
   188
lemma loop_inv:
wenzelm@19742
   189
  assumes premP: "P(x)"
wenzelm@19742
   190
    and premI: "!!y. P y ==> INV y"
wenzelm@19742
   191
    and premTT: "!!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y)"
wenzelm@19742
   192
    and premFF: "!!y. [| INV y; b$y=FF|] ==> Q y"
wenzelm@19742
   193
    and premW: "while$b$g$x ~= UU"
wenzelm@19742
   194
  shows "Q (while$b$g$x)"
wenzelm@19742
   195
apply (rule loop_inv2)
wenzelm@19742
   196
apply (rule_tac [3] premP [THEN premI])
wenzelm@19742
   197
apply (rule_tac [3] premW)
wenzelm@19742
   198
apply (blast intro: premTT)
wenzelm@19742
   199
apply (blast intro: premFF)
wenzelm@19742
   200
done
nipkow@244
   201
nipkow@244
   202
end
wenzelm@17291
   203