author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 44890 | 22f665a2e91c |
child 57442 | 2373b4c61111 |
permissions | -rw-r--r-- |
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
36862
diff
changeset
|
1 |
(* Title: HOL/Proofs/Lambda/ParRed.thy |
1120 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 1995 TU Muenchen |
|
4 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
5 |
Properties of => and "cd", in particular the diamond property of => and |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
6 |
confluence of beta. |
1120 | 7 |
*) |
8 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
9 |
header {* Parallel reduction and a complete developments *} |
1120 | 10 |
|
16417 | 11 |
theory ParRed imports Lambda Commutation begin |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
12 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
13 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
14 |
subsection {* Parallel reduction *} |
1120 | 15 |
|
23750 | 16 |
inductive par_beta :: "[dB, dB] => bool" (infixl "=>" 50) |
22271 | 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]" |
|
1120 | 22 |
|
23750 | 23 |
inductive_cases par_beta_cases [elim!]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
24 |
"Var n => t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
25 |
"Abs s => Abs t" |
12011 | 26 |
"(Abs s) \<degree> t => u" |
27 |
"s \<degree> t => u" |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
28 |
"Abs s => t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
29 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
30 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
31 |
subsection {* Inclusions *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
32 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
33 |
text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
34 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
35 |
lemma par_beta_varL [simp]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
36 |
"(Var n => t) = (t = Var n)" |
18241 | 37 |
by blast |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
38 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
39 |
lemma par_beta_refl [simp]: "t => t" (* par_beta_refl [intro!] causes search to blow up *) |
18241 | 40 |
by (induct t) simp_all |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
41 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
42 |
lemma beta_subset_par_beta: "beta <= par_beta" |
22271 | 43 |
apply (rule predicate2I) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
44 |
apply (erule beta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
45 |
apply (blast intro!: par_beta_refl)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
46 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
47 |
|
22271 | 48 |
lemma par_beta_subset_beta: "par_beta <= beta^**" |
49 |
apply (rule predicate2I) |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
50 |
apply (erule par_beta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
51 |
apply blast |
23750 | 52 |
apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+ |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
53 |
-- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
54 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
55 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
56 |
|
25972 | 57 |
subsection {* Misc properties of @{text "par_beta"} *} |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
58 |
|
18241 | 59 |
lemma par_beta_lift [simp]: |
60 |
"t => t' \<Longrightarrow> lift t n => lift t' n" |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
39157
diff
changeset
|
61 |
by (induct t arbitrary: t' n) fastforce+ |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
62 |
|
18241 | 63 |
lemma par_beta_subst: |
64 |
"s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]" |
|
20503 | 65 |
apply (induct t arbitrary: s s' t' n) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
66 |
apply (simp add: subst_Var) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
67 |
apply (erule par_beta_cases) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
68 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
69 |
apply (simp add: subst_subst [symmetric]) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
39157
diff
changeset
|
70 |
apply (fastforce intro!: par_beta_lift) |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
39157
diff
changeset
|
71 |
apply fastforce |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
72 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
73 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
74 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
75 |
subsection {* Confluence (directly) *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
76 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
77 |
lemma diamond_par_beta: "diamond par_beta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
78 |
apply (unfold diamond_def commute_def square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
79 |
apply (rule impI [THEN allI [THEN allI]]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
80 |
apply (erule par_beta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
81 |
apply (blast intro!: par_beta_subst)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
82 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
83 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
84 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
85 |
subsection {* Complete developments *} |
1120 | 86 |
|
35440 | 87 |
fun |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
88 |
"cd" :: "dB => dB" |
35440 | 89 |
where |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
90 |
"cd (Var n) = Var n" |
35440 | 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)" |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
95 |
|
18241 | 96 |
lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s" |
20503 | 97 |
apply (induct s arbitrary: t rule: cd.induct) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
98 |
apply auto |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
99 |
apply (fast intro!: par_beta_subst) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
100 |
done |
1120 | 101 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
102 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
103 |
subsection {* Confluence (via complete developments) *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
104 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
105 |
lemma diamond_par_beta2: "diamond par_beta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
106 |
apply (unfold diamond_def commute_def square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
107 |
apply (blast intro: par_beta_cd) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
108 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
109 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
110 |
theorem beta_confluent: "confluent beta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
111 |
apply (rule diamond_par_beta2 diamond_to_confluence |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
112 |
par_beta_subset_beta beta_subset_par_beta)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
113 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
114 |
|
11638 | 115 |
end |