1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/HOLCF/ex/Loop.thy Sat Nov 27 16:08:10 2010 -0800
1.3 @@ -0,0 +1,200 @@
1.4 +(* Title: HOLCF/ex/Loop.thy
1.5 + Author: Franz Regensburger
1.6 +*)
1.7 +
1.8 +header {* Theory for a loop primitive like while *}
1.9 +
1.10 +theory Loop
1.11 +imports HOLCF
1.12 +begin
1.13 +
1.14 +definition
1.15 + step :: "('a -> tr)->('a -> 'a)->'a->'a" where
1.16 + "step = (LAM b g x. If b$x then g$x else x)"
1.17 +
1.18 +definition
1.19 + while :: "('a -> tr)->('a -> 'a)->'a->'a" where
1.20 + "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x))"
1.21 +
1.22 +(* ------------------------------------------------------------------------- *)
1.23 +(* access to definitions *)
1.24 +(* ------------------------------------------------------------------------- *)
1.25 +
1.26 +
1.27 +lemma step_def2: "step$b$g$x = If b$x then g$x else x"
1.28 +apply (unfold step_def)
1.29 +apply simp
1.30 +done
1.31 +
1.32 +lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x)"
1.33 +apply (unfold while_def)
1.34 +apply simp
1.35 +done
1.36 +
1.37 +
1.38 +(* ------------------------------------------------------------------------- *)
1.39 +(* rekursive properties of while *)
1.40 +(* ------------------------------------------------------------------------- *)
1.41 +
1.42 +lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x"
1.43 +apply (rule trans)
1.44 +apply (rule while_def2 [THEN fix_eq5])
1.45 +apply simp
1.46 +done
1.47 +
1.48 +lemma while_unfold2: "ALL x. while$b$g$x = while$b$g$(iterate k$(step$b$g)$x)"
1.49 +apply (induct_tac k)
1.50 +apply simp
1.51 +apply (rule allI)
1.52 +apply (rule trans)
1.53 +apply (rule while_unfold)
1.54 +apply (subst iterate_Suc2)
1.55 +apply (rule trans)
1.56 +apply (erule_tac [2] spec)
1.57 +apply (subst step_def2)
1.58 +apply (rule_tac p = "b$x" in trE)
1.59 +apply simp
1.60 +apply (subst while_unfold)
1.61 +apply (rule_tac s = "UU" and t = "b$UU" in ssubst)
1.62 +apply (erule strictI)
1.63 +apply simp
1.64 +apply simp
1.65 +apply simp
1.66 +apply (subst while_unfold)
1.67 +apply simp
1.68 +done
1.69 +
1.70 +lemma while_unfold3: "while$b$g$x = while$b$g$(step$b$g$x)"
1.71 +apply (rule_tac s = "while$b$g$ (iterate (Suc 0) $ (step$b$g) $x) " in trans)
1.72 +apply (rule while_unfold2 [THEN spec])
1.73 +apply simp
1.74 +done
1.75 +
1.76 +
1.77 +(* ------------------------------------------------------------------------- *)
1.78 +(* properties of while and iterations *)
1.79 +(* ------------------------------------------------------------------------- *)
1.80 +
1.81 +lemma loop_lemma1: "[| EX y. b$y=FF; iterate k$(step$b$g)$x = UU |]
1.82 + ==>iterate(Suc k)$(step$b$g)$x=UU"
1.83 +apply (simp (no_asm))
1.84 +apply (rule trans)
1.85 +apply (rule step_def2)
1.86 +apply simp
1.87 +apply (erule exE)
1.88 +apply (erule flat_codom [THEN disjE])
1.89 +apply simp_all
1.90 +done
1.91 +
1.92 +lemma loop_lemma2: "[|EX y. b$y=FF;iterate (Suc k)$(step$b$g)$x ~=UU |]==>
1.93 + iterate k$(step$b$g)$x ~=UU"
1.94 +apply (blast intro: loop_lemma1)
1.95 +done
1.96 +
1.97 +lemma loop_lemma3 [rule_format (no_asm)]:
1.98 + "[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);
1.99 + EX y. b$y=FF; INV x |]
1.100 + ==> iterate k$(step$b$g)$x ~=UU --> INV (iterate k$(step$b$g)$x)"
1.101 +apply (induct_tac "k")
1.102 +apply (simp (no_asm_simp))
1.103 +apply (intro strip)
1.104 +apply (simp (no_asm) add: step_def2)
1.105 +apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
1.106 +apply (erule notE)
1.107 +apply (simp add: step_def2)
1.108 +apply (simp (no_asm_simp))
1.109 +apply (rule mp)
1.110 +apply (erule spec)
1.111 +apply (simp (no_asm_simp) del: iterate_Suc add: loop_lemma2)
1.112 +apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
1.113 + and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
1.114 +prefer 2 apply (assumption)
1.115 +apply (simp add: step_def2)
1.116 +apply (drule (1) loop_lemma2, simp)
1.117 +done
1.118 +
1.119 +lemma loop_lemma4 [rule_format]:
1.120 + "ALL x. b$(iterate k$(step$b$g)$x)=FF --> while$b$g$x= iterate k$(step$b$g)$x"
1.121 +apply (induct_tac k)
1.122 +apply (simp (no_asm))
1.123 +apply (intro strip)
1.124 +apply (simplesubst while_unfold)
1.125 +apply simp
1.126 +apply (rule allI)
1.127 +apply (simplesubst iterate_Suc2)
1.128 +apply (intro strip)
1.129 +apply (rule trans)
1.130 +apply (rule while_unfold3)
1.131 +apply simp
1.132 +done
1.133 +
1.134 +lemma loop_lemma5 [rule_format (no_asm)]:
1.135 + "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==>
1.136 + ALL m. while$b$g$(iterate m$(step$b$g)$x)=UU"
1.137 +apply (simplesubst while_def2)
1.138 +apply (rule fix_ind)
1.139 +apply simp
1.140 +apply simp
1.141 +apply (rule allI)
1.142 +apply (simp (no_asm))
1.143 +apply (rule_tac p = "b$ (iterate m$ (step$b$g) $x) " in trE)
1.144 +apply (simp (no_asm_simp))
1.145 +apply (simp (no_asm_simp))
1.146 +apply (rule_tac s = "xa$ (iterate (Suc m) $ (step$b$g) $x) " in trans)
1.147 +apply (erule_tac [2] spec)
1.148 +apply (rule cfun_arg_cong)
1.149 +apply (rule trans)
1.150 +apply (rule_tac [2] iterate_Suc [symmetric])
1.151 +apply (simp add: step_def2)
1.152 +apply blast
1.153 +done
1.154 +
1.155 +lemma loop_lemma6: "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==> while$b$g$x=UU"
1.156 +apply (rule_tac t = "x" in iterate_0 [THEN subst])
1.157 +apply (erule loop_lemma5)
1.158 +done
1.159 +
1.160 +lemma loop_lemma7: "while$b$g$x ~= UU ==> EX k. b$(iterate k$(step$b$g)$x) = FF"
1.161 +apply (blast intro: loop_lemma6)
1.162 +done
1.163 +
1.164 +
1.165 +(* ------------------------------------------------------------------------- *)
1.166 +(* an invariant rule for loops *)
1.167 +(* ------------------------------------------------------------------------- *)
1.168 +
1.169 +lemma loop_inv2:
1.170 +"[| (ALL y. INV y & b$y=TT & g$y ~= UU --> INV (g$y));
1.171 + (ALL y. INV y & b$y=FF --> Q y);
1.172 + INV x; while$b$g$x~=UU |] ==> Q (while$b$g$x)"
1.173 +apply (rule_tac P = "%k. b$ (iterate k$ (step$b$g) $x) =FF" in exE)
1.174 +apply (erule loop_lemma7)
1.175 +apply (simplesubst loop_lemma4)
1.176 +apply assumption
1.177 +apply (drule spec, erule mp)
1.178 +apply (rule conjI)
1.179 +prefer 2 apply (assumption)
1.180 +apply (rule loop_lemma3)
1.181 +apply assumption
1.182 +apply (blast intro: loop_lemma6)
1.183 +apply assumption
1.184 +apply (rotate_tac -1)
1.185 +apply (simp add: loop_lemma4)
1.186 +done
1.187 +
1.188 +lemma loop_inv:
1.189 + assumes premP: "P(x)"
1.190 + and premI: "!!y. P y ==> INV y"
1.191 + and premTT: "!!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y)"
1.192 + and premFF: "!!y. [| INV y; b$y=FF|] ==> Q y"
1.193 + and premW: "while$b$g$x ~= UU"
1.194 + shows "Q (while$b$g$x)"
1.195 +apply (rule loop_inv2)
1.196 +apply (rule_tac [3] premP [THEN premI])
1.197 +apply (rule_tac [3] premW)
1.198 +apply (blast intro: premTT)
1.199 +apply (blast intro: premFF)
1.200 +done
1.201 +
1.202 +end
1.203 +