src/HOLCF/ex/Hoare.ML
changeset 10835 f4745d77e620
parent 9265 35aab1c9c08c
child 13454 01e2496dee05
     1.1 --- a/src/HOLCF/ex/Hoare.ML	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/ex/Hoare.ML	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -14,21 +14,21 @@
     1.4  by (fast_tac HOL_cs 1);
     1.5  qed "hoare_lemma2";
     1.6  
     1.7 -Goal " (ALL k. b1`(iterate k g x) = TT) | (EX k. b1`(iterate k g x)~=TT)";
     1.8 +Goal " (ALL k. b1$(iterate k g x) = TT) | (EX k. b1$(iterate k g x)~=TT)";
     1.9  by (fast_tac HOL_cs 1);
    1.10  qed "hoare_lemma3";
    1.11  
    1.12 -Goal "(EX k. b1`(iterate k g x) ~= TT) ==> \
    1.13 -\ EX k. b1`(iterate k g x) = FF | b1`(iterate k g x) = UU";
    1.14 +Goal "(EX k. b1$(iterate k g x) ~= TT) ==> \
    1.15 +\ EX k. b1$(iterate k g x) = FF | b1$(iterate k g x) = UU";
    1.16  by (etac exE 1);
    1.17  by (rtac exI 1);
    1.18  by (rtac hoare_lemma2 1);
    1.19  by (atac 1);
    1.20  qed "hoare_lemma4";
    1.21  
    1.22 -Goal "[|(EX k. b1`(iterate k g x) ~= TT);\
    1.23 -\   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
    1.24 -\ b1`(iterate k g x)=FF | b1`(iterate k g x)=UU";
    1.25 +Goal "[|(EX k. b1$(iterate k g x) ~= TT);\
    1.26 +\   k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \
    1.27 +\ b1$(iterate k g x)=FF | b1$(iterate k g x)=UU";
    1.28  by (hyp_subst_tac 1);
    1.29  by (rtac hoare_lemma2 1);
    1.30  by (etac exE 1);
    1.31 @@ -45,13 +45,13 @@
    1.32  by (resolve_tac dist_eq_tr 1);
    1.33  qed "hoare_lemma7";
    1.34  
    1.35 -Goal "[|(EX k. b1`(iterate k g x) ~= TT);\
    1.36 -\   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
    1.37 -\ ALL m. m < k --> b1`(iterate m g x)=TT";
    1.38 +Goal "[|(EX k. b1$(iterate k g x) ~= TT);\
    1.39 +\   k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \
    1.40 +\ ALL m. m < k --> b1$(iterate m g x)=TT";
    1.41  by (hyp_subst_tac 1);
    1.42  by (etac exE 1);
    1.43  by (strip_tac 1);
    1.44 -by (res_inst_tac [("p","b1`(iterate m g x)")] trE 1);
    1.45 +by (res_inst_tac [("p","b1$(iterate m g x)")] trE 1);
    1.46  by (atac 2);
    1.47  by (rtac (le_less_trans RS less_irrefl) 1);
    1.48  by (atac 2);
    1.49 @@ -64,7 +64,7 @@
    1.50  qed "hoare_lemma8";
    1.51  
    1.52  
    1.53 -Goal "f`(y::'a)=(UU::tr) ==> f`UU = UU";
    1.54 +Goal "f$(y::'a)=(UU::tr) ==> f$UU = UU";
    1.55  by (etac (flat_codom RS disjE) 1);
    1.56  by Auto_tac;  
    1.57  qed "hoare_lemma28";
    1.58 @@ -72,28 +72,28 @@
    1.59  
    1.60  (* ----- access to definitions ----- *)
    1.61  
    1.62 -Goal "p`x = If b1`x then p`(g`x) else x fi";
    1.63 +Goal "p$x = If b1$x then p$(g$x) else x fi";
    1.64  by (fix_tac3 p_def 1);
    1.65  by (Simp_tac 1);
    1.66  qed "p_def3";
    1.67  
    1.68 -Goal "q`x = If b1`x orelse b2`x then q`(g`x) else x fi";
    1.69 +Goal "q$x = If b1$x orelse b2$x then q$(g$x) else x fi";
    1.70  by (fix_tac3 q_def 1);
    1.71  by (Simp_tac 1);
    1.72  qed "q_def3";
    1.73  
    1.74  (** --------- proves about iterations of p and q ---------- **)
    1.75  
    1.76 -Goal "(ALL m. m< Suc k --> b1`(iterate m g x)=TT) -->\
    1.77 -\  p`(iterate k g x)=p`x";
    1.78 +Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) -->\
    1.79 +\  p$(iterate k g x)=p$x";
    1.80  by (nat_ind_tac "k" 1);
    1.81  by (Simp_tac 1);
    1.82  by (Simp_tac 1);
    1.83  by (strip_tac 1);
    1.84 -by (res_inst_tac [("s","p`(iterate k g x)")] trans 1);
    1.85 +by (res_inst_tac [("s","p$(iterate k g x)")] trans 1);
    1.86  by (rtac trans 1);
    1.87  by (rtac (p_def3 RS sym) 2);
    1.88 -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
    1.89 +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
    1.90  by (rtac mp 1);
    1.91  by (etac spec 1);
    1.92  by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    1.93 @@ -106,16 +106,16 @@
    1.94  by (Simp_tac 1);
    1.95  qed "hoare_lemma9";
    1.96  
    1.97 -Goal "(ALL m. m< Suc k --> b1`(iterate m g x)=TT) --> \
    1.98 -\ q`(iterate k g x)=q`x";
    1.99 +Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) --> \
   1.100 +\ q$(iterate k g x)=q$x";
   1.101  by (nat_ind_tac "k" 1);
   1.102  by (Simp_tac 1);
   1.103  by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   1.104  by (strip_tac 1);
   1.105 -by (res_inst_tac [("s","q`(iterate k g x)")] trans 1);
   1.106 +by (res_inst_tac [("s","q$(iterate k g x)")] trans 1);
   1.107  by (rtac trans 1);
   1.108  by (rtac (q_def3 RS sym) 2);
   1.109 -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
   1.110 +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
   1.111  by (fast_tac HOL_cs 1);
   1.112  by (simp_tac HOLCF_ss 1);
   1.113  by (etac mp 1);
   1.114 @@ -123,20 +123,20 @@
   1.115  by (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1);
   1.116  qed "hoare_lemma24";
   1.117  
   1.118 -(* -------- results about p for case (EX k. b1`(iterate k g x)~=TT) ------- *)
   1.119 +(* -------- results about p for case (EX k. b1$(iterate k g x)~=TT) ------- *)
   1.120  
   1.121  
   1.122  val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
   1.123  (* 
   1.124 -val hoare_lemma10 = "[| EX k. b1`(iterate k g ?x1) ~= TT;
   1.125 -    Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
   1.126 - p`(iterate ?k3 g ?x1) = p`?x1" : thm
   1.127 +val hoare_lemma10 = "[| EX k. b1$(iterate k g ?x1) ~= TT;
   1.128 +    Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==>
   1.129 + p$(iterate ?k3 g ?x1) = p$?x1" : thm
   1.130  
   1.131  *)
   1.132  
   1.133 -Goal "(EX n. b1`(iterate n g x) ~= TT) ==>\
   1.134 -\ k=(LEAST n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
   1.135 -\ --> p`x = iterate k g x";
   1.136 +Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
   1.137 +\ k=(LEAST n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x)=FF \
   1.138 +\ --> p$x = iterate k g x";
   1.139  by (case_tac "k" 1);
   1.140  by (hyp_subst_tac 1);
   1.141  by (Simp_tac 1);
   1.142 @@ -153,7 +153,7 @@
   1.143  by (atac 1);
   1.144  by (rtac trans 1);
   1.145  by (rtac p_def3 1);
   1.146 -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
   1.147 +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
   1.148  by (rtac (hoare_lemma8 RS spec RS mp) 1);
   1.149  by (atac 1);
   1.150  by (atac 1);
   1.151 @@ -166,9 +166,9 @@
   1.152  by (simp_tac HOLCF_ss 1);
   1.153  qed "hoare_lemma11";
   1.154  
   1.155 -Goal "(EX n. b1`(iterate n g x) ~= TT) ==>\
   1.156 -\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
   1.157 -\ --> p`x = UU";
   1.158 +Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
   1.159 +\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \
   1.160 +\ --> p$x = UU";
   1.161  by (case_tac "k" 1);
   1.162  by (hyp_subst_tac 1);
   1.163  by (Simp_tac 1);
   1.164 @@ -187,7 +187,7 @@
   1.165  by (atac 1);
   1.166  by (rtac trans 1);
   1.167  by (rtac p_def3 1);
   1.168 -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
   1.169 +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
   1.170  by (rtac (hoare_lemma8 RS spec RS mp) 1);
   1.171  by (atac 1);
   1.172  by (atac 1);
   1.173 @@ -198,9 +198,9 @@
   1.174  by (asm_simp_tac HOLCF_ss 1);
   1.175  qed "hoare_lemma12";
   1.176  
   1.177 -(* -------- results about p for case  (ALL k. b1`(iterate k g x)=TT) ------- *)
   1.178 +(* -------- results about p for case  (ALL k. b1$(iterate k g x)=TT) ------- *)
   1.179  
   1.180 -Goal "(ALL k. b1`(iterate k g x)=TT) ==> ALL k. p`(iterate k g x) = UU";
   1.181 +Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. p$(iterate k g x) = UU";
   1.182  by (rtac (p_def RS def_fix_ind) 1);
   1.183  by (rtac adm_all 1);
   1.184  by (rtac allI 1);
   1.185 @@ -211,21 +211,21 @@
   1.186  by (rtac refl 1);
   1.187  by (Simp_tac 1);
   1.188  by (rtac allI 1);
   1.189 -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
   1.190 +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
   1.191  by (etac spec 1);
   1.192  by (asm_simp_tac HOLCF_ss 1);
   1.193  by (rtac (iterate_Suc RS subst) 1);
   1.194  by (etac spec 1);
   1.195  qed "fernpass_lemma";
   1.196  
   1.197 -Goal "(ALL k. b1`(iterate k g x)=TT) ==> p`x = UU";
   1.198 +Goal "(ALL k. b1$(iterate k g x)=TT) ==> p$x = UU";
   1.199  by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
   1.200  by (etac (fernpass_lemma RS spec) 1);
   1.201  qed "hoare_lemma16";
   1.202  
   1.203 -(* -------- results about q for case  (ALL k. b1`(iterate k g x)=TT) ------- *)
   1.204 +(* -------- results about q for case  (ALL k. b1$(iterate k g x)=TT) ------- *)
   1.205  
   1.206 -Goal "(ALL k. b1`(iterate k g x)=TT) ==> ALL k. q`(iterate k g x) = UU";
   1.207 +Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. q$(iterate k g x) = UU";
   1.208  by (rtac (q_def RS def_fix_ind) 1);
   1.209  by (rtac adm_all 1);
   1.210  by (rtac allI 1);
   1.211 @@ -236,25 +236,25 @@
   1.212  by (rtac refl 1);
   1.213  by (rtac allI 1);
   1.214  by (Simp_tac 1);
   1.215 -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
   1.216 +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
   1.217  by (etac spec 1);
   1.218  by (asm_simp_tac HOLCF_ss 1);
   1.219  by (rtac (iterate_Suc RS subst) 1);
   1.220  by (etac spec 1);
   1.221  qed "hoare_lemma17";
   1.222  
   1.223 -Goal "(ALL k. b1`(iterate k g x)=TT) ==> q`x = UU";
   1.224 +Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$x = UU";
   1.225  by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
   1.226  by (etac (hoare_lemma17 RS spec) 1);
   1.227  qed "hoare_lemma18";
   1.228  
   1.229 -Goal "(ALL k. (b1::'a->tr)`(iterate k g x)=TT) ==> b1`(UU::'a) = UU | (ALL y. b1`(y::'a)=TT)";
   1.230 +Goal "(ALL k. (b1::'a->tr)$(iterate k g x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)";
   1.231  by (rtac (flat_codom) 1);
   1.232  by (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1);
   1.233  by (etac spec 1);
   1.234  qed "hoare_lemma19";
   1.235  
   1.236 -Goal "(ALL y. b1`(y::'a)=TT) ==> ALL k. q`(iterate k g (x::'a)) = UU";
   1.237 +Goal "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k g (x::'a)) = UU";
   1.238  by (rtac (q_def RS def_fix_ind) 1);
   1.239  by (rtac adm_all 1);
   1.240  by (rtac allI 1);
   1.241 @@ -265,35 +265,35 @@
   1.242  by (rtac refl 1);
   1.243  by (rtac allI 1);
   1.244  by (Simp_tac 1);
   1.245 -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g (x::'a))")] ssubst 1);
   1.246 +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g (x::'a))")] ssubst 1);
   1.247  by (etac spec 1);
   1.248  by (asm_simp_tac HOLCF_ss 1);
   1.249  by (rtac (iterate_Suc RS subst) 1);
   1.250  by (etac spec 1);
   1.251  qed "hoare_lemma20";
   1.252  
   1.253 -Goal "(ALL y. b1`(y::'a)=TT) ==> q`(x::'a) = UU";
   1.254 +Goal "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU";
   1.255  by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
   1.256  by (etac (hoare_lemma20 RS spec) 1);
   1.257  qed "hoare_lemma21";
   1.258  
   1.259 -Goal "b1`(UU::'a)=UU ==> q`(UU::'a) = UU";
   1.260 +Goal "b1$(UU::'a)=UU ==> q$(UU::'a) = UU";
   1.261  by (stac q_def3 1);
   1.262  by (asm_simp_tac HOLCF_ss 1);
   1.263  qed "hoare_lemma22";
   1.264  
   1.265 -(* -------- results about q for case (EX k. b1`(iterate k g x) ~= TT) ------- *)
   1.266 +(* -------- results about q for case (EX k. b1$(iterate k g x) ~= TT) ------- *)
   1.267  
   1.268  val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
   1.269  (* 
   1.270 -val hoare_lemma25 = "[| EX k. b1`(iterate k g ?x1) ~= TT;
   1.271 -    Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
   1.272 - q`(iterate ?k3 g ?x1) = q`?x1" : thm
   1.273 +val hoare_lemma25 = "[| EX k. b1$(iterate k g ?x1) ~= TT;
   1.274 +    Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==>
   1.275 + q$(iterate ?k3 g ?x1) = q$?x1" : thm
   1.276  *)
   1.277  
   1.278 -Goal "(EX n. b1`(iterate n g x)~=TT) ==>\
   1.279 -\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \
   1.280 -\ --> q`x = q`(iterate k g x)";
   1.281 +Goal "(EX n. b1$(iterate n g x)~=TT) ==>\
   1.282 +\ k=Least(%n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x) =FF \
   1.283 +\ --> q$x = q$(iterate k g x)";
   1.284  by (case_tac "k" 1);
   1.285  by (hyp_subst_tac 1);
   1.286  by (strip_tac 1);
   1.287 @@ -307,7 +307,7 @@
   1.288  by (atac 1);
   1.289  by (rtac trans 1);
   1.290  by (rtac q_def3 1);
   1.291 -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
   1.292 +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
   1.293  by (rtac (hoare_lemma8 RS spec RS mp) 1);
   1.294  by (atac 1);
   1.295  by (atac 1);
   1.296 @@ -316,9 +316,9 @@
   1.297  qed "hoare_lemma26";
   1.298  
   1.299  
   1.300 -Goal "(EX n. b1`(iterate n g x) ~= TT) ==>\
   1.301 -\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
   1.302 -\ --> q`x = UU";
   1.303 +Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
   1.304 +\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \
   1.305 +\ --> q$x = UU";
   1.306  by (case_tac "k" 1);
   1.307  by (hyp_subst_tac 1);
   1.308  by (Simp_tac 1);
   1.309 @@ -336,7 +336,7 @@
   1.310  by (atac 1);
   1.311  by (rtac trans 1);
   1.312  by (rtac q_def3 1);
   1.313 -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
   1.314 +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
   1.315  by (rtac (hoare_lemma8 RS spec RS mp) 1);
   1.316  by (atac 1);
   1.317  by (atac 1);
   1.318 @@ -347,9 +347,9 @@
   1.319  by (asm_simp_tac HOLCF_ss 1);
   1.320  qed "hoare_lemma27";
   1.321  
   1.322 -(* ------- (ALL k. b1`(iterate k g x)=TT) ==> q o p = q   ----- *)
   1.323 +(* ------- (ALL k. b1$(iterate k g x)=TT) ==> q o p = q   ----- *)
   1.324  
   1.325 -Goal "(ALL k. b1`(iterate k g x)=TT) ==> q`(p`x) = q`x";
   1.326 +Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$(p$x) = q$x";
   1.327  by (stac hoare_lemma16 1);
   1.328  by (atac 1);
   1.329  by (rtac (hoare_lemma19 RS disjE) 1);
   1.330 @@ -368,7 +368,7 @@
   1.331  
   1.332  (* ------------  EX k. b1~(iterate k g x) ~= TT ==> q o p = q   ----- *)
   1.333  
   1.334 -Goal "EX k. b1`(iterate k g x) ~= TT ==> q`(p`x) = q`x";
   1.335 +Goal "EX k. b1$(iterate k g x) ~= TT ==> q$(p$x) = q$x";
   1.336  by (rtac (hoare_lemma5 RS disjE) 1);
   1.337  by (atac 1);
   1.338  by (rtac refl 1);