src/HOLCF/IOA/meta_theory/CompoScheds.ML
changeset 10835 f4745d77e620
parent 7229 6773ba0c36d5
child 11655 923e4d0d36d5
     1.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -30,25 +30,25 @@
     1.4  \     | Def y =>  \
     1.5  \        (if y:act A then \
     1.6  \            (if y:act B then \
     1.7 -\               (case HD`exA of \
     1.8 +\               (case HD$exA of \
     1.9  \                  Undef => UU \
    1.10 -\                | Def a => (case HD`exB of \
    1.11 +\                | Def a => (case HD$exB of \
    1.12  \                             Undef => UU \
    1.13  \                           | Def b => \
    1.14  \                  (y,(snd a,snd b))>>  \
    1.15 -\                    (mkex2 A B`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))  \
    1.16 +\                    (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))  \
    1.17  \             else   \
    1.18 -\               (case HD`exA of   \
    1.19 +\               (case HD$exA of   \
    1.20  \                  Undef => UU  \
    1.21  \                | Def a => \
    1.22 -\                  (y,(snd a,t))>>(mkex2 A B`xs`(TL`exA)`exB) (snd a) t)  \
    1.23 +\                  (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t)  \
    1.24  \             )  \       
    1.25  \         else   \
    1.26  \            (if y:act B then \
    1.27 -\               (case HD`exB of  \
    1.28 +\               (case HD$exB of  \
    1.29  \                  Undef => UU  \
    1.30  \                | Def b =>  \
    1.31 -\                  (y,(s,snd b))>>(mkex2 A B`xs`exA`(TL`exB)) s (snd b))  \
    1.32 +\                  (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b))  \
    1.33  \            else  \
    1.34  \              UU  \
    1.35  \            )  \
    1.36 @@ -56,38 +56,38 @@
    1.37  \      )))");
    1.38  
    1.39  
    1.40 -Goal "(mkex2 A B`UU`exA`exB) s t = UU";
    1.41 +Goal "(mkex2 A B$UU$exA$exB) s t = UU";
    1.42  by (stac mkex2_unfold 1);
    1.43  by (Simp_tac 1);
    1.44  qed"mkex2_UU";
    1.45  
    1.46 -Goal "(mkex2 A B`nil`exA`exB) s t= nil";
    1.47 +Goal "(mkex2 A B$nil$exA$exB) s t= nil";
    1.48  by (stac mkex2_unfold 1);
    1.49  by (Simp_tac 1);
    1.50  qed"mkex2_nil";
    1.51  
    1.52 -Goal "[| x:act A; x~:act B; HD`exA=Def a|] \
    1.53 -\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =   \
    1.54 -\       (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
    1.55 +Goal "[| x:act A; x~:act B; HD$exA=Def a|] \
    1.56 +\   ==> (mkex2 A B$(x>>sch)$exA$exB) s t =   \
    1.57 +\       (x,snd a,t) >> (mkex2 A B$sch$(TL$exA)$exB) (snd a) t";
    1.58  by (rtac trans 1);
    1.59  by (stac mkex2_unfold 1);
    1.60  by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
    1.61  by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
    1.62  qed"mkex2_cons_1";
    1.63  
    1.64 -Goal "[| x~:act A; x:act B; HD`exB=Def b|] \
    1.65 -\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
    1.66 -\       (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
    1.67 +Goal "[| x~:act A; x:act B; HD$exB=Def b|] \
    1.68 +\   ==> (mkex2 A B$(x>>sch)$exA$exB) s t = \
    1.69 +\       (x,s,snd b) >> (mkex2 A B$sch$exA$(TL$exB)) s (snd b)";
    1.70  by (rtac trans 1);
    1.71  by (stac mkex2_unfold 1);
    1.72  by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
    1.73  by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
    1.74  qed"mkex2_cons_2";
    1.75  
    1.76 -Goal "[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
    1.77 -\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =  \
    1.78 +Goal "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|] \
    1.79 +\   ==> (mkex2 A B$(x>>sch)$exA$exB) s t =  \
    1.80  \        (x,snd a,snd b) >> \
    1.81 -\           (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
    1.82 +\           (mkex2 A B$sch$(TL$exA)$(TL$exB)) (snd a) (snd b)";
    1.83  by (rtac trans 1);
    1.84  by (stac mkex2_unfold 1);
    1.85  by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
    1.86 @@ -156,8 +156,8 @@
    1.87  (* --------------------------------------------------------------------- *)
    1.88  
    1.89  Goalw [filter_act_def,Filter_ex2_def]
    1.90 -   "filter_act`(Filter_ex2 (asig_of A)`xs)=\
    1.91 -\   Filter (%a. a:act A)`(filter_act`xs)";
    1.92 +   "filter_act$(Filter_ex2 (asig_of A)$xs)=\
    1.93 +\   Filter (%a. a:act A)$(filter_act$xs)";
    1.94  
    1.95  by (simp_tac (simpset() addsimps [MapFilter,o_def]) 1);
    1.96  qed"lemma_2_1a";
    1.97 @@ -168,8 +168,8 @@
    1.98  (* --------------------------------------------------------------------- *)
    1.99  
   1.100  Goal 
   1.101 -   "filter_act`(ProjA2`xs) =filter_act`xs &\
   1.102 -\   filter_act`(ProjB2`xs) =filter_act`xs";
   1.103 +   "filter_act$(ProjA2$xs) =filter_act$xs &\
   1.104 +\   filter_act$(ProjB2$xs) =filter_act$xs";
   1.105  
   1.106  by (pair_induct_tac "xs" [] 1);
   1.107  qed"lemma_2_1b";
   1.108 @@ -184,7 +184,7 @@
   1.109     is the same proposition, but we cannot change this one, when then rather lemma_1_1c  *)
   1.110  
   1.111  Goal "!s. is_exec_frag (A||B) (s,xs) \
   1.112 -\  --> Forall (%x. x:act (A||B)) (filter_act`xs)";
   1.113 +\  --> Forall (%x. x:act (A||B)) (filter_act$xs)";
   1.114  
   1.115  by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
   1.116  (* main case *)
   1.117 @@ -205,9 +205,9 @@
   1.118  
   1.119  Goal "! exA exB s t. \
   1.120  \ Forall (%x. x:act (A||B)) sch  & \
   1.121 -\ Filter (%a. a:act A)`sch << filter_act`exA &\
   1.122 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   1.123 -\ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch";
   1.124 +\ Filter (%a. a:act A)$sch << filter_act$exA &\
   1.125 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   1.126 +\ --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch";
   1.127  
   1.128  by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1);
   1.129  
   1.130 @@ -268,9 +268,9 @@
   1.131  
   1.132  Goal "! exA exB s t. \
   1.133  \ Forall (%x. x:act (A||B)) sch & \
   1.134 -\ Filter (%a. a:act A)`sch << filter_act`exA &\
   1.135 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   1.136 -\ --> stutter (asig_of A) (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
   1.137 +\ Filter (%a. a:act A)$sch << filter_act$exA &\
   1.138 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   1.139 +\ --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))";
   1.140  
   1.141  by (mkex_induct_tac "sch" "exA" "exB");
   1.142  
   1.143 @@ -279,8 +279,8 @@
   1.144  
   1.145  Goal "[|  \
   1.146  \ Forall (%x. x:act (A||B)) sch ; \
   1.147 -\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
   1.148 -\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
   1.149 +\ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;\
   1.150 +\ Filter (%a. a:act B)$sch << filter_act$(snd exB) |] \
   1.151  \ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))";
   1.152  
   1.153  by (cut_facts_tac [stutterA_mkex] 1);
   1.154 @@ -299,9 +299,9 @@
   1.155  
   1.156  Goal "! exA exB s t. \
   1.157  \ Forall (%x. x:act (A||B)) sch & \
   1.158 -\ Filter (%a. a:act A)`sch << filter_act`exA &\
   1.159 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   1.160 -\ --> stutter (asig_of B) (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
   1.161 +\ Filter (%a. a:act A)$sch << filter_act$exA &\
   1.162 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   1.163 +\ --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))";
   1.164  
   1.165  by (mkex_induct_tac "sch" "exA" "exB");
   1.166  
   1.167 @@ -310,8 +310,8 @@
   1.168  
   1.169  Goal "[|  \
   1.170  \ Forall (%x. x:act (A||B)) sch ; \
   1.171 -\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
   1.172 -\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
   1.173 +\ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;\
   1.174 +\ Filter (%a. a:act B)$sch << filter_act$(snd exB) |] \
   1.175  \ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))";
   1.176  
   1.177  by (cut_facts_tac [stutterB_mkex] 1);
   1.178 @@ -325,40 +325,40 @@
   1.179  
   1.180  (*---------------------------------------------------------------------------
   1.181       Filter of mkex(sch,exA,exB) to A after projection onto A is exA 
   1.182 -        --  using zip`(proj1`exA)`(proj2`exA) instead of exA    --
   1.183 +        --  using zip$(proj1$exA)$(proj2$exA) instead of exA    --
   1.184          --           because of admissibility problems          --
   1.185                               structural induction
   1.186    --------------------------------------------------------------------------- *)
   1.187  
   1.188  Goal "! exA exB s t. \
   1.189  \ Forall (%x. x:act (A||B)) sch & \
   1.190 -\ Filter (%a. a:act A)`sch << filter_act`exA  &\
   1.191 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   1.192 -\ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   1.193 -\     Zip`(Filter (%a. a:act A)`sch)`(Map snd`exA)";
   1.194 +\ Filter (%a. a:act A)$sch << filter_act$exA  &\
   1.195 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   1.196 +\ --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   1.197 +\     Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)";
   1.198  
   1.199  by (mkex_induct_tac "sch" "exB" "exA");
   1.200  
   1.201  qed"filter_mkex_is_exA_tmp";
   1.202  
   1.203  (*---------------------------------------------------------------------------
   1.204 -                      zip`(proj1`y)`(proj2`y) = y   (using the lift operations)
   1.205 +                      zip$(proj1$y)$(proj2$y) = y   (using the lift operations)
   1.206                      lemma for admissibility problems         
   1.207    --------------------------------------------------------------------------- *)
   1.208  
   1.209 -Goal  "Zip`(Map fst`y)`(Map snd`y) = y";
   1.210 +Goal  "Zip$(Map fst$y)$(Map snd$y) = y";
   1.211  by (Seq_induct_tac "y" [] 1);
   1.212  qed"Zip_Map_fst_snd";
   1.213  
   1.214  
   1.215  (*---------------------------------------------------------------------------
   1.216 -      filter A`sch = proj1`ex   -->  zip`(filter A`sch)`(proj2`ex) = ex 
   1.217 +      filter A$sch = proj1$ex   -->  zip$(filter A$sch)$(proj2$ex) = ex 
   1.218           lemma for eliminating non admissible equations in assumptions      
   1.219    --------------------------------------------------------------------------- *)
   1.220  
   1.221  Goal "!! sch ex. \
   1.222 -\ Filter (%a. a:act AB)`sch = filter_act`ex  \
   1.223 -\ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)";
   1.224 +\ Filter (%a. a:act AB)$sch = filter_act$ex  \
   1.225 +\ ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)";
   1.226  by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 1);
   1.227  by (rtac (Zip_Map_fst_snd RS sym) 1);
   1.228  qed"trick_against_eq_in_ass";
   1.229 @@ -371,8 +371,8 @@
   1.230  
   1.231  Goal "!!sch exA exB.\
   1.232  \ [| Forall (%a. a:act (A||B)) sch ; \
   1.233 -\ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
   1.234 -\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
   1.235 +\ Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;\
   1.236 +\ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]\
   1.237  \ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA";
   1.238  by (asm_full_simp_tac (simpset() addsimps [ProjA_def,Filter_ex_def]) 1);
   1.239  by (pair_tac "exA" 1);
   1.240 @@ -388,7 +388,7 @@
   1.241  
   1.242  (*---------------------------------------------------------------------------
   1.243       Filter of mkex(sch,exA,exB) to B after projection onto B is exB 
   1.244 -        --  using zip`(proj1`exB)`(proj2`exB) instead of exB    --
   1.245 +        --  using zip$(proj1$exB)$(proj2$exB) instead of exB    --
   1.246          --           because of admissibility problems          --
   1.247                               structural induction
   1.248    --------------------------------------------------------------------------- *)
   1.249 @@ -396,10 +396,10 @@
   1.250  
   1.251  Goal "! exA exB s t. \
   1.252  \ Forall (%x. x:act (A||B)) sch & \
   1.253 -\ Filter (%a. a:act A)`sch << filter_act`exA  &\
   1.254 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   1.255 -\ --> Filter_ex2 (asig_of B)`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   1.256 -\     Zip`(Filter (%a. a:act B)`sch)`(Map snd`exB)";
   1.257 +\ Filter (%a. a:act A)$sch << filter_act$exA  &\
   1.258 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   1.259 +\ --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   1.260 +\     Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)";
   1.261  
   1.262  (* notice necessary change of arguments exA and exB *)
   1.263  by (mkex_induct_tac "sch" "exA" "exB");
   1.264 @@ -415,8 +415,8 @@
   1.265  
   1.266  Goal "!!sch exA exB.\
   1.267  \ [| Forall (%a. a:act (A||B)) sch ; \
   1.268 -\ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
   1.269 -\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
   1.270 +\ Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;\
   1.271 +\ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]\
   1.272  \ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB";
   1.273  by (asm_full_simp_tac (simpset() addsimps [ProjB_def,Filter_ex_def]) 1);
   1.274  by (pair_tac "exA" 1);
   1.275 @@ -436,8 +436,8 @@
   1.276  
   1.277  Goal "!s t exA exB. \
   1.278  \ Forall (%x. x : act (A || B)) sch &\
   1.279 -\ Filter (%a. a:act A)`sch << filter_act`exA  &\
   1.280 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   1.281 +\ Filter (%a. a:act A)$sch << filter_act$exA  &\
   1.282 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   1.283  \  --> Forall (%x. fst x : act (A ||B))   \
   1.284  \        (snd (mkex A B sch (s,exA) (t,exB)))";
   1.285  
   1.286 @@ -453,8 +453,8 @@
   1.287  
   1.288  Goal  
   1.289  "sch : schedules (A||B) = \
   1.290 -\ (Filter (%a. a:act A)`sch : schedules A &\
   1.291 -\  Filter (%a. a:act B)`sch : schedules B &\
   1.292 +\ (Filter (%a. a:act A)$sch : schedules A &\
   1.293 +\  Filter (%a. a:act B)$sch : schedules B &\
   1.294  \  Forall (%x. x:act (A||B)) sch)";
   1.295  
   1.296  by (simp_tac (simpset() addsimps [schedules_def, has_schedule_def]) 1);