src/HOLCF/IOA/meta_theory/ShortExecutions.ML
changeset 10835 f4745d77e620
parent 9877 b2a62260f8ac
child 12028 52aa183c15bb
     1.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -29,24 +29,24 @@
     1.4  \    | x##xs => \
     1.5  \      (case x of\ 
     1.6  \        Undef => UU\
     1.7 -\      | Def y => (Takewhile (%a.~ P a)`s)\
     1.8 -\                  @@ (y>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`xs))\
     1.9 +\      | Def y => (Takewhile (%a.~ P a)$s)\
    1.10 +\                  @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))\
    1.11  \      )\
    1.12  \    )");
    1.13  
    1.14 -Goal "oraclebuild P`sch`UU = UU";
    1.15 +Goal "oraclebuild P$sch$UU = UU";
    1.16  by (stac oraclebuild_unfold 1);
    1.17  by (Simp_tac 1);
    1.18  qed"oraclebuild_UU";
    1.19  
    1.20 -Goal "oraclebuild P`sch`nil = nil";
    1.21 +Goal "oraclebuild P$sch$nil = nil";
    1.22  by (stac oraclebuild_unfold 1);
    1.23  by (Simp_tac 1);
    1.24  qed"oraclebuild_nil";
    1.25  
    1.26 -Goal "oraclebuild P`s`(x>>t) = \
    1.27 -\         (Takewhile (%a.~ P a)`s)   \
    1.28 -\          @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";     
    1.29 +Goal "oraclebuild P$s$(x>>t) = \
    1.30 +\         (Takewhile (%a.~ P a)$s)   \
    1.31 +\          @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))";     
    1.32  by (rtac trans 1);
    1.33  by (stac oraclebuild_unfold 1);
    1.34  by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
    1.35 @@ -63,7 +63,7 @@
    1.36  Goalw [Cut_def]
    1.37  "[| Forall (%a.~ P a) s; Finite s|] \
    1.38  \           ==> Cut P s =nil";
    1.39 -by (subgoal_tac "Filter P`s = nil" 1);
    1.40 +by (subgoal_tac "Filter P$s = nil" 1);
    1.41  by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1);
    1.42  by (rtac ForallQFilterPnil 1);
    1.43  by (REPEAT (atac 1));
    1.44 @@ -72,7 +72,7 @@
    1.45  Goalw [Cut_def]
    1.46  "[| Forall (%a.~ P a) s; ~Finite s|] \
    1.47  \           ==> Cut P s =UU";
    1.48 -by (subgoal_tac "Filter P`s= UU" 1);
    1.49 +by (subgoal_tac "Filter P$s= UU" 1);
    1.50  by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1);
    1.51  by (rtac ForallQFilterPUU 1);
    1.52  by (REPEAT (atac 1));
    1.53 @@ -93,7 +93,7 @@
    1.54  (* ---------------------------------------------------------------- *)
    1.55  
    1.56  
    1.57 -Goal "Filter P`s = Filter P`(Cut P s)";
    1.58 +Goal "Filter P$s = Filter P$(Cut P s)";
    1.59  
    1.60  by (res_inst_tac [("A1","%x. True")
    1.61                   ,("Q1","%x.~ P x"), ("x1","s")]
    1.62 @@ -128,7 +128,7 @@
    1.63  qed"Cut_idemp";
    1.64  
    1.65  
    1.66 -Goal "Map f`(Cut (P o f) s) = Cut P (Map f`s)";
    1.67 +Goal "Map f$(Cut (P o f) s) = Cut P (Map f$s)";
    1.68  
    1.69  by (res_inst_tac [("A1","%x. True")
    1.70                   ,("Q1","%x.~ P (f x)"), ("x1","s")]
    1.71 @@ -200,13 +200,13 @@
    1.72  
    1.73  
    1.74  Goalw [schedules_def,has_schedule_def]
    1.75 - "[|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
    1.76 + "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] \
    1.77  \   ==> ? sch. sch : schedules A & \
    1.78 -\              tr = Filter (%a. a:ext A)`sch &\
    1.79 +\              tr = Filter (%a. a:ext A)$sch &\
    1.80  \              LastActExtsch A sch";
    1.81  
    1.82  by (safe_tac set_cs);
    1.83 -by (res_inst_tac [("x","filter_act`(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
    1.84 +by (res_inst_tac [("x","filter_act$(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
    1.85  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    1.86  by (pair_tac "ex" 1);
    1.87  by (safe_tac set_cs);
    1.88 @@ -220,7 +220,7 @@
    1.89  (* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
    1.90  
    1.91  by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    1.92 -by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
    1.93 +by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1);
    1.94  
    1.95  by (rtac (rewrite_rule [o_def] MapCut) 2);
    1.96  by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1);
    1.97 @@ -228,7 +228,7 @@
    1.98  (* Subgoal 3: Lemma: Cut idempotent  *)
    1.99  
   1.100  by (simp_tac (simpset() addsimps [LastActExtsch_def,filter_act_def]) 1);
   1.101 -by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
   1.102 +by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1);
   1.103  by (rtac (rewrite_rule [o_def] MapCut) 2);
   1.104  by (asm_full_simp_tac (simpset() addsimps [Cut_idemp]) 1);
   1.105  qed"exists_LastActExtsch";
   1.106 @@ -239,7 +239,7 @@
   1.107  (* ---------------------------------------------------------------- *)
   1.108  
   1.109  Goalw [LastActExtsch_def]
   1.110 -  "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
   1.111 +  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] \
   1.112  \   ==> sch=nil";
   1.113  by (dtac FilternPnilForallP 1);
   1.114  by (etac conjE 1);
   1.115 @@ -249,7 +249,7 @@
   1.116  qed"LastActExtimplnil";
   1.117  
   1.118  Goalw [LastActExtsch_def]
   1.119 -  "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
   1.120 +  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] \
   1.121  \   ==> sch=UU";
   1.122  by (dtac FilternPUUForallP 1);
   1.123  by (etac conjE 1);