src/HOL/HOLCF/ex/Loop.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
permissions -rw-r--r--
Quotient_Info stores only relation maps
wenzelm@42151
     1
(*  Title:      HOL/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
huffman@40322
    13
  "step = (LAM b g x. If b$x then g$x else x)"
wenzelm@19742
    14
wenzelm@21404
    15
definition
wenzelm@21404
    16
  while :: "('a -> tr)->('a -> 'a)->'a->'a" where
huffman@40322
    17
  "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x))"
nipkow@244
    18
wenzelm@19742
    19
(* ------------------------------------------------------------------------- *)
wenzelm@19742
    20
(* access to definitions                                                     *)
wenzelm@19742
    21
(* ------------------------------------------------------------------------- *)
wenzelm@19742
    22
wenzelm@19742
    23
huffman@40322
    24
lemma step_def2: "step$b$g$x = If b$x then g$x else x"
wenzelm@19742
    25
apply (unfold step_def)
wenzelm@19742
    26
apply simp
wenzelm@19742
    27
done
wenzelm@19742
    28
huffman@40322
    29
lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x)"
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
huffman@40322
    39
lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x"
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)
huffman@40429
    50
apply (rule while_unfold)
wenzelm@19742
    51
apply (subst iterate_Suc2)
wenzelm@19742
    52
apply (rule trans)
wenzelm@19742
    53
apply (erule_tac [2] spec)
wenzelm@19742
    54
apply (subst step_def2)
wenzelm@19742
    55
apply (rule_tac p = "b$x" in trE)
wenzelm@19742
    56
apply simp
wenzelm@19742
    57
apply (subst while_unfold)
wenzelm@19742
    58
apply (rule_tac s = "UU" and t = "b$UU" in ssubst)
huffman@40429
    59
apply (erule strictI)
wenzelm@19742
    60
apply simp
wenzelm@19742
    61
apply simp
wenzelm@19742
    62
apply simp
wenzelm@19742
    63
apply (subst while_unfold)
wenzelm@19742
    64
apply simp
wenzelm@19742
    65
done
wenzelm@19742
    66
wenzelm@19742
    67
lemma while_unfold3: "while$b$g$x = while$b$g$(step$b$g$x)"
wenzelm@19742
    68
apply (rule_tac s = "while$b$g$ (iterate (Suc 0) $ (step$b$g) $x) " in trans)
wenzelm@19742
    69
apply (rule while_unfold2 [THEN spec])
wenzelm@19742
    70
apply simp
wenzelm@19742
    71
done
wenzelm@19742
    72
wenzelm@19742
    73
wenzelm@19742
    74
(* ------------------------------------------------------------------------- *)
wenzelm@19742
    75
(* properties of while and iterations                                        *)
wenzelm@19742
    76
(* ------------------------------------------------------------------------- *)
wenzelm@19742
    77
wenzelm@19742
    78
lemma loop_lemma1: "[| EX y. b$y=FF; iterate k$(step$b$g)$x = UU |]
wenzelm@19742
    79
     ==>iterate(Suc k)$(step$b$g)$x=UU"
wenzelm@19742
    80
apply (simp (no_asm))
wenzelm@19742
    81
apply (rule trans)
wenzelm@19742
    82
apply (rule step_def2)
wenzelm@19742
    83
apply simp
wenzelm@19742
    84
apply (erule exE)
wenzelm@19742
    85
apply (erule flat_codom [THEN disjE])
wenzelm@19742
    86
apply simp_all
wenzelm@19742
    87
done
wenzelm@19742
    88
wenzelm@19742
    89
lemma loop_lemma2: "[|EX y. b$y=FF;iterate (Suc k)$(step$b$g)$x ~=UU |]==>
wenzelm@19742
    90
      iterate k$(step$b$g)$x ~=UU"
wenzelm@19742
    91
apply (blast intro: loop_lemma1)
wenzelm@19742
    92
done
wenzelm@19742
    93
wenzelm@19742
    94
lemma loop_lemma3 [rule_format (no_asm)]:
wenzelm@19742
    95
  "[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);
wenzelm@19742
    96
         EX y. b$y=FF; INV x |]
wenzelm@19742
    97
      ==> iterate k$(step$b$g)$x ~=UU --> INV (iterate k$(step$b$g)$x)"
wenzelm@19742
    98
apply (induct_tac "k")
wenzelm@19742
    99
apply (simp (no_asm_simp))
wenzelm@19742
   100
apply (intro strip)
wenzelm@19742
   101
apply (simp (no_asm) add: step_def2)
wenzelm@19742
   102
apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
wenzelm@19742
   103
apply (erule notE)
huffman@40028
   104
apply (simp add: step_def2)
huffman@40028
   105
apply (simp (no_asm_simp))
wenzelm@19742
   106
apply (rule mp)
wenzelm@19742
   107
apply (erule spec)
huffman@40028
   108
apply (simp (no_asm_simp) del: iterate_Suc add: loop_lemma2)
wenzelm@19742
   109
apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
wenzelm@19742
   110
  and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
wenzelm@19742
   111
prefer 2 apply (assumption)
wenzelm@19742
   112
apply (simp add: step_def2)
huffman@35170
   113
apply (drule (1) loop_lemma2, simp)
wenzelm@19742
   114
done
wenzelm@19742
   115
wenzelm@19742
   116
