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