| author | kleing |
| Wed, 07 Jan 2004 07:52:12 +0100 | |
| changeset 14343 | 6bc647f472b9 |
| parent 13339 | 0f89104dd377 |
| child 16417 | 9bc16273c2d4 |
| permissions | -rw-r--r-- |
| 1478 | 1 |
(* Title: Confluence.thy |
| 1048 | 2 |
ID: $Id$ |
| 1478 | 3 |
Author: Ole Rasmussen |
| 1048 | 4 |
Copyright 1995 University of Cambridge |
5 |
Logic Image: ZF |
|
6 |
*) |
|
7 |
||
| 12593 | 8 |
theory Confluence = Reduction: |
9 |
||
10 |
constdefs |
|
11 |
confluence :: "i=>o" |
|
12 |
"confluence(R) == |
|
13 |
\<forall>x y. <x,y> \<in> R --> (\<forall>z.<x,z> \<in> R --> (\<exists>u.<y,u> \<in> R & <z,u> \<in> R))" |
|
14 |
||
15 |
strip :: "o" |
|
16 |
"strip == \<forall>x y. (x ===> y) --> |
|
17 |
(\<forall>z.(x =1=> z) --> (\<exists>u.(y =1=> u) & (z===>u)))" |
|
18 |
||
19 |
||
20 |
(* ------------------------------------------------------------------------- *) |
|
21 |
(* strip lemmas *) |
|
22 |
(* ------------------------------------------------------------------------- *) |
|
23 |
||
24 |
lemma strip_lemma_r: |
|
25 |
"[|confluence(Spar_red1)|]==> strip" |
|
26 |
apply (unfold confluence_def strip_def) |
|
27 |
apply (rule impI [THEN allI, THEN allI]) |
|
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
28 |
apply (erule Spar_red.induct, fast) |
| 12593 | 29 |
apply (fast intro: Spar_red.trans) |
30 |
done |
|
31 |
||
32 |
||
33 |
lemma strip_lemma_l: |
|
34 |
"strip==> confluence(Spar_red)" |
|
35 |
apply (unfold confluence_def strip_def) |
|
36 |
apply (rule impI [THEN allI, THEN allI]) |
|
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
37 |
apply (erule Spar_red.induct, blast) |
| 12593 | 38 |
apply clarify |
39 |
apply (blast intro: Spar_red.trans) |
|
40 |
done |
|
41 |
||
42 |
(* ------------------------------------------------------------------------- *) |
|
43 |
(* Confluence *) |
|
44 |
(* ------------------------------------------------------------------------- *) |
|
45 |
||
46 |
||
47 |
lemma parallel_moves: "confluence(Spar_red1)" |
|
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
48 |
apply (unfold confluence_def, clarify) |
| 12593 | 49 |
apply (frule simulation) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
50 |
apply (frule_tac n = z in simulation, clarify) |
|
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
51 |
apply (frule_tac v = va in paving) |
| 12593 | 52 |
apply (force intro: completeness)+ |
53 |
done |
|
54 |
||
55 |
lemmas confluence_parallel_reduction = |
|
56 |
parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard] |
|
57 |
||
58 |
lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)" |
|
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
59 |
by (unfold confluence_def, blast intro: par_red_red red_par_red) |
| 12593 | 60 |
|
61 |
lemmas confluence_beta_reduction = |
|
62 |
confluence_parallel_reduction [THEN lemma1, standard] |
|
63 |
||
64 |
||
65 |
(**** Conversion ****) |
|
| 1048 | 66 |
|
67 |
consts |
|
| 12593 | 68 |
Sconv1 :: "i" |
69 |
"<-1->" :: "[i,i]=>o" (infixl 50) |
|
70 |
Sconv :: "i" |
|
71 |
"<--->" :: "[i,i]=>o" (infixl 50) |
|
72 |
||
73 |
translations |
|
74 |
"a<-1->b" == "<a,b> \<in> Sconv1" |
|
75 |
"a<--->b" == "<a,b> \<in> Sconv" |
|
76 |
||
77 |
inductive |
|
78 |
domains "Sconv1" <= "lambda*lambda" |
|
79 |
intros |
|
80 |
red1: "m -1-> n ==> m<-1->n" |
|
81 |
expl: "n -1-> m ==> m<-1->n" |
|
82 |
type_intros red1D1 red1D2 lambda.intros bool_typechecks |
|
83 |
||
84 |
declare Sconv1.intros [intro] |
|
| 1048 | 85 |
|
| 12593 | 86 |
inductive |
87 |
domains "Sconv" <= "lambda*lambda" |
|
88 |
intros |
|
89 |
one_step: "m<-1->n ==> m<--->n" |
|
90 |
refl: "m \<in> lambda ==> m<--->m" |
|
91 |
trans: "[|m<--->n; n<--->p|] ==> m<--->p" |
|
92 |
type_intros Sconv1.dom_subset [THEN subsetD] lambda.intros bool_typechecks |
|
93 |
||
94 |
declare Sconv.intros [intro] |
|
95 |
||
96 |
lemma conv_sym: "m<--->n ==> n<--->m" |
|
97 |
apply (erule Sconv.induct) |
|
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
98 |
apply (erule Sconv1.induct, blast+) |
| 12593 | 99 |
done |
100 |
||
101 |
(* ------------------------------------------------------------------------- *) |
|
102 |
(* Church_Rosser Theorem *) |
|
103 |
(* ------------------------------------------------------------------------- *) |
|
104 |
||
105 |
lemma Church_Rosser: "m<--->n ==> \<exists>p.(m --->p) & (n ---> p)" |
|
106 |
apply (erule Sconv.induct) |
|
107 |
apply (erule Sconv1.induct) |
|
108 |
apply (blast intro: red1D1 redD2) |
|
109 |
apply (blast intro: red1D1 redD2) |
|
110 |
apply (blast intro: red1D1 redD2) |
|
111 |
apply (cut_tac confluence_beta_reduction) |
|
112 |
apply (unfold confluence_def) |
|
113 |
apply (blast intro: Sred.trans) |
|
114 |
done |
|
115 |
||
| 1048 | 116 |
end |
117 |