src/HOLCF/ex/Loop.ML
changeset 10835 f4745d77e620
parent 9248 e1dee89de037
child 12036 49f6c49454c2
     1.1 --- a/src/HOLCF/ex/Loop.ML	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/ex/Loop.ML	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -11,11 +11,11 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  
     1.6  
     1.7 -Goalw [step_def] "step`b`g`x = If b`x then g`x else x fi";
     1.8 +Goalw [step_def] "step$b$g$x = If b$x then g$x else x fi";
     1.9  by (Simp_tac 1);
    1.10  qed "step_def2";
    1.11  
    1.12 -Goalw [while_def] "while`b`g = fix`(LAM f x. If b`x then f`(g`x) else x fi)";
    1.13 +Goalw [while_def] "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)";
    1.14  by (Simp_tac 1);
    1.15  qed "while_def2";
    1.16  
    1.17 @@ -24,12 +24,12 @@
    1.18  (* rekursive properties of while                                             *)
    1.19  (* ------------------------------------------------------------------------- *)
    1.20  
    1.21 -Goal "while`b`g`x = If b`x then while`b`g`(g`x) else x fi";
    1.22 +Goal "while$b$g$x = If b$x then while$b$g$(g$x) else x fi";
    1.23  by (fix_tac5  while_def2 1);
    1.24  by (Simp_tac 1);
    1.25  qed "while_unfold";
    1.26  
    1.27 -Goal "ALL x. while`b`g`x = while`b`g`(iterate k (step`b`g) x)";
    1.28 +Goal "ALL x. while$b$g$x = while$b$g$(iterate k (step$b$g) x)";
    1.29  by (nat_ind_tac "k" 1);
    1.30  by (simp_tac HOLCF_ss 1);
    1.31  by (rtac allI 1);
    1.32 @@ -40,10 +40,10 @@
    1.33  by (rtac trans 1);
    1.34  by (etac spec 2);
    1.35  by (stac step_def2 1);
    1.36 -by (res_inst_tac [("p","b`x")] trE 1);
    1.37 +by (res_inst_tac [("p","b$x")] trE 1);
    1.38  by (asm_simp_tac HOLCF_ss 1);
    1.39  by (stac while_unfold 1);
    1.40 -by (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1);
    1.41 +by (res_inst_tac [("s","UU"),("t","b$UU")]ssubst 1);
    1.42  by (etac (flat_codom RS disjE) 1);
    1.43  by (atac 1);
    1.44  by (etac spec 1);
    1.45 @@ -54,8 +54,8 @@
    1.46  by (asm_simp_tac HOLCF_ss 1);
    1.47  qed "while_unfold2";
    1.48  
    1.49 -Goal "while`b`g`x = while`b`g`(step`b`g`x)";
    1.50 -by (res_inst_tac [("s", "while`b`g`(iterate (Suc 0) (step`b`g) x)")] trans 1);
    1.51 +Goal "while$b$g$x = while$b$g$(step$b$g$x)";
    1.52 +by (res_inst_tac [("s", "while$b$g$(iterate (Suc 0) (step$b$g) x)")] trans 1);
    1.53  by (rtac (while_unfold2 RS spec) 1);
    1.54  by (Simp_tac 1);
    1.55  qed "while_unfold3";
    1.56 @@ -65,8 +65,8 @@
    1.57  (* properties of while and iterations                                        *)
    1.58  (* ------------------------------------------------------------------------- *)
    1.59  
    1.60 -Goal "[| EX y. b`y=FF; iterate k (step`b`g) x = UU |] \
    1.61 -\    ==>iterate(Suc k) (step`b`g) x=UU";
    1.62 +Goal "[| EX y. b$y=FF; iterate k (step$b$g) x = UU |] \
    1.63 +\    ==>iterate(Suc k) (step$b$g) x=UU";
    1.64  by (Simp_tac 1);
    1.65  by (rtac trans 1);
    1.66  by (rtac step_def2 1);
    1.67 @@ -77,34 +77,34 @@
    1.68  by (asm_simp_tac HOLCF_ss 1);
    1.69  qed "loop_lemma1";
    1.70  
    1.71 -Goal "[|EX y. b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
    1.72 -\     iterate k (step`b`g) x ~=UU";
    1.73 +Goal "[|EX y. b$y=FF;iterate (Suc k) (step$b$g) x ~=UU |]==>\
    1.74 +\     iterate k (step$b$g) x ~=UU";
    1.75  
    1.76  by (blast_tac (claset() addIs [loop_lemma1]) 1);
    1.77  qed "loop_lemma2";
    1.78  
    1.79 -Goal "[| ALL x. INV x & b`x=TT & g`x~=UU --> INV (g`x);\
    1.80 -\        EX y. b`y=FF; INV x |] \
    1.81 -\     ==> iterate k (step`b`g) x ~=UU --> INV (iterate k (step`b`g) x)";
    1.82 +Goal "[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);\
    1.83 +\        EX y. b$y=FF; INV x |] \
    1.84 +\     ==> iterate k (step$b$g) x ~=UU --> INV (iterate k (step$b$g) x)";
    1.85  by (nat_ind_tac "k" 1);
    1.86  by (Asm_simp_tac 1);
    1.87  by (strip_tac 1);
    1.88  by (simp_tac (simpset() addsimps [step_def2]) 1);
    1.89 -by (res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1);
    1.90 +by (res_inst_tac [("p","b$(iterate k (step$b$g) x)")] trE 1);
    1.91  by (etac notE 1);
    1.92  by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
    1.93  by (asm_simp_tac HOLCF_ss 1);
    1.94  by (rtac mp 1);
    1.95  by (etac spec 1);
    1.96  by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
    1.97 -by (res_inst_tac [("s","iterate (Suc k) (step`b`g) x"),
    1.98 -                  ("t","g`(iterate k (step`b`g) x)")] ssubst 1);
    1.99 +by (res_inst_tac [("s","iterate (Suc k) (step$b$g) x"),
   1.100 +                  ("t","g$(iterate k (step$b$g) x)")] ssubst 1);
   1.101  by (atac 2);
   1.102  by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
   1.103  by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
   1.104  qed_spec_mp "loop_lemma3";
   1.105  
   1.106 -Goal "ALL x. b`(iterate k (step`b`g) x)=FF --> while`b`g`x= iterate k (step`b`g) x";
   1.107 +Goal "ALL x. b$(iterate k (step$b$g) x)=FF --> while$b$g$x= iterate k (step$b$g) x";
   1.108  by (nat_ind_tac "k" 1);
   1.109  by (Simp_tac 1);
   1.110  by (strip_tac 1);
   1.111 @@ -118,8 +118,8 @@
   1.112  by (Asm_simp_tac 1);
   1.113  qed_spec_mp "loop_lemma4";
   1.114  
   1.115 -Goal "ALL k. b`(iterate k (step`b`g) x) ~= FF ==>\
   1.116 -\ ALL m. while`b`g`(iterate m (step`b`g) x)=UU";
   1.117 +Goal "ALL k. b$(iterate k (step$b$g) x) ~= FF ==>\
   1.118 +\ ALL m. while$b$g$(iterate m (step$b$g) x)=UU";
   1.119  by (stac while_def2 1);
   1.120  by (rtac fix_ind 1);
   1.121  by (rtac (allI RS adm_all) 1);
   1.122 @@ -128,10 +128,10 @@
   1.123  by (Simp_tac  1);
   1.124  by (rtac allI 1);
   1.125  by (Simp_tac  1);
   1.126 -by (res_inst_tac [("p","b`(iterate m (step`b`g) x)")] trE 1);
   1.127 +by (res_inst_tac [("p","b$(iterate m (step$b$g) x)")] trE 1);
   1.128  by (Asm_simp_tac 1);
   1.129  by (Asm_simp_tac 1);
   1.130 -by (res_inst_tac [("s","xa`(iterate (Suc m) (step`b`g) x)")] trans 1);
   1.131 +by (res_inst_tac [("s","xa$(iterate (Suc m) (step$b$g) x)")] trans 1);
   1.132  by (etac spec 2);
   1.133  by (rtac cfun_arg_cong 1);
   1.134  by (rtac trans 1);
   1.135 @@ -141,12 +141,12 @@
   1.136  qed_spec_mp "loop_lemma5";
   1.137  
   1.138  
   1.139 -Goal "ALL k. b`(iterate k (step`b`g) x) ~= FF ==> while`b`g`x=UU";
   1.140 +Goal "ALL k. b$(iterate k (step$b$g) x) ~= FF ==> while$b$g$x=UU";
   1.141  by (res_inst_tac [("t","x")] (iterate_0 RS subst) 1);
   1.142  by (etac (loop_lemma5) 1);
   1.143  qed "loop_lemma6";
   1.144  
   1.145 -Goal "while`b`g`x ~= UU ==> EX k. b`(iterate k (step`b`g) x) = FF";
   1.146 +Goal "while$b$g$x ~= UU ==> EX k. b$(iterate k (step$b$g) x) = FF";
   1.147  by (blast_tac (claset() addIs [loop_lemma6]) 1);
   1.148  qed "loop_lemma7";
   1.149  
   1.150 @@ -156,10 +156,10 @@
   1.151  (* ------------------------------------------------------------------------- *)
   1.152  
   1.153  Goal
   1.154 -"[| (ALL y. INV y & b`y=TT & g`y ~= UU --> INV (g`y));\
   1.155 -\   (ALL y. INV y & b`y=FF --> Q y);\
   1.156 -\   INV x; while`b`g`x~=UU |] ==> Q (while`b`g`x)";
   1.157 -by (res_inst_tac [("P","%k. b`(iterate k (step`b`g) x)=FF")] exE 1);
   1.158 +"[| (ALL y. INV y & b$y=TT & g$y ~= UU --> INV (g$y));\
   1.159 +\   (ALL y. INV y & b$y=FF --> Q y);\
   1.160 +\   INV x; while$b$g$x~=UU |] ==> Q (while$b$g$x)";
   1.161 +by (res_inst_tac [("P","%k. b$(iterate k (step$b$g) x)=FF")] exE 1);
   1.162  by (etac loop_lemma7 1);
   1.163  by (stac (loop_lemma4) 1);
   1.164  by (atac 1);
   1.165 @@ -177,9 +177,9 @@
   1.166  val [premP,premI,premTT,premFF,premW] = Goal
   1.167  "[| P(x); \
   1.168  \   !!y. P y ==> INV y;\
   1.169 -\   !!y. [| INV y; b`y=TT; g`y~=UU|] ==> INV (g`y);\
   1.170 -\   !!y. [| INV y; b`y=FF|] ==> Q y;\
   1.171 -\   while`b`g`x ~= UU |] ==> Q (while`b`g`x)";
   1.172 +\   !!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y);\
   1.173 +\   !!y. [| INV y; b$y=FF|] ==> Q y;\
   1.174 +\   while$b$g$x ~= UU |] ==> Q (while$b$g$x)";
   1.175  by (rtac loop_inv2 1);
   1.176  by (rtac (premP RS premI) 3);
   1.177  by (rtac premW 3);