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.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
```