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