--- 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";
--- 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];
--- 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];
--- 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";
--- 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];
--- 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)"
--- 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";
--- 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";
--- 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];
--- 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";