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";