# HG changeset patch
# User wenzelm
# Date 934898372 -7200
# Node ID 6773ba0c36d5991cd30d6b708e4ef21aa8a06533
# Parent  ddb67dcf026c75f0aa68ad0a5b07283083f8cc81
renamed Cons to Consq in order to avoid clash with List.Cons;

diff -r ddb67dcf026c -r 6773ba0c36d5 src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Tue Aug 17 15:59:32 1999 +0200
@@ -110,7 +110,7 @@
 \                andalso (stutter2 sig`xs) (snd at))"; 
 by (rtac trans 1);
 by (stac stutter2_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def,If_and_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1);
 by (Simp_tac 1);
 qed"stutter2_cons";
 
diff -r ddb67dcf026c -r 6773ba0c36d5 src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Aug 17 15:59:32 1999 +0200
@@ -71,8 +71,8 @@
 \       (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
 by (rtac trans 1);
 by (stac mkex2_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"mkex2_cons_1";
 
 Goal "[| x~:act A; x:act B; HD`exB=Def b|] \
@@ -80,8 +80,8 @@
 \       (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
 by (rtac trans 1);
 by (stac mkex2_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"mkex2_cons_2";
 
 Goal "[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
@@ -90,8 +90,8 @@
 \           (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
 by (rtac trans 1);
 by (stac mkex2_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"mkex2_cons_3";
 
 Addsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
diff -r ddb67dcf026c -r 6773ba0c36d5 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Aug 17 15:59:32 1999 +0200
@@ -67,8 +67,8 @@
 \                             `schB))";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"mksch_cons1";
 
 Goal "[|x~:act A;x:act B|] \
@@ -78,8 +78,8 @@
 \                            ))";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"mksch_cons2";
 
 Goal "[|x:act A;x:act B|] \
@@ -91,8 +91,8 @@
 \             )";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"mksch_cons3";
 
 val compotr_simps =[mksch_UU,mksch_nil, mksch_cons1,mksch_cons2,mksch_cons3];
diff -r ddb67dcf026c -r 6773ba0c36d5 src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Tue Aug 17 15:59:32 1999 +0200
@@ -45,7 +45,7 @@
 \          @@ ((corresp_exC A f`xs) (snd at))";
 by (rtac trans 1);
 by (stac corresp_exC_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
 by (Simp_tac 1);
 qed"corresp_exC_cons";
 
diff -r ddb67dcf026c -r 6773ba0c36d5 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Aug 17 15:59:32 1999 +0200
@@ -27,7 +27,7 @@
 qed"Map_nil";
 
 Goal "Map f`(x>>xs)=(f x) >> Map f`xs";
-by (simp_tac (simpset() addsimps [Map_def, Cons_def,flift2_def]) 1);
+by (simp_tac (simpset() addsimps [Map_def, Consq_def,flift2_def]) 1);
 qed"Map_cons";
 
 (* ---------------------------------------------------------------- *)
@@ -43,7 +43,7 @@
 qed"Filter_nil";
 
 Goal "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)"; 
-by (simp_tac (simpset() addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Filter_def, Consq_def,flift2_def,If_and_if]) 1);
 qed"Filter_cons";
 
 (* ---------------------------------------------------------------- *)
@@ -60,7 +60,7 @@
 
 Goal "Forall P (x>>xs)= (P x & Forall P xs)";
 by (simp_tac (simpset() addsimps [Forall_def, sforall_def,
-                                 Cons_def,flift2_def]) 1);
+                                 Consq_def,flift2_def]) 1);
 qed"Forall_cons";
 
 (* ---------------------------------------------------------------- *)
@@ -69,7 +69,7 @@
 
 
 Goal "(x>>xs) @@ y = x>>(xs @@y)"; 
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"Conc_cons";
 
 (* ---------------------------------------------------------------- *)
@@ -85,7 +85,7 @@
 qed"Takewhile_nil";
 
 Goal "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)"; 
-by (simp_tac (simpset() addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Takewhile_def, Consq_def,flift2_def,If_and_if]) 1);
 qed"Takewhile_cons";
 
 (* ---------------------------------------------------------------- *)
@@ -101,7 +101,7 @@
 qed"Dropwhile_nil";
 
 Goal "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)"; 
