1(* Title: HOL/Proofs/Lambda/ParRed.thy 2 Author: Tobias Nipkow 3 Copyright 1995 TU Muenchen 4 5Properties of => and "cd", in particular the diamond property of => and 6confluence of beta. 7*) 8 9section \<open>Parallel reduction and a complete developments\<close> 10 11theory ParRed imports Lambda Commutation begin 12 13 14subsection \<open>Parallel reduction\<close> 15 16inductive par_beta :: "[dB, dB] => bool" (infixl "=>" 50) 17 where 18 var [simp, intro!]: "Var n => Var n" 19 | abs [simp, intro!]: "s => t ==> Abs s => Abs t" 20 | app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'" 21 | beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]" 22 23inductive_cases par_beta_cases [elim!]: 24 "Var n => t" 25 "Abs s => Abs t" 26 "(Abs s) \<degree> t => u" 27 "s \<degree> t => u" 28 "Abs s => t" 29 30 31subsection \<open>Inclusions\<close> 32 33text \<open>\<open>beta \<subseteq> par_beta \<subseteq> beta\<^sup>*\<close> \medskip\<close> 34 35lemma par_beta_varL [simp]: 36 "(Var n => t) = (t = Var n)" 37 by blast 38 39lemma par_beta_refl [simp]: "t => t" (* par_beta_refl [intro!] causes search to blow up *) 40 by (induct t) simp_all 41 42lemma beta_subset_par_beta: "beta <= par_beta" 43 apply (rule predicate2I) 44 apply (erule beta.induct) 45 apply (blast intro!: par_beta_refl)+ 46 done 47 48lemma par_beta_subset_beta: "par_beta \<le> beta\<^sup>*\<^sup>*" 49 apply (rule predicate2I) 50 apply (erule par_beta.induct) 51 apply blast 52 apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+ 53 \<comment> \<open>@{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor\<close> 54 done 55 56 57subsection \<open>Misc properties of \<open>par_beta\<close>\<close> 58 59lemma par_beta_lift [simp]: 60 "t => t' \<Longrightarrow> lift t n => lift t' n" 61 by (induct t arbitrary: t' n) fastforce+ 62 63lemma par_beta_subst: 64 "s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]" 65 apply (induct t arbitrary: s s' t' n) 66 apply (simp add: subst_Var) 67 apply (erule par_beta_cases) 68 apply simp 69 apply (simp add: subst_subst [symmetric]) 70 apply (fastforce intro!: par_beta_lift) 71 apply fastforce 72 done 73 74 75subsection \<open>Confluence (directly)\<close> 76 77lemma diamond_par_beta: "diamond par_beta" 78 apply (unfold diamond_def commute_def square_def) 79 apply (rule impI [THEN allI [THEN allI]]) 80 apply (erule par_beta.induct) 81 apply (blast intro!: par_beta_subst)+ 82 done 83 84 85subsection \<open>Complete developments\<close> 86 87fun 88 cd :: "dB => dB" 89where 90 "cd (Var n) = Var n" 91| "cd (Var n \<degree> t) = Var n \<degree> cd t" 92| "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t" 93| "cd (Abs u \<degree> t) = (cd u)[cd t/0]" 94| "cd (Abs s) = Abs (cd s)" 95 96lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s" 97 apply (induct s arbitrary: t rule: cd.induct) 98 apply auto 99 apply (fast intro!: par_beta_subst) 100 done 101 102 103subsection \<open>Confluence (via complete developments)\<close> 104 105lemma diamond_par_beta2: "diamond par_beta" 106 apply (unfold diamond_def commute_def square_def) 107 apply (blast intro: par_beta_cd) 108 done 109 110theorem beta_confluent: "confluent beta" 111 apply (rule diamond_par_beta2 diamond_to_confluence 112 par_beta_subset_beta beta_subset_par_beta)+ 113 done 114 115end 116