# HG changeset patch
# User berghofe
# Date 901280387 -7200
# Node ID 8ceaa19f771712c07d8f073e1877b71e9d08104c
# Parent  4ae03162259259943a6ef0615ce9cb16bfbf68ba
Renamed '$' to 'Scons' because of clashes with constants of the same
name in theories using datatypes.

diff -r 4ae031622592 -r 8ceaa19f7717 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Fri Jul 24 13:36:49 1998 +0200
+++ b/src/HOL/Induct/SList.thy	Fri Jul 24 13:39:47 1998 +0200
@@ -62,8 +62,8 @@
 
 defs
   (* Defining the Concrete Constructors *)
-  NIL_def       "NIL == In0(Numb(0))"
-  CONS_def      "CONS M N == In1(M $ N)"
+  NIL_def       "NIL == In0 (Numb 0)"
+  CONS_def      "CONS M N == In1 (Scons M N)"
 
 inductive "list(A)"
   intrs
diff -r 4ae031622592 -r 8ceaa19f7717 src/HOL/Induct/Simult.thy
--- a/src/HOL/Induct/Simult.thy	Fri Jul 24 13:36:49 1998 +0200
+++ b/src/HOL/Induct/Simult.thy	Fri Jul 24 13:39:47 1998 +0200
@@ -40,7 +40,7 @@
 
 defs
      (*the concrete constants*)
-  TCONS_def     "TCONS M N == In0(M $ N)"
+  TCONS_def     "TCONS M N == In0 (Scons M N)"
   FNIL_def      "FNIL      == In1(NIL)"
   FCONS_def     "FCONS M N == In1(CONS M N)"
      (*the abstract constants*)