-by (simp_tac (simpset() addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Dropwhile_def, Consq_def,flift2_def,If_and_if]) 1);
 qed"Dropwhile_cons";
 
 (* ---------------------------------------------------------------- *)
@@ -118,7 +118,7 @@
 qed"Last_nil";
 
 Goal "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)"; 
-by (simp_tac (simpset() addsimps [Last_def, Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Last_def, Consq_def]) 1);
 by (res_inst_tac [("x","xs")] seq.casedist 1);
 by (Asm_simp_tac 1);
 by (REPEAT (Asm_simp_tac 1));
@@ -138,7 +138,7 @@
 qed"Flat_nil";
 
 Goal "Flat`(x##xs)= x @@ (Flat`xs)"; 
-by (simp_tac (simpset() addsimps [Flat_def, Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Flat_def, Consq_def]) 1);
 qed"Flat_cons";
 
 
@@ -181,14 +181,14 @@
 
 Goal "Zip`(x>>xs)`nil= UU"; 
 by (stac Zip_unfold 1);
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"Zip_cons_nil";
 
 Goal "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys"; 
 by (rtac trans 1);
 by (stac Zip_unfold 1);
 by (Simp_tac 1);
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"Zip_cons";
 
 
@@ -219,11 +219,11 @@
 section "Cons";
 
 Goal "a>>s = (Def a)##s";
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
-qed"Cons_def2";
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
+qed"Consq_def2";
 
 Goal "x = UU | x = nil | (? a s. x = a >> s)";
-by (simp_tac (simpset() addsimps [Cons_def2]) 1);
+by (simp_tac (simpset() addsimps [Consq_def2]) 1);
 by (cut_facts_tac [seq.exhaust] 1);
 by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1);
 qed"Seq_exhaust";
@@ -248,7 +248,7 @@
                                              THEN Asm_full_simp_tac i;
 
 Goal "a>>s ~= UU";
-by (stac Cons_def2 1);
+by (stac Consq_def2 1);
 by (resolve_tac seq.con_rews 1);
 by (rtac Def_not_UU 1);
 qed"Cons_not_UU";
@@ -262,22 +262,22 @@
 qed"Cons_not_less_UU";
 
 Goal "~a>>s << nil";
-by (stac Cons_def2 1);
+by (stac Consq_def2 1);
 by (resolve_tac seq.rews 1);
 by (rtac Def_not_UU 1);
 qed"Cons_not_less_nil";
 
 Goal "a>>s ~= nil";
-by (stac Cons_def2 1);
+by (stac Consq_def2 1);
 by (resolve_tac seq.rews 1);
 qed"Cons_not_nil";
 
 Goal "nil ~= a>>s";
-by (simp_tac (simpset() addsimps [Cons_def2]) 1);
+by (simp_tac (simpset() addsimps [Consq_def2]) 1);
 qed"Cons_not_nil2";
 
 Goal "(a>>s = b>>t) = (a = b & s = t)";
-by (simp_tac (HOL_ss addsimps [Cons_def2]) 1);
+by (simp_tac (HOL_ss addsimps [Consq_def2]) 1);
 by (stac (hd lift.inject RS sym) 1);
 back(); back();
 by (rtac scons_inject_eq 1);
@@ -285,7 +285,7 @@
 qed"Cons_inject_eq";
 
 Goal "(a>>s<<b>>t) = (a = b & s<<t)";
-by (simp_tac (simpset() addsimps [Cons_def2]) 1);
+by (simp_tac (simpset() addsimps [Consq_def2]) 1);
 by (stac (Def_inject_less_eq RS sym) 1);
 back();
 by (rtac iffI 1);
