Lambda calculus in de Bruijn notation.
authornipkow
Sat May 13 13:46:48 1995 +0200 (1995-05-13)
changeset 1120ff7dd80513e6
parent 1119 49ed9a415637
child 1121 485b49694253
Lambda calculus in de Bruijn notation.
Proof of confluence.
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 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Lambda/Confluence.ML	Sat May 13 13:46:48 1995 +0200
     1.3 @@ -0,0 +1,25 @@
     1.4 +(*  Title:      HOL/Lambda/Confluence.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   1995 TU Muenchen
     1.8 +
     1.9 +Basic confluence lemmas.
    1.10 +*)
    1.11 +
    1.12 +open Confluence;
    1.13 +
    1.14 +goalw Confluence.thy [confluent_def,confluent1_def,diamondP_def]
    1.15 +  "!!R. confluent1(R) ==> diamondP(R^*)";
    1.16 +by(strip_tac 1);
    1.17 +be rtrancl_induct 1;
    1.18 +by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rtrancl_comp])));
    1.19 +qed "confluent1";
    1.20 +
    1.21 +goalw Confluence.thy [confluent_def]
    1.22 +  "!!R.[| diamondP(R); T <= R; R <= T^* |] ==> confluent(T)";
    1.23 +bd rtrancl_mono 1;
    1.24 +bd rtrancl_mono 1;
    1.25 +by(fast_tac (HOL_cs addIs [diamondP_confluent1,confluent1]
    1.26 +                    addDs [subset_antisym]
    1.27 +                    addss (HOL_ss addsimps [rtrancl_idemp])) 1);
    1.28 +qed "diamond_to_confluence";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Lambda/Confluence.thy	Sat May 13 13:46:48 1995 +0200
     2.3 @@ -0,0 +1,27 @@
     2.4 +(*  Title: 	HOL/Lambda/Confluence.thy
     2.5 +    ID:         $Id$
     2.6 +    Author: 	Tobias Nipkow
     2.7 +    Copyright   1995  TU Muenchen
     2.8 +
     2.9 +Abstract confluence notions.
    2.10 +*)
    2.11 +
    2.12 +Confluence = Trancl +
    2.13 +
    2.14 +consts
    2.15 +  confluent, confluent1, diamondP :: "('a*'a)set => bool"
    2.16 +
    2.17 +defs
    2.18 +  diamondP_def
    2.19 +  "diamondP(R) ==   \
    2.20 +\  !x y. (x,y):R --> (!z. (x,z):R --> (EX u. (y,u):R & (z,u):R))" 
    2.21 +
    2.22 +  confluent_def "confluent(R) == diamondP(R^*)"
    2.23 +
    2.24 +  confluent1_def
    2.25 +  "confluent1(R) ==
    2.26 +   !x y. (x,y):R --> (!z. (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R^*))"
    2.27 +
    2.28 +rules
    2.29 +  diamondP_confluent1 "diamondP R ==> confluent1(R)"
    2.30 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Lambda/Lambda.ML	Sat May 13 13:46:48 1995 +0200
     3.3 @@ -0,0 +1,182 @@
     3.4 +(*  Title:      HOL/Lambda.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow
     3.7 +    Copyright   1995 TU Muenchen
     3.8 +
     3.9 +Substitution-lemmas.  Most of the proofs, esp. those about natural numbers,
    3.10 +are ported from Ole Rasmussen's ZF development.  In ZF, m<=n is syntactic
    3.11 +sugar for m<Suc(n). In HOL <= is a separate operator. Hence we have to prove
    3.12 +some compatibility lemmas.
    3.13 +
    3.14 +*)
    3.15 +
    3.16 +(*** Nat ***)
    3.17 +
    3.18 +goal Nat.thy "!!i. [| i < Suc j; j < k |] ==> i < k";
    3.19 +br le_less_trans 1;
    3.20 +ba 2;
    3.21 +by(asm_full_simp_tac (nat_ss addsimps [le_def]) 1);
    3.22 +by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1);
    3.23 +qed "lt_trans1";
    3.24 +
    3.25 +goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k";
    3.26 +be less_le_trans 1;
    3.27 +by(asm_full_simp_tac (nat_ss addsimps [le_def]) 1);
    3.28 +by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1);
    3.29 +qed "lt_trans2";
    3.30 +
    3.31 +val major::prems = goal Nat.thy
    3.32 +  "[| i < Suc j; i < j ==> P; i = j ==> P |] ==> P";
    3.33 +br (major RS lessE) 1;
    3.34 +by(ALLGOALS(asm_full_simp_tac nat_ss));
    3.35 +by(resolve_tac prems 1 THEN etac sym 1);
    3.36 +by(fast_tac (HOL_cs addIs prems) 1);
    3.37 +qed "leqE";
    3.38 +
    3.39 +goal Arith.thy "!!i. i < j ==> Suc(pred j) = j";
    3.40 +by(fast_tac (HOL_cs addEs [lessE] addss arith_ss) 1);
    3.41 +qed "Suc_pred";
    3.42 +
    3.43 +goal Arith.thy "!!i. Suc i < j ==> i < pred j ";
    3.44 +by (resolve_tac [Suc_less_SucD] 1);
    3.45 +by (asm_simp_tac (arith_ss addsimps [Suc_pred]) 1);
    3.46 +qed "lt_pred";
    3.47 +
    3.48 +goal Arith.thy "!!i. [| i < Suc j; k < i |] ==> pred i < j ";
    3.49 +by (resolve_tac [Suc_less_SucD] 1);
    3.50 +by (asm_simp_tac (arith_ss addsimps [Suc_pred]) 1);
    3.51 +qed "gt_pred";
    3.52 +
    3.53 +(*** Lambda ***)
    3.54 +
    3.55 +open Lambda;
    3.56 +
    3.57 +val lambda_ss = arith_ss delsimps [less_Suc_eq] addsimps
    3.58 +  db.simps @ beta.intrs @
    3.59 +  [if_not_P, not_less_eq,
    3.60 +   subst_App,subst_Fun,
    3.61 +   lift_Var,lift_App,lift_Fun];
    3.62 +
    3.63 +val lambda_cs = HOL_cs addSIs beta.intrs;
    3.64 +
    3.65 +(*** Congruence rules for ->> ***)
    3.66 +
    3.67 +goal Lambda.thy "!!s. s ->> s' ==> Fun s ->> Fun s'";
    3.68 +be rtrancl_induct 1;
    3.69 +by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    3.70 +qed "rtrancl_beta_Fun";
    3.71 +
    3.72 +goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
    3.73 +be rtrancl_induct 1;
    3.74 +by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    3.75 +qed "rtrancl_beta_AppL";
    3.76 +
    3.77 +goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'";
    3.78 +be rtrancl_induct 1;
    3.79 +by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    3.80 +qed "rtrancl_beta_AppR";
    3.81 +
    3.82 +goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
    3.83 +by (fast_tac (lambda_cs addIs
    3.84 +                [rtrancl_beta_AppL,rtrancl_beta_AppR,rtrancl_comp]) 1);
    3.85 +qed "rtrancl_beta_App";
    3.86 +
    3.87 +(*** subst and lift ***)
    3.88 +
    3.89 +fun addsplit ss = ss addsimps [subst_Var] setloop (split_tac [expand_if]);
    3.90 +
    3.91 +goal Lambda.thy "subst u (Var n) n = u";
    3.92 +by (asm_full_simp_tac (addsplit lambda_ss) 1);
    3.93 +qed "subst_eq";
    3.94 +
    3.95 +goal Lambda.thy "!!s. m<n ==> subst u (Var n) m = Var(pred n)";
    3.96 +by (asm_full_simp_tac (addsplit lambda_ss) 1);
    3.97 +qed "subst_gt";
    3.98 +
    3.99 +goal Lambda.thy "!!s. n<m ==> subst u (Var n) m = Var(n)";
   3.100 +by (asm_full_simp_tac (addsplit lambda_ss addsimps
   3.101 +                          [less_not_refl2 RS not_sym,less_SucI]) 1);
   3.102 +qed "subst_lt";
   3.103 +
   3.104 +val lambda_ss = lambda_ss addsimps [subst_eq,subst_gt,subst_lt];
   3.105 +
   3.106 +goal Lambda.thy
   3.107 +  "!n i. i < Suc n --> lift (lift s i) (Suc n) = lift (lift s n) i";
   3.108 +by(db.induct_tac "s" 1);
   3.109 +by(ALLGOALS(asm_simp_tac lambda_ss));
   3.110 +by(strip_tac 1);
   3.111 +by (excluded_middle_tac "nat < i" 1);
   3.112 +by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
   3.113 +by (ALLGOALS(asm_full_simp_tac ((addsplit lambda_ss) addsimps [less_SucI])));
   3.114 +qed"lift_lift";
   3.115 +
   3.116 +goal Lambda.thy "!m n s. n < Suc m --> \
   3.117 +\         lift (subst s t n) m = subst (lift s m) (lift t (Suc m)) n";
   3.118 +by(db.induct_tac "t" 1);
   3.119 +by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift])));
   3.120 +by(strip_tac 1);
   3.121 +by (excluded_middle_tac "nat < n" 1);
   3.122 +by (asm_full_simp_tac lambda_ss 1);
   3.123 +by (eres_inst_tac [("j","nat")] leqE 1);
   3.124 +by (asm_full_simp_tac ((addsplit lambda_ss) 
   3.125 +                        addsimps [less_SucI,gt_pred,Suc_pred]) 1);
   3.126 +by (hyp_subst_tac 1);
   3.127 +by (asm_simp_tac lambda_ss 1);
   3.128 +by (forw_inst_tac [("j","n")] lt_trans2 1);
   3.129 +by (assume_tac 1);
   3.130 +by (asm_full_simp_tac (addsplit lambda_ss addsimps [less_SucI]) 1);
   3.131 +qed "lift_subst";
   3.132 +val lambda_ss = lambda_ss addsimps [lift_subst];
   3.133 +
   3.134 +goal Lambda.thy
   3.135 +  "!n m u. m < Suc n -->\
   3.136 +\         lift (subst u v n) m = subst (lift u m) (lift v m) (Suc n)";
   3.137 +by(db.induct_tac "v" 1);
   3.138 +by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift])));
   3.139 +by(strip_tac 1);
   3.140 +by (excluded_middle_tac "nat < n" 1);
   3.141 +by (asm_full_simp_tac lambda_ss 1);
   3.142 +by (eres_inst_tac [("i","n")] leqE 1);
   3.143 +by (forward_tac  [lt_trans1] 1 THEN assume_tac 1);
   3.144 +by (ALLGOALS(asm_full_simp_tac 
   3.145 +	     (lambda_ss addsimps [Suc_pred,less_SucI,gt_pred])));
   3.146 +by (hyp_subst_tac 1);
   3.147 +by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1);
   3.148 +by(split_tac [expand_if] 1);
   3.149 +by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1);
   3.150 +qed "lift_subst_lt";
   3.151 +
   3.152 +goal Lambda.thy "!n v. subst v (lift u n) n = u";
   3.153 +by(db.induct_tac "u" 1);
   3.154 +by(ALLGOALS(asm_simp_tac lambda_ss));
   3.155 +by(split_tac [expand_if] 1);
   3.156 +by(ALLGOALS(asm_full_simp_tac lambda_ss));
   3.157 +qed "subst_lift";
   3.158 +val lambda_ss = lambda_ss addsimps [subst_lift];
   3.159 +
   3.160 +
   3.161 +goal Lambda.thy "!m n u w. m < Suc n --> \
   3.162 +\ subst (subst w u n) (subst (lift w m) v (Suc n)) m = \
   3.163 +\ subst w (subst u v m) n";
   3.164 +by(db.induct_tac "v" 1);
   3.165 +by (ALLGOALS(asm_simp_tac (lambda_ss addsimps
   3.166 +                   [lift_lift RS spec RS spec RS mp RS sym,lift_subst_lt])));
   3.167 +by(strip_tac 1);
   3.168 +by (excluded_middle_tac "nat < Suc(Suc n)" 1);
   3.169 +by(asm_full_simp_tac lambda_ss 1);
   3.170 +by (forward_tac [lessI RS less_trans] 1);
   3.171 +by (eresolve_tac [leqE] 1);
   3.172 +by (asm_simp_tac (lambda_ss addsimps [Suc_pred,lt_pred]) 2);
   3.173 +by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1);
   3.174 +by (forw_inst_tac [("i","m")] (lessI RS less_trans) 1);
   3.175 +by (asm_simp_tac (lambda_ss addsimps [Suc_pred,lt_pred]) 1);
   3.176 +by (eres_inst_tac [("i","nat")] leqE 1);
   3.177 +by (asm_full_simp_tac (lambda_ss addsimps [Suc_pred,less_SucI]) 2);
   3.178 +by (excluded_middle_tac "nat < m" 1);
   3.179 +by (asm_full_simp_tac lambda_ss 1);
   3.180 +by (eres_inst_tac [("j","nat")] leqE 1);
   3.181 +by (asm_simp_tac (lambda_ss addsimps [gt_pred]) 1);
   3.182 +by (asm_simp_tac lambda_ss 1);
   3.183 +by (forward_tac [lt_trans2] 1 THEN assume_tac 1);
   3.184 +by (asm_simp_tac (lambda_ss addsimps [gt_pred]) 1);
   3.185 +bind_thm("subst_subst", result() RS spec RS spec RS spec RS spec RS mp);
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Lambda/Lambda.thy	Sat May 13 13:46:48 1995 +0200
     4.3 @@ -0,0 +1,43 @@
     4.4 +(*  Title:      HOL/Lambda.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Nipkow
     4.7 +    Copyright   1995 TU Muenchen
     4.8 +
     4.9 +Lambda-terms in de Bruijn notation,
    4.10 +substitution and beta-reduction.
    4.11 +*)
    4.12 +
    4.13 +Lambda = Arith +
    4.14 +
    4.15 +datatype db = Var nat | "@" db db (infixl 200) | Fun db
    4.16 +
    4.17 +consts
    4.18 +  subst  :: "[db,db,nat]=>db"
    4.19 +  lift   :: "[db,nat] => db"
    4.20 +
    4.21 +primrec subst db
    4.22 +  subst_Var "subst s (Var i) n = (if n < i then Var(pred i)
    4.23 +                                  else if i = n then s else Var i)"
    4.24 +  subst_App "subst s (t @ u) n = (subst s t n) @ (subst s u n)"
    4.25 +  subst_Fun "subst s (Fun t) n = Fun (subst (lift s 0) t (Suc n))"
    4.26 +
    4.27 +primrec lift db
    4.28 +  lift_Var "lift (Var i) n = (if i < n then Var i else Var(Suc i))"
    4.29 +  lift_App "lift (s @ t) n = (lift s n) @ (lift t n)"
    4.30 +  lift_Fun "lift (Fun s) n = Fun(lift s (Suc n))"
    4.31 +
    4.32 +consts  beta :: "(db * db) set"
    4.33 +
    4.34 +syntax  "->", "->>" :: "[db,db] => bool" (infixl 50)
    4.35 +
    4.36 +translations
    4.37 +  "s -> t"  == "(s,t) : beta"
    4.38 +  "s ->> t" == "(s,t) : beta^*"
    4.39 +
    4.40 +inductive "beta"
    4.41 +intrs
    4.42 +   beta  "(Fun s) @ t -> subst t s 0"
    4.43 +   appL  "s -> t ==> s@u -> t@u"
    4.44 +   appR  "s -> t ==> u@s -> u@t"
    4.45 +   abs   "s -> t ==> Fun s -> Fun t"
    4.46 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Lambda/ParRed.ML	Sat May 13 13:46:48 1995 +0200
     5.3 @@ -0,0 +1,107 @@
     5.4 +(*  Title:      HOL/Lambda/ParRed.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Tobias Nipkow
     5.7 +    Copyright   1995 TU Muenchen
     5.8 +
     5.9 +Properties of => and cd, in particular the diamond property of => and
    5.10 +confluence of beta.
    5.11 +*)
    5.12 +
    5.13 +open ParRed;
    5.14 +
    5.15 +val parred_ss = lambda_ss addsimps
    5.16 +  par_beta.intrs @ [cd_Var,cd_Fun];
    5.17 +
    5.18 +val par_beta_cases = map (par_beta.mk_cases db.simps)
    5.19 +    ["Var n => t", "Fun s => Fun t",
    5.20 +     "(Fun s) @ t => u", "s @ t => u", "Fun s => t"];
    5.21 +
    5.22 +val parred_cs = lambda_cs addSIs par_beta.intrs addSEs par_beta_cases;
    5.23 +
    5.24 +(*** beta <= par_beta <= beta^* ***)
    5.25 +
    5.26 +goal ParRed.thy "(Var n => t) = (t = Var n)";
    5.27 +by(fast_tac parred_cs 1);
    5.28 +qed "par_beta_varL";
    5.29 +val parred_ss = parred_ss addsimps [par_beta_varL];
    5.30 +
    5.31 +goal ParRed.thy "t => t";
    5.32 +by(db.induct_tac "t" 1);
    5.33 +by(ALLGOALS(asm_simp_tac parred_ss));
    5.34 +qed"par_beta_refl";
    5.35 +val parred_ss = parred_ss addsimps [par_beta_refl];
    5.36 +
    5.37 +goal ParRed.thy "beta <= par_beta";
    5.38 +br subsetI 1;
    5.39 +by (res_inst_tac[("p","x")]PairE 1);
    5.40 +by (hyp_subst_tac 1);
    5.41 +be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
    5.42 +by (ALLGOALS(fast_tac (parred_cs addSIs [par_beta_refl])));
    5.43 +qed "beta_subset_par_beta";
    5.44 +
    5.45 +goal ParRed.thy "par_beta <= beta^*";
    5.46 +br subsetI 1;
    5.47 +by (res_inst_tac[("p","x")]PairE 1);
    5.48 +by (hyp_subst_tac 1);
    5.49 +be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
    5.50 +by (ALLGOALS(fast_tac (parred_cs addIs
    5.51 +       [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl,
    5.52 +        rtrancl_into_rtrancl] addEs [rtrancl_comp])));
    5.53 +qed "par_beta_subset_beta";
    5.54 +
    5.55 +(*** cd ***)
    5.56 +
    5.57 +goal ParRed.thy "cd(Var n @ t) = Var n @ cd t";
    5.58 +by(simp_tac (parred_ss addsimps [cd_App]) 1);
    5.59 +qed"cd_App_Var";
    5.60 +
    5.61 +goal ParRed.thy "cd((r @ s) @ t) = cd(r @ s) @ cd t";
    5.62 +by(simp_tac (parred_ss addsimps [cd_App]) 1);
    5.63 +qed"cd_App_App";
    5.64 +
    5.65 +goal ParRed.thy "cd((Fun s) @ t) = subst (cd t) (cd s) 0";
    5.66 +by(simp_tac (parred_ss addsimps [cd_App,deFun_Fun]) 1);
    5.67 +qed"cd_App_Fun";
    5.68 +
    5.69 +val parred_ss = parred_ss addsimps [cd_App_Var,cd_App_App,cd_App_Fun];
    5.70 +
    5.71 +(*** => ***)
    5.72 +
    5.73 +goal ParRed.thy "!s' n. s => s' --> lift s n => lift s' n";
    5.74 +by(db.induct_tac "s" 1);
    5.75 +by(ALLGOALS(fast_tac (parred_cs addss parred_ss)));
    5.76 +bind_thm("par_beta_lift", result() RS spec RS spec RS mp);
    5.77 +val parred_ss = parred_ss addsimps [par_beta_lift];
    5.78 +
    5.79 +goal ParRed.thy
    5.80 +  "!s s' t' n. s => s' --> t => t' --> subst s t n => subst s' t' n";
    5.81 +by(db.induct_tac "t" 1);
    5.82 +  by(asm_simp_tac (addsplit parred_ss) 1);
    5.83 + by(strip_tac 1);
    5.84 + bes par_beta_cases 1;
    5.85 +  by(asm_simp_tac parred_ss 1);
    5.86 + by(asm_simp_tac parred_ss 1);
    5.87 + br (zero_less_Suc RS subst_subst RS subst) 1;
    5.88 + by(fast_tac (parred_cs addSIs [par_beta_lift] addss parred_ss) 1);
    5.89 +by(fast_tac (parred_cs addss parred_ss) 1);
    5.90 +bind_thm("par_beta_subst",
    5.91 +         result()  RS spec RS spec RS spec RS spec RS mp RS mp);
    5.92 +
    5.93 +goal ParRed.thy "!t. s => t --> t => cd s";
    5.94 +by(db.induct_tac "s" 1);
    5.95 +  by(simp_tac parred_ss 1);
    5.96 + be rev_mp 1;
    5.97 + by(db.induct_tac "db1" 1);
    5.98 + by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss parred_ss)));
    5.99 +bind_thm("par_beta_cd", result() RS spec RS mp);
   5.100 +
   5.101 +(*** Confluence ***)
   5.102 +
   5.103 +goalw ParRed.thy [diamondP_def] "diamondP par_beta";
   5.104 +by(fast_tac (HOL_cs addIs [par_beta_cd]) 1);
   5.105 +qed "diamondP_par_beta";
   5.106 +
   5.107 +goal ParRed.thy "confluent(beta)";
   5.108 +by(fast_tac (HOL_cs addIs [diamondP_par_beta,diamond_to_confluence,
   5.109 +                           par_beta_subset_beta,beta_subset_par_beta]) 1);
   5.110 +qed"beta_confluent";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Lambda/ParRed.thy	Sat May 13 13:46:48 1995 +0200
     6.3 @@ -0,0 +1,41 @@
     6.4 +(*  Title:      HOL/Lambda/ParRed.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Tobias Nipkow
     6.7 +    Copyright   1995 TU Muenchen
     6.8 +
     6.9 +Parallel reduction and a complete developments function "cd".
    6.10 +*)
    6.11 +
    6.12 +ParRed = Lambda + Confluence +
    6.13 +
    6.14 +consts  par_beta :: "(db * db) set"
    6.15 +
    6.16 +syntax  "=>" :: "[db,db] => bool" (infixl 50)
    6.17 +
    6.18 +translations
    6.19 +  "s => t" == "(s,t) : par_beta"
    6.20 +
    6.21 +inductive "par_beta"
    6.22 +  intrs
    6.23 +    var   "Var n => Var n"
    6.24 +    abs   "s => t ==> Fun s => Fun t"
    6.25 +    app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
    6.26 +    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => subst t' s' 0"
    6.27 +
    6.28 +consts
    6.29 +  cd  :: "db => db"
    6.30 +  deFun :: "db => db"
    6.31 +
    6.32 +primrec cd db
    6.33 +  cd_Var "cd(Var n) = Var n"
    6.34 +  cd_App "cd(s @ t) = (case s of
    6.35 +            Var n => s @ (cd t) |
    6.36 +            s1 @ s2 => (cd s) @ (cd t) |
    6.37 +            Fun u => subst (cd t) (deFun(cd s)) 0)"
    6.38 +  cd_Fun "cd(Fun s) = Fun(cd s)"
    6.39 +
    6.40 +primrec deFun db
    6.41 +  deFun_Var "deFun(Var n) = Var n"
    6.42 +  deFun_App "deFun(s @ t) = s @ t"
    6.43 +  deFun_Fun "deFun(Fun s) = s"
    6.44 +end