# HG changeset patch
# User nipkow
# Date 900496939 -7200
# Node ID 1ea751ae62b2116dcde715fb501bf6cea1c0bd83
# Parent  963aff0818c2592ae7cecf2c6356f77c7025391b
@ -> $

diff -r 963aff0818c2 -r 1ea751ae62b2 src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Wed Jul 15 11:15:57 1998 +0200
+++ b/src/HOL/Lambda/Eta.ML	Wed Jul 15 12:02:19 1998 +0200
@@ -14,10 +14,10 @@
 Addsimps eta.intrs;
 
 val eta_cases = map (eta.mk_cases dB.simps)
-    ["Abs s -e> z","s @ t -e> u","Var i -e> t"];
+    ["Abs s -e> z","s $ t -e> u","Var i -e> t"];
 
 val beta_cases = map (beta.mk_cases dB.simps)
-    ["s @ t -> u","Var i -> t"];
+    ["s $ t -> u","Var i -> t"];
 
 AddIs eta.intrs;
 AddSEs (beta_cases@eta_cases);
@@ -94,17 +94,17 @@
 by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_Abs";
 
-Goal "s -e>> s' ==> s @ t -e>> s' @ t";
+Goal "s -e>> s' ==> s $ t -e>> s' $ t";
 by (etac rtrancl_induct 1);
 by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_AppL";
 
-Goal "t -e>> t' ==> s @ t -e>> s @ t'";
+Goal "t -e>> t' ==> s $ t -e>> s $ t'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_AppR";
 
-Goal "[| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
+Goal "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'";
 by (blast_tac (claset() addSIs [rtrancl_eta_AppL, rtrancl_eta_AppR]
                        addIs [rtrancl_trans]) 1);
 qed "rtrancl_eta_App";
@@ -163,7 +163,7 @@
                     beta_confluent,eta_confluent,square_beta_eta] 1));
 qed "confluent_beta_eta";
 
-section "Implicit definition of -e>: Abs(lift s 0 @ Var 0) -e> s";
+section "Implicit definition of -e>: Abs(lift s 0 $ Var 0) -e> s";
 
 Goal "!i. (~free s i) = (? t. s = lift t i)";
 by (dB.induct_tac "s" 1);
@@ -189,7 +189,7 @@
  by (rtac iffI 1);
   by (REPEAT(eresolve_tac [conjE,exE] 1));
   by (rename_tac "u1 u2" 1);
-  by (res_inst_tac [("x","u1@u2")] exI 1);
+  by (res_inst_tac [("x","u1$u2")] exI 1);
   by (Asm_simp_tac 1);
  by (etac exE 1);
  by (etac rev_mp 1);
@@ -214,7 +214,7 @@
 by (Blast_tac 1);
 qed_spec_mp "not_free_iff_lifted";
 
-Goal "(!s u. (~free s 0) --> R(Abs(s @ Var 0))(s[u/0])) = \
-\     (!s. R(Abs(lift s 0 @ Var 0))(s))";
+Goal "(!s u. (~free s 0) --> R(Abs(s $ Var 0))(s[u/0])) = \
+\     (!s. R(Abs(lift s 0 $ Var 0))(s))";
 by (fast_tac (HOL_cs addss (simpset() addsimps [not_free_iff_lifted])) 1);
 qed "explicit_is_implicit";
diff -r 963aff0818c2 -r 1ea751ae62b2 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Wed Jul 15 11:15:57 1998 +0200
+++ b/src/HOL/Lambda/Eta.thy	Wed Jul 15 12:02:19 1998 +0200
@@ -21,14 +21,14 @@
 
 primrec free Lambda.dB
   "free (Var j) i = (j=i)"
-  "free (s @ t) i = (free s i | free t i)"
+  "free (s $ t) i = (free s i | free t i)"
   "free (Abs s) i = free s (Suc i)"
 
 inductive eta
 intrs
-   eta  "~free s 0 ==> Abs(s @ Var 0) -e> s[dummy/0]"
-   appL  "s -e> t ==> s@u -e> t@u"
-   appR  "s -e> t ==> u@s -e> u@t"
+   eta  "~free s 0 ==> Abs(s $ Var 0) -e> s[dummy/0]"
+   appL  "s -e> t ==> s$u -e> t$u"
+   appR  "s -e> t ==> u$s -e> u$t"
    abs   "s -e> t ==> Abs s -e> Abs t"
 end
 
diff -r 963aff0818c2 -r 1ea751ae62b2 src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Wed Jul 15 11:15:57 1998 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Wed Jul 15 12:02:19 1998 +0200
@@ -27,17 +27,17 @@
 qed "rtrancl_beta_Abs";
 AddSIs [rtrancl_beta_Abs];
 
