|
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])
|
|
|
28 |
apply (erule Spar_red.induct)
|
|
|
29 |
apply fast
|
|
|
30 |
apply (fast intro: Spar_red.trans)
|
|
|
31 |
done
|
|
|
32 |
|
|
|
33 |
|
|
|
34 |
lemma strip_lemma_l:
|
|
|
35 |
"strip==> confluence(Spar_red)"
|
|
|
36 |
apply (unfold confluence_def strip_def)
|
|
|
37 |
apply (rule impI [THEN allI, THEN allI])
|
|
|
38 |
apply (erule Spar_red.induct)
|
|
|
39 |
apply blast
|
|
|
40 |
apply clarify
|
|
|
41 |
apply (blast intro: Spar_red.trans)
|
|
|
42 |
done
|
|
|
43 |
|
|
|
44 |
(* ------------------------------------------------------------------------- *)
|
|
|
45 |
(* Confluence *)
|
|
|
46 |
(* ------------------------------------------------------------------------- *)
|
|
|
47 |
|
|
|
48 |
|
|
|
49 |
lemma parallel_moves: "confluence(Spar_red1)"
|
|
|
50 |
apply (unfold confluence_def)
|
|
|
51 |
apply clarify
|
|
|
52 |
apply (frule simulation)
|
|
|
53 |
apply (frule_tac n = "z" in simulation)
|
|
|
54 |
apply clarify
|
|
|
55 |
apply (frule_tac v = "va" in paving)
|
|
|
56 |
apply (force intro: completeness)+
|
|
|
57 |
done
|
|
|
58 |
|
|
|
59 |
lemmas confluence_parallel_reduction =
|
|
|
60 |
parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard]
|
|
|
61 |
|
|
|
62 |
lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)"
|
|
|
63 |
apply (unfold confluence_def, blast intro: par_red_red red_par_red)
|
|
|
64 |
done
|
|
|
65 |
|
|
|
66 |
lemmas confluence_beta_reduction =
|
|
|
67 |
confluence_parallel_reduction [THEN lemma1, standard]
|
|
|
68 |
|
|
|
69 |
|
|
|
70 |
(**** Conversion ****)
|
|
1048
|
71 |
|
|
|
72 |
consts
|
|
12593
|
73 |
Sconv1 :: "i"
|
|
|
74 |
"<-1->" :: "[i,i]=>o" (infixl 50)
|
|
|
75 |
Sconv :: "i"
|
|
|
76 |
"<--->" :: "[i,i]=>o" (infixl 50)
|
|
|
77 |
|
|
|
78 |
translations
|
|
|
79 |
"a<-1->b" == "<a,b> \<in> Sconv1"
|
|
|
80 |
"a<--->b" == "<a,b> \<in> Sconv"
|
|
|
81 |
|
|
|
82 |
inductive
|
|
|
83 |
domains "Sconv1" <= "lambda*lambda"
|
|
|
84 |
intros
|
|
|
85 |
red1: "m -1-> n ==> m<-1->n"
|
|
|
86 |
expl: "n -1-> m ==> m<-1->n"
|
|
|
87 |
type_intros red1D1 red1D2 lambda.intros bool_typechecks
|
|
|
88 |
|
|
|
89 |
declare Sconv1.intros [intro]
|
|
1048
|
90 |
|
|
12593
|
91 |
inductive
|
|
|
92 |
domains "Sconv" <= "lambda*lambda"
|
|
|
93 |
intros
|
|
|
94 |
one_step: "m<-1->n ==> m<--->n"
|
|
|
95 |
refl: "m \<in> lambda ==> m<--->m"
|
|
|
96 |
trans: "[|m<--->n; n<--->p|] ==> m<--->p"
|
|
|
97 |
type_intros Sconv1.dom_subset [THEN subsetD] lambda.intros bool_typechecks
|
|
|
98 |
|
|
|
99 |
declare Sconv.intros [intro]
|
|
|
100 |
|
|
|
101 |
lemma conv_sym: "m<--->n ==> n<--->m"
|
|
|
102 |
apply (erule Sconv.induct)
|
|
|
103 |
apply (erule Sconv1.induct)
|
|
|
104 |
apply blast+
|
|
|
105 |
done
|
|
|
106 |
|
|
|
107 |
(* ------------------------------------------------------------------------- *)
|
|
|
108 |
(* Church_Rosser Theorem *)
|
|
|
109 |
(* ------------------------------------------------------------------------- *)
|
|
|
110 |
|
|
|
111 |
lemma Church_Rosser: "m<--->n ==> \<exists>p.(m --->p) & (n ---> p)"
|
|
|
112 |
apply (erule Sconv.induct)
|
|
|
113 |
apply (erule Sconv1.induct)
|
|
|
114 |
apply (blast intro: red1D1 redD2)
|
|
|
115 |
apply (blast intro: red1D1 redD2)
|
|
|
116 |
apply (blast intro: red1D1 redD2)
|
|
|
117 |
apply (cut_tac confluence_beta_reduction)
|
|
|
118 |
apply (unfold confluence_def)
|
|
|
119 |
apply (blast intro: Sred.trans)
|
|
|
120 |
done
|
|
|
121 |
|
|
1048
|
122 |
end
|
|
|
123 |
|