Polished the presentation making it completely definitional.
authornipkow
Mon May 22 14:12:40 1995 +0200 (1995-05-22)
changeset 1124a6233ea105a4
parent 1123 5dfdc1464966
child 1125 13a3df2adbe5
Polished the presentation making it completely definitional.
src/HOL/Lambda/Confluence.ML
src/HOL/Lambda/Confluence.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/Confluence.ML	Thu May 18 11:51:23 1995 +0200
     1.2 +++ b/src/HOL/Lambda/Confluence.ML	Mon May 22 14:12:40 1995 +0200
     1.3 @@ -8,18 +8,32 @@
     1.4  
     1.5  open Confluence;
     1.6  
     1.7 -goalw Confluence.thy [confluent_def,confluent1_def,diamondP_def]
     1.8 -  "!!R. confluent1(R) ==> diamondP(R^*)";
     1.9 +goalw Confluence.thy [confluent1_def,diamond_def]
    1.10 +  "!!R. confluent1(R) ==> diamond(R^*)";
    1.11  by(strip_tac 1);
    1.12  be rtrancl_induct 1;
    1.13 -by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rtrancl_comp])));
    1.14 -qed "confluent1";
    1.15 +by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rtrancl_trans])));
    1.16 +qed "confluent1_diamond";
    1.17 +
    1.18 +goalw Confluence.thy [confluent1_def,confluent2_def]
    1.19 +  "!!R. confluent2(R) ==> confluent1(R)";
    1.20 +by(fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
    1.21 +qed "confluent2_confluent1";
    1.22 +
    1.23 +goalw Confluence.thy [confluent2_def,diamond_def]
    1.24 +  "!!R. diamond(R) ==> confluent2(R)";
    1.25 +by(strip_tac 1);
    1.26 +be rtrancl_induct 1;
    1.27 +by(fast_tac (HOL_cs addSIs [rtrancl_refl]) 1);
    1.28 +by(fast_tac (HOL_cs addSEs [rtrancl_into_rtrancl]) 1);
    1.29 +qed "diamond_confluent2";
    1.30  
    1.31  goalw Confluence.thy [confluent_def]
    1.32 -  "!!R.[| diamondP(R); T <= R; R <= T^* |] ==> confluent(T)";
    1.33 +  "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
    1.34  bd rtrancl_mono 1;
    1.35  bd rtrancl_mono 1;
    1.36 -by(fast_tac (HOL_cs addIs [diamondP_confluent1,confluent1]
    1.37 +by(fast_tac (HOL_cs addIs [diamond_confluent2, confluent2_confluent1,
    1.38 +                           confluent1_diamond]
    1.39                      addDs [subset_antisym]
    1.40                      addss (HOL_ss addsimps [rtrancl_idemp])) 1);
    1.41  qed "diamond_to_confluence";
     2.1 --- a/src/HOL/Lambda/Confluence.thy	Thu May 18 11:51:23 1995 +0200
     2.2 +++ b/src/HOL/Lambda/Confluence.thy	Mon May 22 14:12:40 1995 +0200
     2.3 @@ -9,19 +9,20 @@
     2.4  Confluence = Trancl +
     2.5  
     2.6  consts
     2.7 -  confluent, confluent1, diamondP :: "('a*'a)set => bool"
     2.8 +  confluent, confluent1, confluent2, diamond :: "('a*'a)set => bool"
     2.9  
    2.10  defs
    2.11 -  diamondP_def
    2.12 -  "diamondP(R) ==   \
    2.13 -\  !x y. (x,y):R --> (!z. (x,z):R --> (EX u. (y,u):R & (z,u):R))" 
    2.14 +  diamond_def
    2.15 +  "diamond(R) == !x y z. (x,y):R --> (x,z):R --> (EX u. (y,u):R & (z,u):R)" 
    2.16  
    2.17 -  confluent_def "confluent(R) == diamondP(R^*)"
    2.18 +  confluent_def "confluent(R) == diamond(R^*)"
    2.19  
    2.20    confluent1_def
    2.21    "confluent1(R) ==
    2.22 -   !x y. (x,y):R --> (!z. (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R^*))"
    2.23 +   !x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R^*)"
    2.24  
    2.25 -rules
    2.26 -  diamondP_confluent1 "diamondP R ==> confluent1(R)"
    2.27 +  confluent2_def
    2.28 +  "confluent2(R) ==
    2.29 +   !x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R)"
    2.30 +
    2.31  end
     3.1 --- a/src/HOL/Lambda/Lambda.ML	Thu May 18 11:51:23 1995 +0200
     3.2 +++ b/src/HOL/Lambda/Lambda.ML	Mon May 22 14:12:40 1995 +0200
     3.3 @@ -78,22 +78,22 @@
     3.4  
     3.5  goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
     3.6  by (fast_tac (lambda_cs addIs
     3.7 -                [rtrancl_beta_AppL,rtrancl_beta_AppR,rtrancl_comp]) 1);
     3.8 +                [rtrancl_beta_AppL,rtrancl_beta_AppR,rtrancl_trans]) 1);
     3.9  qed "rtrancl_beta_App";
    3.10  
    3.11  (*** subst and lift ***)
    3.12  
    3.13  fun addsplit ss = ss addsimps [subst_Var] setloop (split_tac [expand_if]);
    3.14  
    3.15 -goal Lambda.thy "subst u (Var n) n = u";
    3.16 +goal Lambda.thy "(Var n)[u/n] = u";
    3.17  by (asm_full_simp_tac (addsplit lambda_ss) 1);
    3.18  qed "subst_eq";
    3.19  
    3.20 -goal Lambda.thy "!!s. m<n ==> subst u (Var n) m = Var(pred n)";
    3.21 +goal Lambda.thy "!!s. m<n ==> (Var n)[u/m] = Var(pred n)";
    3.22  by (asm_full_simp_tac (addsplit lambda_ss) 1);
    3.23  qed "subst_gt";
    3.24  
    3.25 -goal Lambda.thy "!!s. n<m ==> subst u (Var n) m = Var(n)";
    3.26 +goal Lambda.thy "!!s. n<m ==> (Var n)[u/m] = Var(n)";
    3.27  by (asm_full_simp_tac (addsplit lambda_ss addsimps
    3.28                            [less_not_refl2 RS not_sym,less_SucI]) 1);
    3.29  qed "subst_lt";
    3.30 @@ -111,7 +111,7 @@
    3.31  qed"lift_lift";
    3.32  
    3.33  goal Lambda.thy "!m n s. n < Suc m --> \
    3.34 -\         lift (subst s t n) m = subst (lift s m) (lift t (Suc m)) n";
    3.35 +\         lift (t[s/n]) m = (lift t (Suc m)) [lift s m / n]";
    3.36  by(db.induct_tac "t" 1);
    3.37  by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift])));
    3.38  by(strip_tac 1);
    3.39 @@ -130,7 +130,7 @@
    3.40  
    3.41  goal Lambda.thy
    3.42    "!n m u. m < Suc n -->\
    3.43 -\         lift (subst u v n) m = subst (lift u m) (lift v m) (Suc n)";
    3.44 +\         lift (v[u/n]) m = (lift v m) [lift u m / Suc n]";
    3.45  by(db.induct_tac "v" 1);
    3.46  by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift])));
    3.47  by(strip_tac 1);
    3.48 @@ -146,7 +146,7 @@
    3.49  by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1);
    3.50  qed "lift_subst_lt";
    3.51  
    3.52 -goal Lambda.thy "!n v. subst v (lift u n) n = u";
    3.53 +goal Lambda.thy "!n v. (lift u n)[v/n] = u";
    3.54  by(db.induct_tac "u" 1);
    3.55  by(ALLGOALS(asm_simp_tac lambda_ss));
    3.56  by(split_tac [expand_if] 1);
    3.57 @@ -156,8 +156,7 @@
    3.58  
    3.59  
    3.60  goal Lambda.thy "!m n u w. m < Suc n --> \
    3.61 -\ subst (subst w u n) (subst (lift w m) v (Suc n)) m = \
    3.62 -\ subst w (subst u v m) n";
    3.63 +\ (v[lift w m / Suc n]) [u[w/n]/m] = (v[u/m])[w/n]";
    3.64  by(db.induct_tac "v" 1);
    3.65  by (ALLGOALS(asm_simp_tac (lambda_ss addsimps
    3.66                     [lift_lift RS spec RS spec RS mp RS sym,lift_subst_lt])));
     4.1 --- a/src/HOL/Lambda/Lambda.thy	Thu May 18 11:51:23 1995 +0200
     4.2 +++ b/src/HOL/Lambda/Lambda.thy	Mon May 22 14:12:40 1995 +0200
     4.3 @@ -12,14 +12,14 @@
     4.4  datatype db = Var nat | "@" db db (infixl 200) | Fun db
     4.5  
     4.6  consts
     4.7 -  subst  :: "[db,db,nat]=>db"
     4.8 +  subst  :: "[db,db,nat]=>db" ("_[_'/_]" [300,0,0] 300)
     4.9    lift   :: "[db,nat] => db"
    4.10  
    4.11  primrec subst db
    4.12 -  subst_Var "subst s (Var i) n = (if n < i then Var(pred i)
    4.13 -                                  else if i = n then s else Var i)"
    4.14 -  subst_App "subst s (t @ u) n = (subst s t n) @ (subst s u n)"
    4.15 -  subst_Fun "subst s (Fun t) n = Fun (subst (lift s 0) t (Suc n))"
    4.16 +  subst_Var "(Var i)[s/n] = (if n < i then Var(pred i)
    4.17 +                            else if i = n then s else Var i)"
    4.18 +  subst_App "(t @ u)[s/n] = t[s/n] @ u[s/n]"
    4.19 +  subst_Fun "(Fun t)[s/n] = Fun (t[lift s 0 / Suc n])"
    4.20  
    4.21  primrec lift db
    4.22    lift_Var "lift (Var i) n = (if i < n then Var i else Var(Suc i))"
    4.23 @@ -36,7 +36,7 @@
    4.24  
    4.25  inductive "beta"
    4.26  intrs
    4.27 -   beta  "(Fun s) @ t -> subst t s 0"
    4.28 +   beta  "(Fun s) @ t -> s[t/0]"
    4.29     appL  "s -> t ==> s@u -> t@u"
    4.30     appR  "s -> t ==> u@s -> u@t"
    4.31     abs   "s -> t ==> Fun s -> Fun t"
     5.1 --- a/src/HOL/Lambda/ParRed.ML	Thu May 18 11:51:23 1995 +0200
     5.2 +++ b/src/HOL/Lambda/ParRed.ML	Mon May 22 14:12:40 1995 +0200
     5.3 @@ -46,7 +46,7 @@
     5.4  be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
     5.5  by (ALLGOALS(fast_tac (parred_cs addIs
     5.6         [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl,
     5.7 -        rtrancl_into_rtrancl] addEs [rtrancl_comp])));
     5.8 +        rtrancl_into_rtrancl] addEs [rtrancl_trans])));
     5.9  qed "par_beta_subset_beta";
    5.10  
    5.11  (*** cd ***)
    5.12 @@ -59,7 +59,7 @@
    5.13  by(simp_tac (parred_ss addsimps [cd_App]) 1);
    5.14  qed"cd_App_App";
    5.15  
    5.16 -goal ParRed.thy "cd((Fun s) @ t) = subst (cd t) (cd s) 0";
    5.17 +goal ParRed.thy "cd((Fun s) @ t) = (cd s)[cd t/0]";
    5.18  by(simp_tac (parred_ss addsimps [cd_App,deFun_Fun]) 1);
    5.19  qed"cd_App_Fun";
    5.20  
    5.21 @@ -74,7 +74,7 @@
    5.22  val parred_ss = parred_ss addsimps [par_beta_lift];
    5.23  
    5.24  goal ParRed.thy
    5.25 -  "!s s' t' n. s => s' --> t => t' --> subst s t n => subst s' t' n";
    5.26 +  "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
    5.27  by(db.induct_tac "t" 1);
    5.28    by(asm_simp_tac (addsplit parred_ss) 1);
    5.29   by(strip_tac 1);
    5.30 @@ -97,11 +97,11 @@
    5.31  
    5.32  (*** Confluence ***)
    5.33  
    5.34 -goalw ParRed.thy [diamondP_def] "diamondP par_beta";
    5.35 +goalw ParRed.thy [diamond_def] "diamond(par_beta)";
    5.36  by(fast_tac (HOL_cs addIs [par_beta_cd]) 1);
    5.37 -qed "diamondP_par_beta";
    5.38 +qed "diamond_par_beta";
    5.39  
    5.40  goal ParRed.thy "confluent(beta)";
    5.41 -by(fast_tac (HOL_cs addIs [diamondP_par_beta,diamond_to_confluence,
    5.42 +by(fast_tac (HOL_cs addIs [diamond_par_beta,diamond_to_confluence,
    5.43                             par_beta_subset_beta,beta_subset_par_beta]) 1);
    5.44  qed"beta_confluent";
     6.1 --- a/src/HOL/Lambda/ParRed.thy	Thu May 18 11:51:23 1995 +0200
     6.2 +++ b/src/HOL/Lambda/ParRed.thy	Mon May 22 14:12:40 1995 +0200
     6.3 @@ -4,6 +4,11 @@
     6.4      Copyright   1995 TU Muenchen
     6.5  
     6.6  Parallel reduction and a complete developments function "cd".
     6.7 +Follows the first two pages of
     6.8 +
     6.9 +@article{Takahashi-IC-95,author="Masako Takahashi",
    6.10 +title="Parallel Reductions in $\lambda$-Calculus",
    6.11 +journal=IC,year=1995,volume=118,pages="120--127"}
    6.12  *)
    6.13  
    6.14  ParRed = Lambda + Confluence +
    6.15 @@ -20,7 +25,7 @@
    6.16      var   "Var n => Var n"
    6.17      abs   "s => t ==> Fun s => Fun t"
    6.18      app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
    6.19 -    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => subst t' s' 0"
    6.20 +    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
    6.21  
    6.22  consts
    6.23    cd  :: "db => db"
    6.24 @@ -31,7 +36,7 @@
    6.25    cd_App "cd(s @ t) = (case s of
    6.26              Var n => s @ (cd t) |
    6.27              s1 @ s2 => (cd s) @ (cd t) |
    6.28 -            Fun u => subst (cd t) (deFun(cd s)) 0)"
    6.29 +            Fun u => deFun(cd s)[cd t/0])"
    6.30    cd_Fun "cd(Fun s) = Fun(cd s)"
    6.31  
    6.32  primrec deFun db