# HG changeset patch
# User nipkow
# Date 800365608 -7200
# Node ID ff7dd80513e693e9253ae01d4529aed6e31e51a2
# Parent  49ed9a4156374c4ba4a013d1f88c7323815391dc
Lambda calculus in de Bruijn notation.
Proof of confluence.

diff -r 49ed9a415637 -r ff7dd80513e6 src/HOL/Lambda/Confluence.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/Confluence.ML	Sat May 13 13:46:48 1995 +0200
@@ -0,0 +1,25 @@
+(*  Title:      HOL/Lambda/Confluence.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1995 TU Muenchen
+
+Basic confluence lemmas.
+*)
+
+open Confluence;
+
+goalw Confluence.thy [confluent_def,confluent1_def,diamondP_def]
+  "!!R. confluent1(R) ==> diamondP(R^*)";
+by(strip_tac 1);
+be rtrancl_induct 1;
+by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rtrancl_comp])));
+qed "confluent1";
+
+goalw Confluence.thy [confluent_def]
+  "!!R.[| diamondP(R); T <= R; R <= T^* |] ==> confluent(T)";
+bd rtrancl_mono 1;
+bd rtrancl_mono 1;
+by(fast_tac (HOL_cs addIs [diamondP_confluent1,confluent1]
+                    addDs [subset_antisym]
+                    addss (HOL_ss addsimps [rtrancl_idemp])) 1);
+qed "diamond_to_confluence";
diff -r 49ed9a415637 -r ff7dd80513e6 src/HOL/Lambda/Confluence.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/Confluence.thy	Sat May 13 13:46:48 1995 +0200
@@ -0,0 +1,27 @@
+(*  Title: 	HOL/Lambda/Confluence.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1995  TU Muenchen
+
+Abstract confluence notions.
+*)
+
+Confluence = Trancl +
+
+consts
+  confluent, confluent1, diamondP :: "('a*'a)set => bool"
+
+defs
+  diamondP_def
+  "diamondP(R) ==   \
+\  !x y. (x,y):R --> (!z. (x,z):R --> (EX u. (y,u):R & (z,u):R))" 
+
+  confluent_def "confluent(R) == diamondP(R^*)"
+
+  confluent1_def
+  "confluent1(R) ==
+   !x y. (x,y):R --> (!z. (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R^*))"
+
+rules
+  diamondP_confluent1 "diamondP R ==> confluent1(R)"
+end
diff -r 49ed9a415637 -r ff7dd80513e6 src/HOL/Lambda/Lambda.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/Lambda.ML	Sat May 13 13:46:48 1995 +0200
@@ -0,0 +1,182 @@
+(*  Title:      HOL/Lambda.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1995 TU Muenchen
+
+Substitution-lemmas.  Most of the proofs, esp. those about natural numbers,
+are ported from Ole Rasmussen's ZF development.  In ZF, m<=n is syntactic
+sugar for m<Suc(n). In HOL <= is a separate operator. Hence we have to prove
+some compatibility lemmas.
+
+*)
+
+(*** Nat ***)
+
+goal Nat.thy "!!i. [| i < Suc j; j < k |] ==> i < k";
+br le_less_trans 1;
+ba 2;
+by(asm_full_simp_tac (nat_ss addsimps [le_def]) 1);
+by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1);
+qed "lt_trans1";
+
+goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k";
+be less_le_trans 1;
+by(asm_full_simp_tac (nat_ss addsimps [le_def]) 1);
+by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1);
+qed "lt_trans2";
+
+val major::prems = goal Nat.thy
+  "[| i < Suc j; i < j ==> P; i = j ==> P |] ==> P";
+br (major RS lessE) 1;
+by(ALLGOALS(asm_full_simp_tac nat_ss));
+by(resolve_tac prems 1 THEN etac sym 1);
+by(fast_tac (HOL_cs addIs prems) 1);
+qed "leqE";
+
+goal Arith.thy "!!i. i < j ==> Suc(pred j) = j";
+by(fast_tac (HOL_cs addEs [lessE] addss arith_ss) 1);
+qed "Suc_pred";
+
+goal Arith.thy "!!i. Suc i < j ==> i < pred j ";
+by (resolve_tac [Suc_less_SucD] 1);
+by (asm_simp_tac (arith_ss addsimps [Suc_pred]) 1);
+qed "lt_pred";
+
+goal Arith.thy "!!i. [| i < Suc j; k < i |] ==> pred i < j ";
+by (resolve_tac [Suc_less_SucD] 1);
+by (asm_simp_tac (arith_ss addsimps [Suc_pred]) 1);
+qed "gt_pred";
+
+(*** Lambda ***)
+
+open Lambda;
+
+val lambda_ss = arith_ss delsimps [less_Suc_eq] addsimps
+  db.simps @ beta.intrs @
+  [if_not_P, not_less_eq,
+   subst_App,subst_Fun,
+   lift_Var,lift_App,lift_Fun];
+
+val lambda_cs = HOL_cs addSIs beta.intrs;
+
+(*** Congruence rules for ->> ***)
+
+goal Lambda.thy "!!s. s ->> s' ==> Fun s ->> Fun s'";
+be rtrancl_induct 1;
+by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+qed "rtrancl_beta_Fun";
+
+goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
+be rtrancl_induct 1;
+by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+qed "rtrancl_beta_AppL";
+
+goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'";
+be rtrancl_induct 1;
+by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+qed "rtrancl_beta_AppR";
+
+goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
+by (fast_tac (lambda_cs addIs
+                [rtrancl_beta_AppL,rtrancl_beta_AppR,rtrancl_comp]) 1);
+qed "rtrancl_beta_App";
+
+(*** subst and lift ***)
+
+fun addsplit ss = ss addsimps [subst_Var] setloop (split_tac [expand_if]);
+
+goal Lambda.thy "subst u (Var n) n = u";
+by (asm_full_simp_tac (addsplit lambda_ss) 1);
+qed "subst_eq";
+
+goal Lambda.thy "!!s. m<n ==> subst u (Var n) m = Var(pred n)";
+by (asm_full_simp_tac (addsplit lambda_ss) 1);
+qed "subst_gt";
+
+goal Lambda.thy "!!s. n<m ==> subst u (Var n) m = Var(n)";
+by (asm_full_simp_tac (addsplit lambda_ss addsimps
+                          [less_not_refl2 RS not_sym,less_SucI]) 1);
+qed "subst_lt";
+
+val lambda_ss = lambda_ss addsimps [subst_eq,subst_gt,subst_lt];
+
+goal Lambda.thy
+  "!n i. i < Suc n --> lift (lift s i) (Suc n) = lift (lift s n) i";
+by(db.induct_tac "s" 1);
+by(ALLGOALS(asm_simp_tac lambda_ss));
+by(strip_tac 1);
+by (excluded_middle_tac "nat < i" 1);
+by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
+by (ALLGOALS(asm_full_simp_tac ((addsplit lambda_ss) addsimps [less_SucI])));
+qed"lift_lift";
+
+goal Lambda.thy "!m n s. n < Suc m --> \
+\         lift (subst s t n) m = subst (lift s m) (lift t (Suc m)) n";
+by(db.induct_tac "t" 1);
+by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift])));
+by(strip_tac 1);
+by (excluded_middle_tac "nat < n" 1);
+by (asm_full_simp_tac lambda_ss 1);
+by (eres_inst_tac [("j","nat")] leqE 1);
+by (asm_full_simp_tac ((addsplit lambda_ss) 
+                        addsimps [less_SucI,gt_pred,Suc_pred]) 1);
+by (hyp_subst_tac 1);
+by (asm_simp_tac lambda_ss 1);
+by (forw_inst_tac [("j","n")] lt_trans2 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (addsplit lambda_ss addsimps [less_SucI]) 1);
+qed "lift_subst";
+val lambda_ss = lambda_ss addsimps [lift_subst];
+
+goal Lambda.thy
+  "!n m u. m < Suc n -->\
+\         lift (subst u v n) m = subst (lift u m) (lift v m) (Suc n)";
+by(db.induct_tac "v" 1);
+by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift])));
+by(strip_tac 1);
+by (excluded_middle_tac "nat < n" 1);
+by (asm_full_simp_tac lambda_ss 1);
+by (eres_inst_tac [("i","n")] leqE 1);
+by (forward_tac  [lt_trans1] 1 THEN assume_tac 1);
+by (ALLGOALS(asm_full_simp_tac 
+	     (lambda_ss addsimps [Suc_pred,less_SucI,gt_pred])));
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1);
+by(split_tac [expand_if] 1);
+by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1);
+qed "lift_subst_lt";
+
+goal Lambda.thy "!n v. subst v (lift u n) n = u";
+by(db.induct_tac "u" 1);
+by(ALLGOALS(asm_simp_tac lambda_ss));
+by(split_tac [expand_if] 1);
+by(ALLGOALS(asm_full_simp_tac lambda_ss));
+qed "subst_lift";
+val lambda_ss = lambda_ss addsimps [subst_lift];
+
+
+goal Lambda.thy "!m n u w. m < Suc n --> \
+\ subst (subst w u n) (subst (lift w m) v (Suc n)) m = \
+\ subst w (subst u v m) n";
+by(db.induct_tac "v" 1);
+by (ALLGOALS(asm_simp_tac (lambda_ss addsimps
+                   [lift_lift RS spec RS spec RS mp RS sym,lift_subst_lt])));
+by(strip_tac 1);
+by (excluded_middle_tac "nat < Suc(Suc n)" 1);
+by(asm_full_simp_tac lambda_ss 1);
+by (forward_tac [lessI RS less_trans] 1);
+by (eresolve_tac [leqE] 1);
+by (asm_simp_tac (lambda_ss addsimps [Suc_pred,lt_pred]) 2);
+by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1);
+by (forw_inst_tac [("i","m")] (lessI RS less_trans) 1);
+by (asm_simp_tac (lambda_ss addsimps [Suc_pred,lt_pred]) 1);
+by (eres_inst_tac [("i","nat")] leqE 1);
+by (asm_full_simp_tac (lambda_ss addsimps [Suc_pred,less_SucI]) 2);
+by (excluded_middle_tac "nat < m" 1);
+by (asm_full_simp_tac lambda_ss 1);
+by (eres_inst_tac [("j","nat")] leqE 1);
+by (asm_simp_tac (lambda_ss addsimps [gt_pred]) 1);
+by (asm_simp_tac lambda_ss 1);
+by (forward_tac [lt_trans2] 1 THEN assume_tac 1);
+by (asm_simp_tac (lambda_ss addsimps [gt_pred]) 1);
+bind_thm("subst_subst", result() RS spec RS spec RS spec RS spec RS mp);
diff -r 49ed9a415637 -r ff7dd80513e6 src/HOL/Lambda/Lambda.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/Lambda.thy	Sat May 13 13:46:48 1995 +0200
@@ -0,0 +1,43 @@
+(*  Title:      HOL/Lambda.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1995 TU Muenchen
+
+Lambda-terms in de Bruijn notation,
+substitution and beta-reduction.
+*)
+
+Lambda = Arith +
+
+datatype db = Var nat | "@" db db (infixl 200) | Fun db
+
+consts
+  subst  :: "[db,db,nat]=>db"
+  lift   :: "[db,nat] => db"
+
+primrec subst db
+  subst_Var "subst s (Var i) n = (if n < i then Var(pred i)
+                                  else if i = n then s else Var i)"
+  subst_App "subst s (t @ u) n = (subst s t n) @ (subst s u n)"
+  subst_Fun "subst s (Fun t) n = Fun (subst (lift s 0) t (Suc n))"
+
+primrec lift db
+  lift_Var "lift (Var i) n = (if i < n then Var i else Var(Suc i))"
+  lift_App "lift (s @ t) n = (lift s n) @ (lift t n)"
+  lift_Fun "lift (Fun s) n = Fun(lift s (Suc n))"
+
+consts  beta :: "(db * db) set"
+
+syntax  "->", "->>" :: "[db,db] => bool" (infixl 50)
+
+translations
+  "s -> t"  == "(s,t) : beta"
+  "s ->> t" == "(s,t) : beta^*"
+
+inductive "beta"
+intrs
+   beta  "(Fun s) @ t -> subst t s 0"
+   appL  "s -> t ==> s@u -> t@u"
+   appR  "s -> t ==> u@s -> u@t"
+   abs   "s -> t ==> Fun s -> Fun t"
+end
diff -r 49ed9a415637 -r ff7dd80513e6 src/HOL/Lambda/ParRed.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ParRed.ML	Sat May 13 13:46:48 1995 +0200
@@ -0,0 +1,107 @@
+(*  Title:      HOL/Lambda/ParRed.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1995 TU Muenchen
+
+Properties of => and cd, in particular the diamond property of => and
+confluence of beta.
+*)
+
+open ParRed;
+
+val parred_ss = lambda_ss addsimps
+  par_beta.intrs @ [cd_Var,cd_Fun];
+
+val par_beta_cases = map (par_beta.mk_cases db.simps)
+    ["Var n => t", "Fun s => Fun t",
+     "(Fun s) @ t => u", "s @ t => u", "Fun s => t"];
+
+val parred_cs = lambda_cs addSIs par_beta.intrs addSEs par_beta_cases;
+
+(*** beta <= par_beta <= beta^* ***)
+
+goal ParRed.thy "(Var n => t) = (t = Var n)";
+by(fast_tac parred_cs 1);
+qed "par_beta_varL";
+val parred_ss = parred_ss addsimps [par_beta_varL];
+
+goal ParRed.thy "t => t";
+by(db.induct_tac "t" 1);
+by(ALLGOALS(asm_simp_tac parred_ss));
+qed"par_beta_refl";
+val parred_ss = parred_ss addsimps [par_beta_refl];
+
+goal ParRed.thy "beta <= par_beta";
+br subsetI 1;
+by (res_inst_tac[("p","x")]PairE 1);
+by (hyp_subst_tac 1);
+be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
+by (ALLGOALS(fast_tac (parred_cs addSIs [par_beta_refl])));
+qed "beta_subset_par_beta";
+
+goal ParRed.thy "par_beta <= beta^*";
+br subsetI 1;
+by (res_inst_tac[("p","x")]PairE 1);
+by (hyp_subst_tac 1);
+be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
+by (ALLGOALS(fast_tac (parred_cs addIs
+       [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl,
+        rtrancl_into_rtrancl] addEs [rtrancl_comp])));
+qed "par_beta_subset_beta";
+
+(*** cd ***)
+
+goal ParRed.thy "cd(Var n @ t) = Var n @ cd t";
+by(simp_tac (parred_ss addsimps [cd_App]) 1);
+qed"cd_App_Var";
+
+goal ParRed.thy "cd((r @ s) @ t) = cd(r @ s) @ cd t";
+by(simp_tac (parred_ss addsimps [cd_App]) 1);
+qed"cd_App_App";
+
+goal ParRed.thy "cd((Fun s) @ t) = subst (cd t) (cd s) 0";
+by(simp_tac (parred_ss addsimps [cd_App,deFun_Fun]) 1);
+qed"cd_App_Fun";
+
+val parred_ss = parred_ss addsimps [cd_App_Var,cd_App_App,cd_App_Fun];
+
+(*** => ***)
+
+goal ParRed.thy "!s' n. s => s' --> lift s n => lift s' n";
+by(db.induct_tac "s" 1);
+by(ALLGOALS(fast_tac (parred_cs addss parred_ss)));
+bind_thm("par_beta_lift", result() RS spec RS spec RS mp);
+val parred_ss = parred_ss addsimps [par_beta_lift];
+
+goal ParRed.thy
+  "!s s' t' n. s => s' --> t => t' --> subst s t n => subst s' t' n";
+by(db.induct_tac "t" 1);
+  by(asm_simp_tac (addsplit parred_ss) 1);
+ by(strip_tac 1);
+ bes par_beta_cases 1;
+  by(asm_simp_tac parred_ss 1);
+ by(asm_simp_tac parred_ss 1);
+ br (zero_less_Suc RS subst_subst RS subst) 1;
+ by(fast_tac (parred_cs addSIs [par_beta_lift] addss parred_ss) 1);
+by(fast_tac (parred_cs addss parred_ss) 1);
+bind_thm("par_beta_subst",
+         result()  RS spec RS spec RS spec RS spec RS mp RS mp);
+
+goal ParRed.thy "!t. s => t --> t => cd s";
+by(db.induct_tac "s" 1);
+  by(simp_tac parred_ss 1);
+ be rev_mp 1;
+ by(db.induct_tac "db1" 1);
+ by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss parred_ss)));
+bind_thm("par_beta_cd", result() RS spec RS mp);
+
+(*** Confluence ***)
+
+goalw ParRed.thy [diamondP_def] "diamondP par_beta";
+by(fast_tac (HOL_cs addIs [par_beta_cd]) 1);
+qed "diamondP_par_beta";
+
+goal ParRed.thy "confluent(beta)";
+by(fast_tac (HOL_cs addIs [diamondP_par_beta,diamond_to_confluence,
+                           par_beta_subset_beta,beta_subset_par_beta]) 1);
+qed"beta_confluent";
diff -r 49ed9a415637 -r ff7dd80513e6 src/HOL/Lambda/ParRed.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ParRed.thy	Sat May 13 13:46:48 1995 +0200
@@ -0,0 +1,41 @@
+(*  Title:      HOL/Lambda/ParRed.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1995 TU Muenchen
+
+Parallel reduction and a complete developments function "cd".
+*)
+
+ParRed = Lambda + Confluence +
+
+consts  par_beta :: "(db * db) set"
+
+syntax  "=>" :: "[db,db] => bool" (infixl 50)
+
+translations
+  "s => t" == "(s,t) : par_beta"
+
+inductive "par_beta"
+  intrs
+    var   "Var n => Var n"
+    abs   "s => t ==> Fun s => Fun t"
+    app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
+    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => subst t' s' 0"
+
+consts
+  cd  :: "db => db"
+  deFun :: "db => db"
+
+primrec cd db
+  cd_Var "cd(Var n) = Var n"
+  cd_App "cd(s @ t) = (case s of
+            Var n => s @ (cd t) |
+            s1 @ s2 => (cd s) @ (cd t) |
+            Fun u => subst (cd t) (deFun(cd s)) 0)"
+  cd_Fun "cd(Fun s) = Fun(cd s)"
+
+primrec deFun db
+  deFun_Var "deFun(Var n) = Var n"
+  deFun_App "deFun(s @ t) = s @ t"
+  deFun_Fun "deFun(Fun s) = s"
+end