lemma loop_lemma4 [rule_format]:
wenzelm@19742
   117
  "ALL x. b$(iterate k$(step$b$g)$x)=FF --> while$b$g$x= iterate k$(step$b$g)$x"
wenzelm@19742
   118
apply (induct_tac k)
wenzelm@19742
   119
apply (simp (no_asm))
wenzelm@19742
   120
apply (intro strip)
wenzelm@19742
   121
apply (simplesubst while_unfold)
wenzelm@19742
   122
apply simp
wenzelm@19742
   123
apply (rule allI)
wenzelm@19742
   124
apply (simplesubst iterate_Suc2)
wenzelm@19742
   125
apply (intro strip)
wenzelm@19742
   126
apply (rule trans)
wenzelm@19742
   127
apply (rule while_unfold3)
wenzelm@19742
   128
apply simp
wenzelm@19742
   129
done
wenzelm@19742
   130
wenzelm@19742
   131
lemma loop_lemma5 [rule_format (no_asm)]:
wenzelm@19742
   132
  "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==>
wenzelm@19742
   133
    ALL m. while$b$g$(iterate m$(step$b$g)$x)=UU"
wenzelm@19742
   134
apply (simplesubst while_def2)
wenzelm@19742
   135
apply (rule fix_ind)
huffman@35948
   136
apply simp
huffman@35948
   137
apply simp
wenzelm@19742
   138
apply (rule allI)
wenzelm@19742
   139
apply (simp (no_asm))
wenzelm@19742
   140
apply (rule_tac p = "b$ (iterate m$ (step$b$g) $x) " in trE)
wenzelm@19742
   141
apply (simp (no_asm_simp))
wenzelm@19742
   142
apply (simp (no_asm_simp))
wenzelm@19742
   143
apply (rule_tac s = "xa$ (iterate (Suc m) $ (step$b$g) $x) " in trans)
wenzelm@19742
   144
apply (erule_tac [2] spec)
wenzelm@19742
   145
apply (rule cfun_arg_cong)
wenzelm@19742
   146
apply (rule trans)
wenzelm@19742
   147
apply (rule_tac [2] iterate_Suc [symmetric])
wenzelm@19742
   148
apply (simp add: step_def2)
wenzelm@19742
   149
apply blast
wenzelm@19742
   150
done
wenzelm@19742
   151
wenzelm@19742
   152
lemma loop_lemma6: "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==> while$b$g$x=UU"
wenzelm@19742
   153
apply (rule_tac t = "x" in iterate_0 [THEN subst])
wenzelm@19742
   154
apply (erule loop_lemma5)
wenzelm@19742
   155
done
wenzelm@19742
   156
wenzelm@19742
   157
lemma loop_lemma7: "while$b$g$x ~= UU ==> EX k. b$(iterate k$(step$b$g)$x) = FF"
wenzelm@19742
   158
apply (blast intro: loop_lemma6)
wenzelm@19742
   159
done
wenzelm@19742
   160
wenzelm@19742
   161
wenzelm@19742
   162
(* ------------------------------------------------------------------------- *)
wenzelm@19742
   163
(* an invariant rule for loops                                               *)
wenzelm@19742
   164
(* ------------------------------------------------------------------------- *)
wenzelm@19742
   165
wenzelm@19742
   166
lemma loop_inv2:
wenzelm@19742
   167
"[| (ALL y. INV y & b$y=TT & g$y ~= UU --> INV (g$y));
wenzelm@19742
   168
    (ALL y. INV y & b$y=FF --> Q y);
wenzelm@19742
   169
    INV x; while$b$g$x~=UU |] ==> Q (while$b$g$x)"
wenzelm@19742
   170
apply (rule_tac P = "%k. b$ (iterate k$ (step$b$g) $x) =FF" in exE)
wenzelm@19742
   171
apply (erule loop_lemma7)
wenzelm@19742
   172
apply (simplesubst loop_lemma4)
wenzelm@19742
   173
apply assumption
wenzelm@19742
   174
apply (drule spec, erule mp)
wenzelm@19742
   175
apply (rule conjI)
wenzelm@19742
   176
prefer 2 apply (assumption)
wenzelm@19742
   177
apply (rule loop_lemma3)
wenzelm@19742
   178
apply assumption
wenzelm@19742
   179
apply (blast intro: loop_lemma6)
wenzelm@19742
   180
apply assumption
wenzelm@19742
   181
apply (rotate_tac -1)
wenzelm@19742
   182
apply (simp add: loop_lemma4)
wenzelm@19742
   183
done
wenzelm@19742
   184
wenzelm@19742
   185
lemma loop_inv:
wenzelm@19742
   186
  assumes premP: "P(x)"
wenzelm@19742
   187
    and premI: "!!y. P y ==> INV y"
wenzelm@19742
   188
    and premTT: "!!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y)"
wenzelm@19742
   189
    and premFF: "!!y. [| INV y; b$y=FF|] ==> Q y"
wenzelm@19742
   190
    and premW: "while$b$g$x ~= UU"
wenzelm@19742
   191
  shows "Q (while$b$g$x)"
wenzelm@19742
   192
apply (rule loop_inv2)
wenzelm@19742
   193
apply (rule_tac [3] premP [THEN premI])
wenzelm@19742
   194
apply (rule_tac [3] premW)
wenzelm@19742
   195
apply (blast intro: premTT)
wenzelm@19742
   196
apply (blast intro: premFF)
wenzelm@19742
   197
done
nipkow@244
   198
nipkow@244
   199
end
wenzelm@17291
   200