author | paulson <lp15@cam.ac.uk> |
Tue, 27 Sep 2022 17:54:20 +0100 | |
changeset 76216 | 9fc34f76b4e8 |
parent 76215 | a642599ffdea |
child 76217 | 8655344f1cf6 |
permissions | -rw-r--r-- |
35762 | 1 |
(* Title: ZF/Resid/Confluence.thy |
1478 | 2 |
Author: Ole Rasmussen |
1048 | 3 |
Copyright 1995 University of Cambridge |
4 |
*) |
|
5 |
||
16417 | 6 |
theory Confluence imports Reduction begin |
12593 | 7 |
|
24893 | 8 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
9 |
confluence :: "i\<Rightarrow>o" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
10 |
"confluence(R) \<equiv> |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
11 |
\<forall>x y. \<langle>x,y\<rangle> \<in> R \<longrightarrow> (\<forall>z.\<langle>x,z\<rangle> \<in> R \<longrightarrow> (\<exists>u.\<langle>y,u\<rangle> \<in> R \<and> \<langle>z,u\<rangle> \<in> R))" |
12593 | 12 |
|
24893 | 13 |
definition |
14 |
strip :: "o" where |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
15 |
"strip \<equiv> \<forall>x y. (x =\<Longrightarrow> y) \<longrightarrow> |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
16 |
(\<forall>z.(x =1\<Rightarrow> z) \<longrightarrow> (\<exists>u.(y =1\<Rightarrow> u) \<and> (z=\<Longrightarrow>u)))" |
12593 | 17 |
|
18 |
||
19 |
(* ------------------------------------------------------------------------- *) |
|
20 |
(* strip lemmas *) |
|
21 |
(* ------------------------------------------------------------------------- *) |
|
22 |
||
23 |
lemma strip_lemma_r: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
24 |
"\<lbrakk>confluence(Spar_red1)\<rbrakk>\<Longrightarrow> strip" |
12593 | 25 |
apply (unfold confluence_def strip_def) |
26 |
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
|
27 |
apply (erule Spar_red.induct, fast) |
12593 | 28 |
apply (fast intro: Spar_red.trans) |
29 |
done |
|
30 |
||
31 |
||
32 |
lemma strip_lemma_l: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
33 |
"strip\<Longrightarrow> confluence(Spar_red)" |
12593 | 34 |
apply (unfold confluence_def strip_def) |
35 |
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
|
36 |
apply (erule Spar_red.induct, blast) |
12593 | 37 |
apply clarify |
38 |
apply (blast intro: Spar_red.trans) |
|
39 |
done |
|
40 |
||
41 |
(* ------------------------------------------------------------------------- *) |
|
42 |
(* Confluence *) |
|
43 |
(* ------------------------------------------------------------------------- *) |
|
44 |
||
45 |
||
46 |
lemma parallel_moves: "confluence(Spar_red1)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
47 |
apply (unfold confluence_def, clarify) |
12593 | 48 |
apply (frule simulation) |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
49 |
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
|
50 |
apply (frule_tac v = va in paving) |
12593 | 51 |
apply (force intro: completeness)+ |
52 |
done |
|
53 |
||
54 |
lemmas confluence_parallel_reduction = |
|
45602 | 55 |
parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l] |
12593 | 56 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
57 |
lemma lemma1: "\<lbrakk>confluence(Spar_red)\<rbrakk>\<Longrightarrow> confluence(Sred)" |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
58 |
by (unfold confluence_def, blast intro: par_red_red red_par_red) |
12593 | 59 |
|
60 |
lemmas confluence_beta_reduction = |
|
45602 | 61 |
confluence_parallel_reduction [THEN lemma1] |
12593 | 62 |
|
63 |
||
64 |
(**** Conversion ****) |
|
1048 | 65 |
|
66 |
consts |
|
12593 | 67 |
Sconv1 :: "i" |
68 |
Sconv :: "i" |
|
69 |
||
22808 | 70 |
abbreviation |
69587 | 71 |
Sconv1_rel (infixl \<open><-1->\<close> 50) where |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
72 |
"a<-1->b \<equiv> \<langle>a,b\<rangle> \<in> Sconv1" |
22808 | 73 |
|
74 |
abbreviation |
|
69587 | 75 |
Sconv_rel (infixl \<open><-\<longrightarrow>\<close> 50) where |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
76 |
"a<-\<longrightarrow>b \<equiv> \<langle>a,b\<rangle> \<in> Sconv" |
12593 | 77 |
|
78 |
inductive |
|
46823 | 79 |
domains "Sconv1" \<subseteq> "lambda*lambda" |
12593 | 80 |
intros |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
81 |
red1: "m -1-> n \<Longrightarrow> m<-1->n" |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
82 |
expl: "n -1-> m \<Longrightarrow> m<-1->n" |
12593 | 83 |
type_intros red1D1 red1D2 lambda.intros bool_typechecks |
84 |
||
85 |
declare Sconv1.intros [intro] |
|
1048 | 86 |
|
12593 | 87 |
inductive |
46823 | 88 |
domains "Sconv" \<subseteq> "lambda*lambda" |
12593 | 89 |
intros |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
90 |
one_step: "m<-1->n \<Longrightarrow> m<-\<longrightarrow>n" |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
91 |
refl: "m \<in> lambda \<Longrightarrow> m<-\<longrightarrow>m" |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
92 |
trans: "\<lbrakk>m<-\<longrightarrow>n; n<-\<longrightarrow>p\<rbrakk> \<Longrightarrow> m<-\<longrightarrow>p" |
12593 | 93 |
type_intros Sconv1.dom_subset [THEN subsetD] lambda.intros bool_typechecks |
94 |
||
95 |
declare Sconv.intros [intro] |
|
96 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69587
diff
changeset
|
97 |
lemma conv_sym: "m<-\<longrightarrow>n \<Longrightarrow> n<-\<longrightarrow>m" |
12593 | 98 |
apply (erule Sconv.induct) |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
99 |
apply (erule Sconv1.induct, blast+) |
12593 | 100 |
done |
101 |
||
102 |
(* ------------------------------------------------------------------------- *) |
|
103 |
(* Church_Rosser Theorem *) |
|
104 |
(* ------------------------------------------------------------------------- *) |
|
105 |
||
76214 | 106 |
lemma Church_Rosser: "m<-\<longrightarrow>n \<Longrightarrow> \<exists>p.(m -\<longrightarrow>p) \<and> (n -\<longrightarrow> p)" |
12593 | 107 |
apply (erule Sconv.induct) |
108 |
apply (erule Sconv1.induct) |
|
109 |
apply (blast intro: red1D1 redD2) |
|
110 |
apply (blast intro: red1D1 redD2) |
|
111 |
apply (blast intro: red1D1 redD2) |
|
112 |
apply (cut_tac confluence_beta_reduction) |
|
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
113 |
unfolding confluence_def |
12593 | 114 |
apply (blast intro: Sred.trans) |
115 |
done |
|
116 |
||
1048 | 117 |
end |
118 |