src/HOL/Lambda/ParRed.thy
changeset 9811 39ffdb8cab03
parent 8624 69619f870939
child 9906 5c027cca6262
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Sat Sep 02 21:53:03 2000 +0200
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Sat Sep 02 21:56:24 2000 +0200
     1.3 @@ -3,32 +3,131 @@
     1.4      Author:     Tobias Nipkow
     1.5      Copyright   1995 TU Muenchen
     1.6  
     1.7 -Parallel reduction and a complete developments function "cd".
     1.8 +Properties of => and "cd", in particular the diamond property of => and
     1.9 +confluence of beta.
    1.10  *)
    1.11  
    1.12 -ParRed = Lambda + Commutation +
    1.13 +header {* Parallel reduction and a complete developments *}
    1.14  
    1.15 -consts  par_beta :: "(dB * dB) set"
    1.16 +theory ParRed = Lambda + Commutation:
    1.17 +
    1.18 +
    1.19 +subsection {* Parallel reduction *}
    1.20  
    1.21 -syntax  "=>" :: [dB,dB] => bool (infixl 50)
    1.22 +consts
    1.23 +  par_beta :: "(dB \<times> dB) set"
    1.24  
    1.25 +syntax
    1.26 +  par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
    1.27  translations
    1.28 -  "s => t" == "(s,t) : par_beta"
    1.29 +  "s => t" == "(s, t) \<in> par_beta"
    1.30  
    1.31  inductive par_beta
    1.32 -  intrs
    1.33 -    var   "Var n => Var n"
    1.34 -    abs   "s => t ==> Abs s => Abs t"
    1.35 -    app   "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
    1.36 -    beta  "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
    1.37 +  intros [simp, intro!]
    1.38 +    var: "Var n => Var n"
    1.39 +    abs: "s => t ==> Abs s => Abs t"
    1.40 +    app: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
    1.41 +    beta: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
    1.42 +
    1.43 +inductive_cases par_beta_cases [elim!]:
    1.44 +  "Var n => t"
    1.45 +  "Abs s => Abs t"
    1.46 +  "(Abs s) $ t => u"
    1.47 +  "s $ t => u"
    1.48 +  "Abs s => t"
    1.49 +
    1.50 +
    1.51 +subsection {* Inclusions *}
    1.52 +
    1.53 +text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *}
    1.54 +
    1.55 +lemma par_beta_varL [simp]:
    1.56 +    "(Var n => t) = (t = Var n)"
    1.57 +  apply blast
    1.58 +  done
    1.59 +
    1.60 +lemma par_beta_refl [simp]: "t => t"  (* par_beta_refl [intro!] causes search to blow up *)
    1.61 +  apply (induct_tac t)
    1.62 +    apply simp_all
    1.63 +  done
    1.64 +
    1.65 +lemma beta_subset_par_beta: "beta <= par_beta"
    1.66 +  apply (rule subsetI)
    1.67 +  apply clarify
    1.68 +  apply (erule beta.induct)
    1.69 +     apply (blast intro!: par_beta_refl)+
    1.70 +  done
    1.71 +
    1.72 +lemma par_beta_subset_beta: "par_beta <= beta^*"
    1.73 +  apply (rule subsetI)
    1.74 +  apply clarify
    1.75 +  apply (erule par_beta.induct)
    1.76 +     apply blast
    1.77 +    apply (blast del: rtrancl_refl intro: rtrancl_into_rtrancl)+
    1.78 +      -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
    1.79 +  done
    1.80 +
    1.81 +
    1.82 +subsection {* Misc properties of par-beta *}
    1.83 +
    1.84 +lemma par_beta_lift [rulify, simp]:
    1.85 +    "\<forall>t' n. t => t' --> lift t n => lift t' n"
    1.86 +  apply (induct_tac t)
    1.87 +    apply fastsimp+
    1.88 +  done
    1.89 +
    1.90 +lemma par_beta_subst [rulify]:
    1.91 +    "\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
    1.92 +  apply (induct_tac t)
    1.93 +    apply (simp add: subst_Var)
    1.94 +   apply (intro strip)
    1.95 +   apply (erule par_beta_cases)
    1.96 +    apply simp
    1.97 +   apply (simp add: subst_subst [symmetric])
    1.98 +   apply (fastsimp intro!: par_beta_lift)
    1.99 +  apply fastsimp
   1.100 +  done
   1.101 +
   1.102 +
   1.103 +subsection {* Confluence (directly) *}
   1.104 +
   1.105 +lemma diamond_par_beta: "diamond par_beta"
   1.106 +  apply (unfold diamond_def commute_def square_def)
   1.107 +  apply (rule impI [THEN allI [THEN allI]])
   1.108 +  apply (erule par_beta.induct)
   1.109 +     apply (blast intro!: par_beta_subst)+
   1.110 +  done
   1.111 +
   1.112 +
   1.113 +subsection {* Complete developments *}
   1.114  
   1.115  consts
   1.116 -  cd  :: dB => dB
   1.117 +  "cd" :: "dB => dB"
   1.118 +recdef "cd" "measure size"
   1.119 +  "cd (Var n) = Var n"
   1.120 +  "cd (Var n $ t) = Var n $ cd t"
   1.121 +  "cd ((s1 $ s2) $ t) = cd (s1 $ s2) $ cd t"
   1.122 +  "cd (Abs u $ t) = (cd u)[cd t/0]"
   1.123 +  "cd (Abs s) = Abs (cd s)"
   1.124 +
   1.125 +lemma par_beta_cd [rulify]:
   1.126 +    "\<forall>t. s => t --> t => cd s"
   1.127 +  apply (induct_tac s rule: cd.induct)
   1.128 +      apply auto
   1.129 +  apply (fast intro!: par_beta_subst)
   1.130 +  done
   1.131  
   1.132 -recdef cd "measure size"
   1.133 -  "cd(Var n) = Var n"
   1.134 -  "cd(Var n     $ t) = Var n $ cd t"
   1.135 -  "cd((s1 $ s2) $ t) = cd(s1 $ s2) $ cd t"
   1.136 -  "cd(Abs u     $ t) = (cd u)[cd t/0]"
   1.137 -  "cd(Abs s) = Abs(cd s)"
   1.138 -end
   1.139 +
   1.140 +subsection {* Confluence (via complete developments) *}
   1.141 +
   1.142 +lemma diamond_par_beta2: "diamond par_beta"
   1.143 +  apply (unfold diamond_def commute_def square_def)
   1.144 +  apply (blast intro: par_beta_cd)
   1.145 +  done
   1.146 +
   1.147 +theorem beta_confluent: "confluent beta"
   1.148 +  apply (rule diamond_par_beta2 diamond_to_confluence
   1.149 +    par_beta_subset_beta beta_subset_par_beta)+
   1.150 +  done
   1.151 +
   1.152 +end
   1.153 \ No newline at end of file