@@ -299,7 +299,7 @@
 qed"Cons_inject_less_eq";
 
 Goal "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)";
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"seq_take_Cons";
 
 Addsimps [Cons_not_nil2,Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
@@ -322,7 +322,7 @@
 by (etac seq.ind 1);
 by (REPEAT (atac 1));
 by (def_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"Seq_induct";
 
 Goal "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]  \
@@ -330,14 +330,14 @@
 by (etac seq_finite_ind 1);
 by (REPEAT (atac 1));
 by (def_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"Seq_FinitePartial_ind";
 
 Goal "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
 by (etac sfinite.induct 1);
 by (assume_tac 1);
 by (def_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"Seq_Finite_ind"; 
 
 
@@ -366,11 +366,11 @@
 section "HD,TL";
 
 Goal "HD`(x>>y) = Def x";
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"HD_Cons";
 
 Goal "TL`(x>>y) = y";
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"TL_Cons";
 
 Addsimps [HD_Cons,TL_Cons];
@@ -380,7 +380,7 @@
 section "Finite, Partial, Infinite";
 
 Goal "Finite (a>>xs) = Finite xs";
-by (simp_tac (simpset() addsimps [Cons_def2,Finite_cons]) 1);
+by (simp_tac (simpset() addsimps [Consq_def2,Finite_cons]) 1);
 qed"Finite_Cons";
 
 Addsimps [Finite_Cons];
diff -r ddb67dcf026c -r 6773ba0c36d5 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Aug 17 15:59:32 1999 +0200
@@ -15,7 +15,7 @@
 
 consts
 
-  Cons             ::"'a            => 'a Seq -> 'a Seq"
+  Consq            ::"'a            => 'a Seq -> 'a Seq"
   Filter           ::"('a => bool)  => 'a Seq -> 'a Seq"
   Map              ::"('a => 'b)    => 'a Seq -> 'b Seq"
   Forall           ::"('a => bool)  => 'a Seq => bool"
@@ -29,7 +29,7 @@
 
 syntax
 
- "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_/>>_)"  [66,65] 65)
+ "@Consq"         ::"'a => 'a Seq => 'a Seq"       ("(_/>>_)"  [66,65] 65)
  (* list Enumeration *)
   "_totlist"      :: args => 'a Seq                          ("[(_)!]")
   "_partlist"     :: args => 'a Seq                          ("[(_)?]")
@@ -37,12 +37,12 @@
 
 syntax (symbols)
 
- "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_\\<leadsto>_)"  [66,65] 65)
+ "@Consq"     ::"'a => 'a Seq => 'a Seq"       ("(_\\<leadsto>_)"  [66,65] 65)
  
 
 translations
 
-  "a>>s" == "Cons a`s"
+  "a>>s"         == "Consq a`s"
   "[x, xs!]"     == "x>>[xs!]"
   "[x!]"         == "x>>nil"
   "[x, xs?]"     == "x>>[xs?]"
@@ -51,7 +51,7 @@
 defs
 
 
-Cons_def      "Cons a == LAM s. Def a ## s"
+Consq_def     "Consq a == LAM s. Def a ## s"
 
 Filter_def    "Filter P == sfilter`(flift2 P)"
 
diff -r ddb67dcf026c -r 6773ba0c36d5 src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Aug 17 15:59:32 1999 +0200
@@ -49,8 +49,8 @@
 \          @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";     
 by (rtac trans 1);
 by (stac oraclebuild_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"oraclebuild_cons";
 
 
diff -r ddb67dcf026c -r 6773ba0c36d5 src/HOLCF/IOA/meta_theory/SimCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Tue Aug 17 15:59:32 1999 +0200
@@ -50,7 +50,7 @@
 \             @@ ((corresp_ex_simC A R`xs) T'))";
 by (rtac trans 1);
 by (stac corresp_ex_simC_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
 by (Simp_tac 1);
 qed"corresp_ex_simC_cons";
 
diff -r ddb67dcf026c -r 6773ba0c36d5 src/HOLCF/IOA/meta_theory/TLS.ML
--- a/src/HOLCF/IOA/meta_theory/TLS.ML	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Tue Aug 17 15:59:32 1999 +0200
@@ -44,8 +44,8 @@
 \          (s,Some a,t)>> ((ex2seqC`xs) t)";
 by (rtac trans 1);
 by (stac ex2seqC_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
 qed"ex2seqC_cons";
 
 Addsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons];
diff -r ddb67dcf026c -r 6773ba0c36d5 src/HOLCF/IOA/meta_theory/Traces.ML
--- a/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Aug 17 15:59:32 1999 +0200
@@ -96,7 +96,7 @@
 \                andalso (is_exec_fragC A`xs)(snd pr))";
 by (rtac trans 1);
 by (stac is_exec_fragC_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
 by (Simp_tac 1);
 qed"is_exec_fragC_cons";