diff -r 4ae031622592 -r 8ceaa19f7717 src/HOL/Induct/Term.ML
--- a/src/HOL/Induct/Term.ML	Fri Jul 24 13:36:49 1998 +0200
+++ b/src/HOL/Induct/Term.ML	Fri Jul 24 13:39:47 1998 +0200
@@ -38,7 +38,7 @@
 val [major,minor] = goal Term.thy 
     "[| M: term(A);  \
 \       !!x zs. [| x: A;  zs: list(term(A));  zs: list({x. R(x)}) \
-\               |] ==> R(x$zs)  \
+\               |] ==> R (Scons x zs)  \
 \    |] ==> R(M)";
 by (rtac (major RS term.induct) 1);
 by (REPEAT (eresolve_tac ([minor] @
@@ -49,9 +49,9 @@
 (*Induction on term(A) followed by induction on list *)
 val major::prems = goal Term.thy
     "[| M: term(A);  \
-\       !!x.      [| x: A |] ==> R(x$NIL);  \
-\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  R(x$zs)  \
-\                 |] ==> R(x $ CONS z zs)  \
+\       !!x.      [| x: A |] ==> R (Scons x NIL);  \
+\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  R (Scons x zs)  \
+\                 |] ==> R (Scons x (CONS z zs))  \
 \    |] ==> R(M)";
 by (rtac (major RS Term_induct) 1);
 by (etac list.induct 1);
@@ -139,7 +139,7 @@
 
 val [prem1,prem2,A_subset_sexp] = goal Term.thy
     "[| M: sexp;  N: list(term(A));  A<=sexp |] ==> \
-\    Term_rec (M$N) d = d M N (Abs_map (%Z. Term_rec Z d) N)";
+\    Term_rec (Scons M N) d = d M N (Abs_map (%Z. Term_rec Z d) N)";
 by (rtac (Term_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps
       [Split,
diff -r 4ae031622592 -r 8ceaa19f7717 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Fri Jul 24 13:36:49 1998 +0200
+++ b/src/HOL/Induct/Term.thy	Fri Jul 24 13:39:47 1998 +0200
@@ -6,7 +6,7 @@
 Terms over a given alphabet -- function applications; illustrates list functor
   (essentially the same type as in Trees & Forests)
 
-There is no constructor APP because it is simply cons ($) 
+There is no constructor APP because it is simply Scons
 *)
 
 Term = SList +
@@ -27,7 +27,7 @@
 
 inductive "term(A)"
   intrs
-    APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
+    APP_I "[| M: A;  N : list(term(A)) |] ==> Scons M N : term(A)"
   monos   "[list_mono]"
 
 defs
@@ -36,7 +36,7 @@
   Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
 
   (*defining the abstract constants*)
-  App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
+  App_def       "App a ts == Abs_term(Scons (Leaf a) (Rep_Tlist ts))"
 
   (*list recursion*)
   Term_rec_def  
diff -r 4ae031622592 -r 8ceaa19f7717 src/HOL/Sexp.ML
--- a/src/HOL/Sexp.ML	Fri Jul 24 13:36:49 1998 +0200
+++ b/src/HOL/Sexp.ML	Fri Jul 24 13:39:47 1998 +0200
@@ -18,7 +18,7 @@
 by (Blast_tac 1);
 qed "sexp_case_Numb";
 
-Goalw [sexp_case_def] "sexp_case c d e (M$N) = e M N";
+Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N";
 by (Blast_tac 1);
 qed "sexp_case_Scons";
 
@@ -41,7 +41,7 @@
 by (Blast_tac 1);
 qed "range_Leaf_subset_sexp";
 
-val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
+val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp";
 by (rtac (major RS setup_induction) 1);
 by (etac sexp.induct 1);
 by (ALLGOALS Blast_tac);
@@ -60,12 +60,12 @@
     pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
 
 Goalw [pred_sexp_def]
-    "!!M. [| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
+    "!!M. [| M: sexp;  N: sexp |] ==> (M, Scons M N) : pred_sexp";
 by (Blast_tac 1);
 qed "pred_sexpI1";
 
 Goalw [pred_sexp_def]
-    "!!M. [| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
+    "!!M. [| M: sexp;  N: sexp |] ==> (N, Scons M N) : pred_sexp";
 by (Blast_tac 1);
 qed "pred_sexpI2";
 
@@ -82,8 +82,8 @@
 
 val major::prems = goalw Sexp.thy [pred_sexp_def]
     "[| p : pred_sexp;                                       \
-\       !!M N. [| p = (M, M$N);  M: sexp;  N: sexp |] ==> R; \
-\       !!M N. [| p = (N, M$N);  M: sexp;  N: sexp |] ==> R  \
+\       !!M N. [| p = (M, Scons M N);  M: sexp;  N: sexp |] ==> R; \
+\       !!M N. [| p = (N, Scons M N);  M: sexp;  N: sexp |] ==> R  \
 \    |] ==> R";
 by (cut_facts_tac [major] 1);
 by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
@@ -125,7 +125,7 @@
 qed "sexp_rec_Numb";
 
 Goal "[| M: sexp;  N: sexp |] ==> \
-\    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
+\    sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
 by (rtac (sexp_rec_unfold RS trans) 1);
 by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
 qed "sexp_rec_Scons";
diff -r 4ae031622592 -r 8ceaa19f7717 src/HOL/Sexp.thy
--- a/src/HOL/Sexp.thy	Fri Jul 24 13:36:49 1998 +0200
+++ b/src/HOL/Sexp.thy	Fri Jul 24 13:39:47 1998 +0200
@@ -22,17 +22,17 @@
   intrs
     LeafI  "Leaf(a): sexp"
     NumbI  "Numb(i): sexp"
-    SconsI "[| M: sexp;  N: sexp |] ==> M$N : sexp"
+    SconsI "[| M: sexp;  N: sexp |] ==> Scons M N : sexp"
 
 defs
 
   sexp_case_def 
    "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
                             | (? k.   M=Numb(k) & z=d(k))  
-                            | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
+                            | (? N1 N2. M = Scons N1 N2  & z=e N1 N2)"
 
   pred_sexp_def
-     "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"
+     "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"
 
   sexp_rec_def
    "sexp_rec M c d e == wfrec pred_sexp
diff -r 4ae031622592 -r 8ceaa19f7717 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Fri Jul 24 13:36:49 1998 +0200
+++ b/src/HOL/Univ.ML	Fri Jul 24 13:39:47 1998 +0200
@@ -82,7 +82,7 @@
 
 (** Scons vs Atom **)
 
-Goalw [Atom_def,Scons_def,Push_Node_def] "(M$N) ~= Atom(a)";
+Goalw [Atom_def,Scons_def,Push_Node_def] "Scons M N ~= Atom(a)";
 by (rtac notI 1);
 by (etac (equalityD2 RS subsetD RS UnE) 1);
 by (rtac singletonI 1);
@@ -112,7 +112,7 @@
 by (etac (Atom_inject RS Inl_inject) 1);
 qed "inj_Leaf";
 
-val Leaf_inject = inj_Leaf RS injD;
+bind_thm ("Leaf_inject", inj_Leaf RS injD);
 AddSDs [Leaf_inject];
 
 Goalw [Numb_def,o_def] "inj(Numb)";
@@ -142,31 +142,31 @@
 
 (** Injectiveness of Scons **)
 
-Goalw [Scons_def] "M$N <= M'$N' ==> M<=M'";
+Goalw [Scons_def] "Scons M N <= Scons M' N' ==> M<=M'";
 by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma1";
 
-Goalw [Scons_def] "M$N <= M'$N' ==> N<=N'";
+Goalw [Scons_def] "Scons M N <= Scons M' N' ==> N<=N'";
 by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma2";
 
-val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
+val [major] = goal Univ.thy "Scons M N = Scons M' N' ==> M=M'";
 by (rtac (major RS equalityE) 1);
 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
 qed "Scons_inject1";
 
-val [major] = goal Univ.thy "M$N = M'$N' ==> N=N'";
+val [major] = goal Univ.thy "Scons M N = Scons M' N' ==> N=N'";
 by (rtac (major RS equalityE) 1);
 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
 qed "Scons_inject2";
 
 val [major,minor] = goal Univ.thy
-    "[| M$N = M'$N';  [| M=M';  N=N' |] ==> P \
+    "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P \
 \    |] ==> P";
 by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
 qed "Scons_inject";
 
-Goal "(M$N = M'$N') = (M=M' & N=N')";
+Goal "(Scons M N = Scons M' N') = (M=M' & N=N')";
 by (blast_tac (claset() addSEs [Scons_inject]) 1);
 qed "Scons_Scons_eq";
 
@@ -174,7 +174,7 @@
 
 (** Scons vs Leaf **)
 
-Goalw [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
+Goalw [Leaf_def,o_def] "Scons M N ~= Leaf(a)";
 by (rtac Scons_not_Atom 1);
 qed "Scons_not_Leaf";
 bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym);
@@ -184,7 +184,7 @@
 
 (** Scons vs Numb **)
 
-Goalw [Numb_def,o_def] "(M$N) ~= Numb(k)";
+Goalw [Numb_def,o_def] "Scons M N ~= Numb(k)";
 by (rtac Scons_not_Atom 1);
 qed "Scons_not_Numb";
 bind_thm ("Numb_not_Scons", Scons_not_Numb RS not_sym);
@@ -257,7 +257,7 @@
 qed "ntrunc_Numb";
 
 Goalw [Scons_def,ntrunc_def]
-    "ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N";
+    "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)";
 by (safe_tac (claset() addSIs [imageI]));
 by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
 by (REPEAT (rtac Suc_less_SucD 1 THEN 
@@ -297,14 +297,14 @@
 
 (*** Cartesian Product ***)
 
-Goalw [uprod_def] "[| M:A;  N:B |] ==> (M$N) : A<*>B";
+Goalw [uprod_def] "[| M:A;  N:B |] ==> Scons M N : A<*>B";
 by (REPEAT (ares_tac [singletonI,UN_I] 1));
 qed "uprodI";
 
 (*The general elimination rule*)
 val major::prems = goalw Univ.thy [uprod_def]
     "[| c : A<*>B;  \
-\       !!x y. [| x:A;  y:B;  c=x$y |] ==> P \
+\       !!x y. [| x:A;  y:B;  c = Scons x y |] ==> P \
 \    |] ==> P";
 by (cut_facts_tac [major] 1);
 by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1
@@ -313,7 +313,7 @@
 
 (*Elimination of a pair -- introduces no eigenvariables*)
 val prems = goal Univ.thy
-    "[| (M$N) : A<*>B;      [| M:A;  N:B |] ==> P   \
+    "[| Scons M N : A<*>B;      [| M:A;  N:B |] ==> P   \
 \    |] ==> P";
 by (rtac uprodE 1);
 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Scons_inject,ssubst] 1));
@@ -416,7 +416,7 @@
 by (Blast_tac 1);
 qed "usum_mono";
 
-Goalw [Scons_def] "[| M<=M';  N<=N' |] ==> M$N <= M'$N'";
+Goalw [Scons_def] "[| M<=M';  N<=N' |] ==> Scons M N <= Scons M' N'";
 by (Blast_tac 1);
 qed "Scons_mono";
 
@@ -431,7 +431,7 @@
 
 (*** Split and Case ***)
 
-Goalw [Split_def] "Split c (M$N) = c M N";
+Goalw [Split_def] "Split c (Scons M N) = c M N";
 by (Blast_tac  1);
 qed "Split";
 
@@ -452,11 +452,11 @@
 by (Blast_tac 1);
 qed "ntrunc_UN1";
 
-Goalw [Scons_def] "(UN x. f(x)) $ M = (UN x. f(x) $ M)";
+Goalw [Scons_def] "Scons (UN x. f x) M = (UN x. Scons (f x) M)";
 by (Blast_tac 1);
 qed "Scons_UN1_x";
 
-Goalw [Scons_def] "M $ (UN x. f(x)) = (UN x. M $ f(x))";
+Goalw [Scons_def] "Scons M (UN x. f x) = (UN x. Scons M (f x))";
 by (Blast_tac 1);
 qed "Scons_UN1_y";
 
@@ -489,14 +489,14 @@
 (*** Equality for Cartesian Product ***)
 
 Goalw [dprod_def]
-    "[| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
+    "[| (M,M'):r;  (N,N'):s |] ==> (Scons M N, Scons M' N') : r<**>s";
 by (Blast_tac 1);
 qed "dprodI";
 
 (*The general elimination rule*)
 val major::prems = goalw Univ.thy [dprod_def]
     "[| c : r<**>s;  \
-\       !!x y x' y'. [| (x,x') : r;  (y,y') : s;  c = (x$y,x'$y') |] ==> P \
+\       !!x y x' y'. [| (x,x') : r;  (y,y') : s;  c = (Scons x y, Scons x' y') |] ==> P \
 \    |] ==> P";
 by (cut_facts_tac [major] 1);
 by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, mem_splitE, singletonE]));
