author nipkow Sat May 13 13:46:48 1995 +0200 (1995-05-13) changeset 1120 ff7dd80513e6 parent 1119 49ed9a415637 child 1121 485b49694253
Lambda calculus in de Bruijn notation.
Proof of confluence.
 src/HOL/Lambda/Confluence.ML file | annotate | diff | revisions src/HOL/Lambda/Confluence.thy file | annotate | diff | revisions src/HOL/Lambda/Lambda.ML file | annotate | diff | revisions src/HOL/Lambda/Lambda.thy file | annotate | diff | revisions src/HOL/Lambda/ParRed.ML file | annotate | diff | revisions src/HOL/Lambda/ParRed.thy file | annotate | diff | revisions
```     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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.51 +       [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl,
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.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.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.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.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
```