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