src/HOLCF/IOA/meta_theory/Traces.ML
changeset 10835 f4745d77e620
parent 7229 6773ba0c36d5
child 12218 6597093b77e7
     1.1 --- a/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -26,15 +26,15 @@
     1.4  (* ---------------------------------------------------------------- *)
     1.5  
     1.6  
     1.7 -Goal  "filter_act`UU = UU";
     1.8 +Goal  "filter_act$UU = UU";
     1.9  by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    1.10  qed"filter_act_UU";
    1.11  
    1.12 -Goal  "filter_act`nil = nil";
    1.13 +Goal  "filter_act$nil = nil";
    1.14  by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    1.15  qed"filter_act_nil";
    1.16  
    1.17 -Goal "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
    1.18 +Goal "filter_act$(x>>xs) = (fst x) >> filter_act$xs";
    1.19  by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    1.20  qed"filter_act_cons";
    1.21  
    1.22 @@ -45,18 +45,18 @@
    1.23  (*                             mk_trace                             *)
    1.24  (* ---------------------------------------------------------------- *)
    1.25  
    1.26 -Goal "mk_trace A`UU=UU";
    1.27 +Goal "mk_trace A$UU=UU";
    1.28  by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
    1.29  qed"mk_trace_UU";
    1.30  
    1.31 -Goal "mk_trace A`nil=nil";
    1.32 +Goal "mk_trace A$nil=nil";
    1.33  by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
    1.34  qed"mk_trace_nil";
    1.35  
    1.36 -Goal "mk_trace A`(at >> xs) =    \
    1.37 +Goal "mk_trace A$(at >> xs) =    \
    1.38  \            (if ((fst at):ext A)    \       
    1.39 -\                 then (fst at) >> (mk_trace A`xs) \   
    1.40 -\                 else mk_trace A`xs)";
    1.41 +\                 then (fst at) >> (mk_trace A$xs) \   
    1.42 +\                 else mk_trace A$xs)";
    1.43  
    1.44  by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1);
    1.45  qed"mk_trace_cons";
    1.46 @@ -71,8 +71,8 @@
    1.47  Goal "is_exec_fragC A = (LAM ex. (%s. case ex of \
    1.48  \      nil => TT \
    1.49  \    | x##xs => (flift1 \ 
    1.50 -\            (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
    1.51 -\             `x) \
    1.52 +\            (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p)) \
    1.53 +\             $x) \
    1.54  \   ))";
    1.55  by (rtac trans 1);
    1.56  by (rtac fix_eq2 1);
    1.57 @@ -81,19 +81,19 @@
    1.58  by (simp_tac (simpset() addsimps [flift1_def]) 1);
    1.59  qed"is_exec_fragC_unfold";
    1.60  
    1.61 -Goal "(is_exec_fragC A`UU) s=UU";
    1.62 +Goal "(is_exec_fragC A$UU) s=UU";
    1.63  by (stac is_exec_fragC_unfold 1);
    1.64  by (Simp_tac 1);
    1.65  qed"is_exec_fragC_UU";
    1.66  
    1.67 -Goal "(is_exec_fragC A`nil) s = TT";
    1.68 +Goal "(is_exec_fragC A$nil) s = TT";
    1.69  by (stac is_exec_fragC_unfold 1);
    1.70  by (Simp_tac 1);
    1.71  qed"is_exec_fragC_nil";
    1.72  
    1.73 -Goal "(is_exec_fragC A`(pr>>xs)) s = \
    1.74 +Goal "(is_exec_fragC A$(pr>>xs)) s = \
    1.75  \                        (Def ((s,pr):trans_of A) \
    1.76 -\                andalso (is_exec_fragC A`xs)(snd pr))";
    1.77 +\                andalso (is_exec_fragC A$xs)(snd pr))";
    1.78  by (rtac trans 1);
    1.79  by (stac is_exec_fragC_unfold 1);
    1.80  by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
    1.81 @@ -163,7 +163,7 @@
    1.82     take the detour of schedules *)
    1.83  
    1.84  Goalw  [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] 
    1.85 -"has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))";
    1.86 +"has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))";
    1.87  
    1.88  by (safe_tac set_cs);
    1.89  (* 1 *)
    1.90 @@ -173,7 +173,7 @@
    1.91  by (Simp_tac 1);
    1.92  by (Asm_simp_tac 1);
    1.93  (* 2 *)
    1.94 -by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1);
    1.95 +by (res_inst_tac[("x","filter_act$(snd ex)")] bexI 1);
    1.96  by (stac beta_cfun 1);
    1.97  by (cont_tacR 1);
    1.98  by (Simp_tac 1);
    1.99 @@ -195,7 +195,7 @@
   1.100  
   1.101  Goal 
   1.102    "!! A. is_trans_of A ==> \
   1.103 -\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act`xs)";
   1.104 +\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)";
   1.105  
   1.106  by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
   1.107  (* main case *)
   1.108 @@ -206,7 +206,7 @@
   1.109  
   1.110  Goal 
   1.111    "!! A.[|  is_trans_of A; x:executions A |] ==> \
   1.112 -\ Forall (%a. a:act A) (filter_act`(snd x))";
   1.113 +\ Forall (%a. a:act A) (filter_act$(snd x))";
   1.114  
   1.115  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   1.116  by (pair_tac "x" 1);