diff -r 4ae031622592 -r 8ceaa19f7717 src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Fri Jul 24 13:36:49 1998 +0200
+++ b/src/HOL/Univ.thy	Fri Jul 24 13:39:47 1998 +0200
@@ -31,7 +31,7 @@
   Atom      :: "('a+nat) => 'a item"
   Leaf      :: 'a => 'a item
   Numb      :: nat => 'a item
-  "$"       :: ['a item, 'a item]=> 'a item   (infixr 60)
+  Scons     :: ['a item, 'a item]=> 'a item
   In0,In1   :: 'a item => 'a item
 
   ntrunc    :: [nat, 'a item] => 'a item
@@ -63,26 +63,26 @@
 
   (*S-expression constructors*)
   Atom_def   "Atom == (%x. {Abs_Node((%k.0, x))})"
-  Scons_def  "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
+  Scons_def  "Scons M N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
 
   (*Leaf nodes, with arbitrary or nat labels*)
   Leaf_def   "Leaf == Atom o Inl"
   Numb_def   "Numb == Atom o Inr"
 
   (*Injections of the "disjoint sum"*)
-  In0_def    "In0(M) == Numb(0) $ M"
-  In1_def    "In1(M) == Numb(Suc(0)) $ M"
+  In0_def    "In0(M) == Scons (Numb 0) M"
+  In1_def    "In1(M) == Scons (Numb 1) M"
 
   (*the set of nodes with depth less than k*)
   ndepth_def "ndepth(n) == (%(f,x). LEAST k. f(k)=0) (Rep_Node n)"
   ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"
 
   (*products and sums for the "universe"*)
-  uprod_def  "A<*>B == UN x:A. UN y:B. { (x$y) }"
+  uprod_def  "A<*>B == UN x:A. UN y:B. { Scons x y }"
   usum_def   "A<+>B == In0``A Un In1``B"
 
   (*the corresponding eliminators*)
-  Split_def  "Split c M == @u. ? x y. M = x$y & u = c x y"
+  Split_def  "Split c M == @u. ? x y. M = Scons x y & u = c x y"
 
   Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) 
                               | (? y . M = In1(y) & u = d(y))"
@@ -92,7 +92,7 @@
 
   diag_def   "diag(A) == UN x:A. {(x,x)}"
 
-  dprod_def  "r<**>s == UN (x,x'):r. UN (y,y'):s. {(x$y,x'$y')}"
+  dprod_def  "r<**>s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
 
   dsum_def   "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 
                        (UN (y,y'):s. {(In1(y),In1(y'))})"