author | wenzelm |
Sat, 02 Sep 2000 21:56:24 +0200 | |
changeset 9811 | 39ffdb8cab03 |
parent 8624 | 69619f870939 |
child 9906 | 5c027cca6262 |
permissions | -rw-r--r-- |
1120 | 1 |
(* Title: HOL/Lambda/ParRed.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
6 |
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
|
7 |
confluence of beta. |
1120 | 8 |
*) |
9 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
10 |
header {* Parallel reduction and a complete developments *} |
1120 | 11 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
12 |
theory ParRed = Lambda + Commutation: |
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 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
15 |
subsection {* Parallel reduction *} |
1120 | 16 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
17 |
consts |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
18 |
par_beta :: "(dB \<times> dB) set" |
1120 | 19 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
20 |
syntax |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
21 |
par_beta :: "[dB, dB] => bool" (infixl "=>" 50) |
1120 | 22 |
translations |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
23 |
"s => t" == "(s, t) \<in> par_beta" |
1120 | 24 |
|
1789 | 25 |
inductive par_beta |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
26 |
intros [simp, intro!] |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
27 |
var: "Var n => Var n" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
28 |
abs: "s => t ==> Abs s => Abs t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
29 |
app: "[| s => s'; t => t' |] ==> s $ t => s' $ t'" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
30 |
beta: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
31 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
32 |
inductive_cases par_beta_cases [elim!]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
33 |
"Var n => t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
34 |
"Abs s => Abs t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
35 |
"(Abs s) $ t => u" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
36 |
"s $ t => u" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
37 |
"Abs s => t" |
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 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
40 |
subsection {* Inclusions *} |
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 |
text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
43 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
44 |
lemma par_beta_varL [simp]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
45 |
"(Var n => t) = (t = Var n)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
46 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
47 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
48 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
49 |
lemma par_beta_refl [simp]: "t => t" (* par_beta_refl [intro!] causes search to blow up *) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
50 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
51 |
apply simp_all |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
52 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
53 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
54 |
lemma beta_subset_par_beta: "beta <= par_beta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
55 |
apply (rule subsetI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
56 |
apply clarify |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
57 |
apply (erule beta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
58 |
apply (blast intro!: par_beta_refl)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
59 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
60 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
61 |
lemma par_beta_subset_beta: "par_beta <= beta^*" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
62 |
apply (rule subsetI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
63 |
apply clarify |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
64 |
apply (erule par_beta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
65 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
66 |
apply (blast del: rtrancl_refl intro: rtrancl_into_rtrancl)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
67 |
-- {* @{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
|
68 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
69 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
70 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
71 |
subsection {* Misc properties of par-beta *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
72 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
73 |
lemma par_beta_lift [rulify, simp]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
74 |
"\<forall>t' n. t => t' --> lift t n => lift t' n" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
75 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
76 |
apply fastsimp+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
77 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
78 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
79 |
lemma par_beta_subst [rulify]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
80 |
"\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
81 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
82 |
apply (simp add: subst_Var) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
83 |
apply (intro strip) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
84 |
apply (erule par_beta_cases) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
85 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
86 |
apply (simp add: subst_subst [symmetric]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
87 |
apply (fastsimp intro!: par_beta_lift) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
88 |
apply fastsimp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
89 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
90 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
91 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
92 |
subsection {* Confluence (directly) *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
93 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
94 |
lemma diamond_par_beta: "diamond par_beta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
95 |
apply (unfold diamond_def commute_def square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
96 |
apply (rule impI [THEN allI [THEN allI]]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
97 |
apply (erule par_beta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
98 |
apply (blast intro!: par_beta_subst)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
99 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
100 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
101 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
102 |
subsection {* Complete developments *} |
1120 | 103 |
|
104 |
consts |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
105 |
"cd" :: "dB => dB" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
106 |
recdef "cd" "measure size" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
107 |
"cd (Var n) = Var n" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
108 |
"cd (Var n $ t) = Var n $ cd t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
109 |
"cd ((s1 $ s2) $ t) = cd (s1 $ s2) $ cd t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
110 |
"cd (Abs u $ t) = (cd u)[cd t/0]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
111 |
"cd (Abs s) = Abs (cd s)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
112 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
113 |
lemma par_beta_cd [rulify]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
114 |
"\<forall>t. s => t --> t => cd s" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
115 |
apply (induct_tac s rule: cd.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
116 |
apply auto |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
117 |
apply (fast intro!: par_beta_subst) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
118 |
done |
1120 | 119 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
120 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
121 |
subsection {* Confluence (via complete developments) *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
122 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
123 |
lemma diamond_par_beta2: "diamond par_beta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
124 |
apply (unfold diamond_def commute_def square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
125 |
apply (blast intro: par_beta_cd) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
126 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
127 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
128 |
theorem beta_confluent: "confluent beta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
129 |
apply (rule diamond_par_beta2 diamond_to_confluence |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
130 |
par_beta_subset_beta beta_subset_par_beta)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
131 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
132 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
133 |
end |