src/HOLCF/ex/Loop.ML
author wenzelm
Sat Nov 03 18:41:28 2001 +0100 (2001-11-03)
changeset 12036 49f6c49454c2
parent 10835 f4745d77e620
child 13454 01e2496dee05
permissions -rw-r--r--
GPLed;
     1 (*  Title:      HOLCF/ex/Loop.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Theory for a loop primitive like while
     7 *)
     8 
     9 (* ------------------------------------------------------------------------- *)
    10 (* access to definitions                                                     *)
    11 (* ------------------------------------------------------------------------- *)
    12 
    13 
    14 Goalw [step_def] "step$b$g$x = If b$x then g$x else x fi";
    15 by (Simp_tac 1);
    16 qed "step_def2";
    17 
    18 Goalw [while_def] "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)";
    19 by (Simp_tac 1);
    20 qed "while_def2";
    21 
    22 
    23 (* ------------------------------------------------------------------------- *)
    24 (* rekursive properties of while                                             *)
    25 (* ------------------------------------------------------------------------- *)
    26 
    27 Goal "while$b$g$x = If b$x then while$b$g$(g$x) else x fi";
    28 by (fix_tac5  while_def2 1);
    29 by (Simp_tac 1);
    30 qed "while_unfold";
    31 
    32 Goal "ALL x. while$b$g$x = while$b$g$(iterate k (step$b$g) x)";
    33 by (nat_ind_tac "k" 1);
    34 by (simp_tac HOLCF_ss 1);
    35 by (rtac allI 1);
    36 by (rtac trans 1);
    37 by (stac while_unfold 1);
    38 by (rtac refl 2);
    39 by (stac iterate_Suc2 1);
    40 by (rtac trans 1);
    41 by (etac spec 2);
    42 by (stac step_def2 1);
    43 by (res_inst_tac [("p","b$x")] trE 1);
    44 by (asm_simp_tac HOLCF_ss 1);
    45 by (stac while_unfold 1);
    46 by (res_inst_tac [("s","UU"),("t","b$UU")]ssubst 1);
    47 by (etac (flat_codom RS disjE) 1);
    48 by (atac 1);
    49 by (etac spec 1);
    50 by (simp_tac HOLCF_ss 1);
    51 by (asm_simp_tac HOLCF_ss 1);
    52 by (asm_simp_tac HOLCF_ss 1);
    53 by (stac while_unfold 1);
    54 by (asm_simp_tac HOLCF_ss 1);
    55 qed "while_unfold2";
    56 
    57 Goal "while$b$g$x = while$b$g$(step$b$g$x)";
    58 by (res_inst_tac [("s", "while$b$g$(iterate (Suc 0) (step$b$g) x)")] trans 1);
    59 by (rtac (while_unfold2 RS spec) 1);
    60 by (Simp_tac 1);
    61 qed "while_unfold3";
    62 
    63 
    64 (* ------------------------------------------------------------------------- *)
    65 (* properties of while and iterations                                        *)
    66 (* ------------------------------------------------------------------------- *)
    67 
    68 Goal "[| EX y. b$y=FF; iterate k (step$b$g) x = UU |] \
    69 \    ==>iterate(Suc k) (step$b$g) x=UU";
    70 by (Simp_tac 1);
    71 by (rtac trans 1);
    72 by (rtac step_def2 1);
    73 by (asm_simp_tac HOLCF_ss 1);
    74 by (etac exE 1);
    75 by (etac (flat_codom RS disjE) 1);
    76 by (asm_simp_tac HOLCF_ss 1);
    77 by (asm_simp_tac HOLCF_ss 1);
    78 qed "loop_lemma1";
    79 
    80 Goal "[|EX y. b$y=FF;iterate (Suc k) (step$b$g) x ~=UU |]==>\
    81 \     iterate k (step$b$g) x ~=UU";
    82 
    83 by (blast_tac (claset() addIs [loop_lemma1]) 1);
    84 qed "loop_lemma2";
    85 
    86 Goal "[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);\
    87 \        EX y. b$y=FF; INV x |] \
    88 \     ==> iterate k (step$b$g) x ~=UU --> INV (iterate k (step$b$g) x)";
    89 by (nat_ind_tac "k" 1);
    90 by (Asm_simp_tac 1);
    91 by (strip_tac 1);
    92 by (simp_tac (simpset() addsimps [step_def2]) 1);
    93 by (res_inst_tac [("p","b$(iterate k (step$b$g) x)")] trE 1);
    94 by (etac notE 1);
    95 by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
    96 by (asm_simp_tac HOLCF_ss 1);
    97 by (rtac mp 1);
    98 by (etac spec 1);
    99 by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
   100 by (res_inst_tac [("s","iterate (Suc k) (step$b$g) x"),
   101                   ("t","g$(iterate k (step$b$g) x)")] ssubst 1);
   102 by (atac 2);
   103 by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
   104 by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
   105 qed_spec_mp "loop_lemma3";
   106 
   107 Goal "ALL x. b$(iterate k (step$b$g) x)=FF --> while$b$g$x= iterate k (step$b$g) x";
   108 by (nat_ind_tac "k" 1);
   109 by (Simp_tac 1);
   110 by (strip_tac 1);
   111 by (stac while_unfold 1);
   112 by (asm_simp_tac HOLCF_ss 1);
   113 by (rtac allI 1);
   114 by (stac iterate_Suc2 1);
   115 by (strip_tac 1);
   116 by (rtac trans 1);
   117 by (rtac while_unfold3 1);
   118 by (Asm_simp_tac 1);
   119 qed_spec_mp "loop_lemma4";
   120 
   121 Goal "ALL k. b$(iterate k (step$b$g) x) ~= FF ==>\
   122 \ ALL m. while$b$g$(iterate m (step$b$g) x)=UU";
   123 by (stac while_def2 1);
   124 by (rtac fix_ind 1);
   125 by (rtac (allI RS adm_all) 1);
   126 by (rtac adm_eq 1);
   127 by (cont_tacR 1);
   128 by (Simp_tac  1);
   129 by (rtac allI 1);
   130 by (Simp_tac  1);
   131 by (res_inst_tac [("p","b$(iterate m (step$b$g) x)")] trE 1);
   132 by (Asm_simp_tac 1);
   133 by (Asm_simp_tac 1);
   134 by (res_inst_tac [("s","xa$(iterate (Suc m) (step$b$g) x)")] trans 1);
   135 by (etac spec 2);
   136 by (rtac cfun_arg_cong 1);
   137 by (rtac trans 1);
   138 by (rtac (iterate_Suc RS sym) 2);
   139 by (asm_simp_tac (HOLCF_ss addsimps [step_def2]) 1);
   140 by (Blast_tac 1);
   141 qed_spec_mp "loop_lemma5";
   142 
   143 
   144 Goal "ALL k. b$(iterate k (step$b$g) x) ~= FF ==> while$b$g$x=UU";
   145 by (res_inst_tac [("t","x")] (iterate_0 RS subst) 1);
   146 by (etac (loop_lemma5) 1);
   147 qed "loop_lemma6";
   148 
   149 Goal "while$b$g$x ~= UU ==> EX k. b$(iterate k (step$b$g) x) = FF";
   150 by (blast_tac (claset() addIs [loop_lemma6]) 1);
   151 qed "loop_lemma7";
   152 
   153 
   154 (* ------------------------------------------------------------------------- *)
   155 (* an invariant rule for loops                                               *)
   156 (* ------------------------------------------------------------------------- *)
   157 
   158 Goal
   159 "[| (ALL y. INV y & b$y=TT & g$y ~= UU --> INV (g$y));\
   160 \   (ALL y. INV y & b$y=FF --> Q y);\
   161 \   INV x; while$b$g$x~=UU |] ==> Q (while$b$g$x)";
   162 by (res_inst_tac [("P","%k. b$(iterate k (step$b$g) x)=FF")] exE 1);
   163 by (etac loop_lemma7 1);
   164 by (stac (loop_lemma4) 1);
   165 by (atac 1);
   166 by (dtac spec 1 THEN etac mp 1);
   167 by (rtac conjI 1);
   168 by (atac 2);
   169 by (rtac (loop_lemma3) 1);
   170 by (assume_tac 1);
   171 by (blast_tac (claset() addIs [loop_lemma6]) 1);
   172 by (assume_tac 1);
   173 by (rotate_tac ~1 1);
   174 by (asm_full_simp_tac (simpset() addsimps [loop_lemma4]) 1);
   175 qed "loop_inv2";
   176 
   177 val [premP,premI,premTT,premFF,premW] = Goal
   178 "[| P(x); \
   179 \   !!y. P y ==> INV y;\
   180 \   !!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y);\
   181 \   !!y. [| INV y; b$y=FF|] ==> Q y;\
   182 \   while$b$g$x ~= UU |] ==> Q (while$b$g$x)";
   183 by (rtac loop_inv2 1);
   184 by (rtac (premP RS premI) 3);
   185 by (rtac premW 3);
   186 by (blast_tac (claset() addIs [premTT]) 1);
   187 by (blast_tac (claset() addIs [premFF]) 1);
   188 qed "loop_inv";