-Goal "s ->> s' ==> s @ t ->> s' @ t";
+Goal "s ->> s' ==> s $ t ->> s' $ t";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_AppL";
 
-Goal "t ->> t' ==> s @ t ->> s @ t'";
+Goal "t ->> t' ==> s $ t ->> s $ t'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_AppR";
 
-Goal "[| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
+Goal "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'";
 by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
                        addIs  [rtrancl_trans]) 1);
 qed "rtrancl_beta_App";
diff -r 963aff0818c2 -r 1ea751ae62b2 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Wed Jul 15 11:15:57 1998 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Wed Jul 15 12:02:19 1998 +0200
@@ -9,7 +9,7 @@
 
 Lambda = Arith + Inductive +
 
-datatype dB = Var nat | "@" dB dB (infixl 200) | Abs dB
+datatype dB = Var nat | "$" dB dB (infixl 200) | Abs dB
 
 consts
   subst  :: [dB,dB,nat]=>dB ("_[_'/_]" [300,0,0] 300)
@@ -20,24 +20,24 @@
 
 primrec lift dB
   "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
-  "lift (s @ t) k = (lift s k) @ (lift t k)"
+  "lift (s $ t) k = (lift s k) $ (lift t k)"
   "lift (Abs s) k = Abs(lift s (Suc k))"
 
 primrec subst dB
   subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
                             else if i = k then s else Var i)"
-  subst_App "(t @ u)[s/k] = t[s/k] @ u[s/k]"
+  subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]"
   subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
 
 primrec liftn dB
   "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
-  "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)"
+  "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)"
   "liftn n (Abs s) k = Abs(liftn n s (Suc k))"
 
 primrec substn dB
   "substn (Var i) s k = (if k < i then Var(i-1)
                          else if i = k then liftn k s 0 else Var i)"
-  "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
+  "substn (t $ u) s k = (substn t s k) $ (substn u s k)"
   "substn (Abs t) s k = Abs (substn t s (Suc k))"
 
 consts  beta :: "(dB * dB) set"
@@ -50,8 +50,8 @@
 
 inductive beta
 intrs
-   beta  "(Abs s) @ t -> s[t/0]"
-   appL  "s -> t ==> s@u -> t@u"
-   appR  "s -> t ==> u@s -> u@t"
+   beta  "(Abs s) $ t -> s[t/0]"
+   appL  "s -> t ==> s$u -> t$u"
+   appR  "s -> t ==> u$s -> u$t"
    abs   "s -> t ==> Abs s -> Abs t"
 end
diff -r 963aff0818c2 -r 1ea751ae62b2 src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Wed Jul 15 11:15:57 1998 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Wed Jul 15 12:02:19 1998 +0200
@@ -13,7 +13,7 @@
 
 val par_beta_cases = map (par_beta.mk_cases dB.simps)
     ["Var n => t", "Abs s => Abs t",
-     "(Abs s) @ t => u", "s @ t => u", "Abs s => t"];
+     "(Abs s) $ t => u", "s $ t => u", "Abs s => t"];
 
 AddSIs par_beta.intrs;
 AddSEs par_beta_cases;
diff -r 963aff0818c2 -r 1ea751ae62b2 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Wed Jul 15 11:15:57 1998 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Wed Jul 15 12:02:19 1998 +0200
@@ -19,26 +19,16 @@
   intrs
     var   "Var n => Var n"
     abs   "s => t ==> Abs s => Abs t"
-    app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
-    beta  "[| s => s'; t => t' |] ==> (Abs s) @ t => s'[t'/0]"
+    app   "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
+    beta  "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
 
 consts
   cd  :: dB => dB
 
 recdef cd "measure size"
   "cd(Var n) = Var n"
-  "cd(Var n @ t) = Var n @ cd t"
-  "cd((s1 @ s2) @ t) = cd(s1 @ s2) @ cd t"
-  "cd(Abs u @ t) = (cd u)[cd t/0]"
-(*
-  "cd(s @ t) = (case s of Var n   => (s @ cd t)
-                        | s1 @ s2 => (cd s @ cd t) 
-                        | Abs u   => deAbs(cd s)[cd t/0])"
-*)
+  "cd(Var n     $ t) = Var n $ cd t"
+  "cd((s1 $ s2) $ t) = cd(s1 $ s2) $ cd t"
+  "cd(Abs u     $ t) = (cd u)[cd t/0]"
   "cd(Abs s) = Abs(cd s)"
-(*
-primrec deAbs dB
-  "deAbs(Var n) = Var n"
-  "deAbs(s @ t) = s @ t"
-  "deAbs(Abs s) = s"*)
 end