@ -> $
authornipkow
Wed Jul 15 12:02:19 1998 +0200 (1998-07-15)
changeset 51461ea751ae62b2
parent 5145 963aff0818c2
child 5147 825877190618
@ -> $
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ParRed.ML
src/HOL/Lambda/ParRed.thy
     1.1 --- a/src/HOL/Lambda/Eta.ML	Wed Jul 15 11:15:57 1998 +0200
     1.2 +++ b/src/HOL/Lambda/Eta.ML	Wed Jul 15 12:02:19 1998 +0200
     1.3 @@ -14,10 +14,10 @@
     1.4  Addsimps eta.intrs;
     1.5  
     1.6  val eta_cases = map (eta.mk_cases dB.simps)
     1.7 -    ["Abs s -e> z","s @ t -e> u","Var i -e> t"];
     1.8 +    ["Abs s -e> z","s $ t -e> u","Var i -e> t"];
     1.9  
    1.10  val beta_cases = map (beta.mk_cases dB.simps)
    1.11 -    ["s @ t -> u","Var i -> t"];
    1.12 +    ["s $ t -> u","Var i -> t"];
    1.13  
    1.14  AddIs eta.intrs;
    1.15  AddSEs (beta_cases@eta_cases);
    1.16 @@ -94,17 +94,17 @@
    1.17  by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    1.18  qed "rtrancl_eta_Abs";
    1.19  
    1.20 -Goal "s -e>> s' ==> s @ t -e>> s' @ t";
    1.21 +Goal "s -e>> s' ==> s $ t -e>> s' $ t";
    1.22  by (etac rtrancl_induct 1);
    1.23  by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    1.24  qed "rtrancl_eta_AppL";
    1.25  
    1.26 -Goal "t -e>> t' ==> s @ t -e>> s @ t'";
    1.27 +Goal "t -e>> t' ==> s $ t -e>> s $ t'";
    1.28  by (etac rtrancl_induct 1);
    1.29  by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    1.30  qed "rtrancl_eta_AppR";
    1.31  
    1.32 -Goal "[| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
    1.33 +Goal "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'";
    1.34  by (blast_tac (claset() addSIs [rtrancl_eta_AppL, rtrancl_eta_AppR]
    1.35                         addIs [rtrancl_trans]) 1);
    1.36  qed "rtrancl_eta_App";
    1.37 @@ -163,7 +163,7 @@
    1.38                      beta_confluent,eta_confluent,square_beta_eta] 1));
    1.39  qed "confluent_beta_eta";
    1.40  
    1.41 -section "Implicit definition of -e>: Abs(lift s 0 @ Var 0) -e> s";
    1.42 +section "Implicit definition of -e>: Abs(lift s 0 $ Var 0) -e> s";
    1.43  
    1.44  Goal "!i. (~free s i) = (? t. s = lift t i)";
    1.45  by (dB.induct_tac "s" 1);
    1.46 @@ -189,7 +189,7 @@
    1.47   by (rtac iffI 1);
    1.48    by (REPEAT(eresolve_tac [conjE,exE] 1));
    1.49    by (rename_tac "u1 u2" 1);
    1.50 -  by (res_inst_tac [("x","u1@u2")] exI 1);
    1.51 +  by (res_inst_tac [("x","u1$u2")] exI 1);
    1.52    by (Asm_simp_tac 1);
    1.53   by (etac exE 1);
    1.54   by (etac rev_mp 1);
    1.55 @@ -214,7 +214,7 @@
    1.56  by (Blast_tac 1);
    1.57  qed_spec_mp "not_free_iff_lifted";
    1.58  
    1.59 -Goal "(!s u. (~free s 0) --> R(Abs(s @ Var 0))(s[u/0])) = \
    1.60 -\     (!s. R(Abs(lift s 0 @ Var 0))(s))";
    1.61 +Goal "(!s u. (~free s 0) --> R(Abs(s $ Var 0))(s[u/0])) = \
    1.62 +\     (!s. R(Abs(lift s 0 $ Var 0))(s))";
    1.63  by (fast_tac (HOL_cs addss (simpset() addsimps [not_free_iff_lifted])) 1);
    1.64  qed "explicit_is_implicit";
     2.1 --- a/src/HOL/Lambda/Eta.thy	Wed Jul 15 11:15:57 1998 +0200
     2.2 +++ b/src/HOL/Lambda/Eta.thy	Wed Jul 15 12:02:19 1998 +0200
     2.3 @@ -21,14 +21,14 @@
     2.4  
     2.5  primrec free Lambda.dB
     2.6    "free (Var j) i = (j=i)"
     2.7 -  "free (s @ t) i = (free s i | free t i)"
     2.8 +  "free (s $ t) i = (free s i | free t i)"
     2.9    "free (Abs s) i = free s (Suc i)"
    2.10  
    2.11  inductive eta
    2.12  intrs
    2.13 -   eta  "~free s 0 ==> Abs(s @ Var 0) -e> s[dummy/0]"
    2.14 -   appL  "s -e> t ==> s@u -e> t@u"
    2.15 -   appR  "s -e> t ==> u@s -e> u@t"
    2.16 +   eta  "~free s 0 ==> Abs(s $ Var 0) -e> s[dummy/0]"
    2.17 +   appL  "s -e> t ==> s$u -e> t$u"
    2.18 +   appR  "s -e> t ==> u$s -e> u$t"
    2.19     abs   "s -e> t ==> Abs s -e> Abs t"
    2.20  end
    2.21  
     3.1 --- a/src/HOL/Lambda/Lambda.ML	Wed Jul 15 11:15:57 1998 +0200
     3.2 +++ b/src/HOL/Lambda/Lambda.ML	Wed Jul 15 12:02:19 1998 +0200
     3.3 @@ -27,17 +27,17 @@
     3.4  qed "rtrancl_beta_Abs";
     3.5  AddSIs [rtrancl_beta_Abs];
     3.6  
     3.7 -Goal "s ->> s' ==> s @ t ->> s' @ t";
     3.8 +Goal "s ->> s' ==> s $ t ->> s' $ t";
     3.9  by (etac rtrancl_induct 1);
    3.10  by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
    3.11  qed "rtrancl_beta_AppL";
    3.12  
    3.13 -Goal "t ->> t' ==> s @ t ->> s @ t'";
    3.14 +Goal "t ->> t' ==> s $ t ->> s $ t'";
    3.15  by (etac rtrancl_induct 1);
    3.16  by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
    3.17  qed "rtrancl_beta_AppR";
    3.18  
    3.19 -Goal "[| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
    3.20 +Goal "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'";
    3.21  by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
    3.22                         addIs  [rtrancl_trans]) 1);
    3.23  qed "rtrancl_beta_App";
     4.1 --- a/src/HOL/Lambda/Lambda.thy	Wed Jul 15 11:15:57 1998 +0200
     4.2 +++ b/src/HOL/Lambda/Lambda.thy	Wed Jul 15 12:02:19 1998 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  Lambda = Arith + Inductive +
     4.6  
     4.7 -datatype dB = Var nat | "@" dB dB (infixl 200) | Abs dB
     4.8 +datatype dB = Var nat | "$" dB dB (infixl 200) | Abs dB
     4.9  
    4.10  consts
    4.11    subst  :: [dB,dB,nat]=>dB ("_[_'/_]" [300,0,0] 300)
    4.12 @@ -20,24 +20,24 @@
    4.13  
    4.14  primrec lift dB
    4.15    "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
    4.16 -  "lift (s @ t) k = (lift s k) @ (lift t k)"
    4.17 +  "lift (s $ t) k = (lift s k) $ (lift t k)"
    4.18    "lift (Abs s) k = Abs(lift s (Suc k))"
    4.19  
    4.20  primrec subst dB
    4.21    subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
    4.22                              else if i = k then s else Var i)"
    4.23 -  subst_App "(t @ u)[s/k] = t[s/k] @ u[s/k]"
    4.24 +  subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]"
    4.25    subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
    4.26  
    4.27  primrec liftn dB
    4.28    "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
    4.29 -  "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)"
    4.30 +  "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)"
    4.31    "liftn n (Abs s) k = Abs(liftn n s (Suc k))"
    4.32  
    4.33  primrec substn dB
    4.34    "substn (Var i) s k = (if k < i then Var(i-1)
    4.35                           else if i = k then liftn k s 0 else Var i)"
    4.36 -  "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
    4.37 +  "substn (t $ u) s k = (substn t s k) $ (substn u s k)"
    4.38    "substn (Abs t) s k = Abs (substn t s (Suc k))"
    4.39  
    4.40  consts  beta :: "(dB * dB) set"
    4.41 @@ -50,8 +50,8 @@
    4.42  
    4.43  inductive beta
    4.44  intrs
    4.45 -   beta  "(Abs s) @ t -> s[t/0]"
    4.46 -   appL  "s -> t ==> s@u -> t@u"
    4.47 -   appR  "s -> t ==> u@s -> u@t"
    4.48 +   beta  "(Abs s) $ t -> s[t/0]"
    4.49 +   appL  "s -> t ==> s$u -> t$u"
    4.50 +   appR  "s -> t ==> u$s -> u$t"
    4.51     abs   "s -> t ==> Abs s -> Abs t"
    4.52  end
     5.1 --- a/src/HOL/Lambda/ParRed.ML	Wed Jul 15 11:15:57 1998 +0200
     5.2 +++ b/src/HOL/Lambda/ParRed.ML	Wed Jul 15 12:02:19 1998 +0200
     5.3 @@ -13,7 +13,7 @@
     5.4  
     5.5  val par_beta_cases = map (par_beta.mk_cases dB.simps)
     5.6      ["Var n => t", "Abs s => Abs t",
     5.7 -     "(Abs s) @ t => u", "s @ t => u", "Abs s => t"];
     5.8 +     "(Abs s) $ t => u", "s $ t => u", "Abs s => t"];
     5.9  
    5.10  AddSIs par_beta.intrs;
    5.11  AddSEs par_beta_cases;
     6.1 --- a/src/HOL/Lambda/ParRed.thy	Wed Jul 15 11:15:57 1998 +0200
     6.2 +++ b/src/HOL/Lambda/ParRed.thy	Wed Jul 15 12:02:19 1998 +0200
     6.3 @@ -19,26 +19,16 @@
     6.4    intrs
     6.5      var   "Var n => Var n"
     6.6      abs   "s => t ==> Abs s => Abs t"
     6.7 -    app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
     6.8 -    beta  "[| s => s'; t => t' |] ==> (Abs s) @ t => s'[t'/0]"
     6.9 +    app   "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
    6.10 +    beta  "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
    6.11  
    6.12  consts
    6.13    cd  :: dB => dB
    6.14  
    6.15  recdef cd "measure size"
    6.16    "cd(Var n) = Var n"
    6.17 -  "cd(Var n @ t) = Var n @ cd t"
    6.18 -  "cd((s1 @ s2) @ t) = cd(s1 @ s2) @ cd t"
    6.19 -  "cd(Abs u @ t) = (cd u)[cd t/0]"
    6.20 -(*
    6.21 -  "cd(s @ t) = (case s of Var n   => (s @ cd t)
    6.22 -                        | s1 @ s2 => (cd s @ cd t) 
    6.23 -                        | Abs u   => deAbs(cd s)[cd t/0])"
    6.24 -*)
    6.25 +  "cd(Var n     $ t) = Var n $ cd t"
    6.26 +  "cd((s1 $ s2) $ t) = cd(s1 $ s2) $ cd t"
    6.27 +  "cd(Abs u     $ t) = (cd u)[cd t/0]"
    6.28    "cd(Abs s) = Abs(cd s)"
    6.29 -(*
    6.30 -primrec deAbs dB
    6.31 -  "deAbs(Var n) = Var n"
    6.32 -  "deAbs(s @ t) = s @ t"
    6.33 -  "deAbs(Abs s) = s"*)
    6.34  end