Renamed '$' to 'Scons' because of clashes with constants of the same
name in theories using datatypes.
--- 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
--- 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*)
--- 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,
--- 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
--- 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";
--- 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
--- 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]));
--- 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'))})"