author | wenzelm |
Thu, 26 Apr 2007 14:24:08 +0200 | |
changeset 22808 | a7daa74e2980 |
parent 16417 | 9bc16273c2d4 |
child 32960 | 69916a850301 |
permissions | -rw-r--r-- |
9284 | 1 |
(* Title: ZF/Resid/Redex.thy |
1048 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Ole Rasmussen |
1048 | 4 |
Copyright 1995 University of Cambridge |
5 |
Logic Image: ZF |
|
6 |
*) |
|
7 |
||
16417 | 8 |
theory Redex imports Main begin |
1048 | 9 |
consts |
1401 | 10 |
redexes :: i |
1048 | 11 |
|
12 |
datatype |
|
12593 | 13 |
"redexes" = Var ("n \<in> nat") |
14 |
| Fun ("t \<in> redexes") |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12610
diff
changeset
|
15 |
| App ("b \<in> bool","f \<in> redexes", "a \<in> redexes") |
1048 | 16 |
|
6046 | 17 |
|
1048 | 18 |
consts |
12593 | 19 |
Ssub :: "i" |
20 |
Scomp :: "i" |
|
21 |
Sreg :: "i" |
|
22808 | 22 |
|
23 |
abbreviation |
|
24 |
Ssub_rel (infixl "<==" 70) where |
|
25 |
"a<==b == <a,b> \<in> Ssub" |
|
12593 | 26 |
|
22808 | 27 |
abbreviation |
28 |
Scomp_rel (infixl "~" 70) where |
|
29 |
"a ~ b == <a,b> \<in> Scomp" |
|
12593 | 30 |
|
22808 | 31 |
abbreviation |
32 |
"regular(a) == a \<in> Sreg" |
|
9284 | 33 |
|
22808 | 34 |
consts union_aux :: "i=>i" |
6046 | 35 |
primrec (*explicit lambda is required because both arguments of "un" vary*) |
36 |
"union_aux(Var(n)) = |
|
12593 | 37 |
(\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))" |
6046 | 38 |
|
39 |
"union_aux(Fun(u)) = |
|
12593 | 40 |
(\<lambda>t \<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y), |
6046 | 41 |
%b y z. 0, t))" |
42 |
||
43 |
"union_aux(App(b,f,a)) = |
|
12593 | 44 |
(\<lambda>t \<in> redexes. |
6046 | 45 |
redexes_case(%j. 0, %y. 0, |
9284 | 46 |
%c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))" |
6046 | 47 |
|
22808 | 48 |
definition |
49 |
union (infixl "un" 70) where |
|
50 |
"u un v == union_aux(u)`v" |
|
6046 | 51 |
|
22808 | 52 |
notation (xsymbols) |
53 |
union (infixl "\<squnion>" 70) and |
|
54 |
Ssub_rel (infixl "\<Longleftarrow>" 70) and |
|
55 |
Scomp_rel (infixl "\<sim>" 70) |
|
56 |
||
6046 | 57 |
|
58 |
inductive |
|
59 |
domains "Ssub" <= "redexes*redexes" |
|
12593 | 60 |
intros |
61 |
Sub_Var: "n \<in> nat ==> Var(n)<== Var(n)" |
|
62 |
Sub_Fun: "[|u<== v|]==> Fun(u)<== Fun(v)" |
|
63 |
Sub_App1: "[|u1<== v1; u2<== v2; b \<in> bool|]==> |
|
6046 | 64 |
App(0,u1,u2)<== App(b,v1,v2)" |
12593 | 65 |
Sub_App2: "[|u1<== v1; u2<== v2|]==> App(1,u1,u2)<== App(1,v1,v2)" |
66 |
type_intros redexes.intros bool_typechecks |
|
6046 | 67 |
|
68 |
inductive |
|
69 |
domains "Scomp" <= "redexes*redexes" |
|
12593 | 70 |
intros |
71 |
Comp_Var: "n \<in> nat ==> Var(n) ~ Var(n)" |
|
72 |
Comp_Fun: "[|u ~ v|]==> Fun(u) ~ Fun(v)" |
|
73 |
Comp_App: "[|u1 ~ v1; u2 ~ v2; b1 \<in> bool; b2 \<in> bool|] |
|
74 |
==> App(b1,u1,u2) ~ App(b2,v1,v2)" |
|
75 |
type_intros redexes.intros bool_typechecks |
|
6046 | 76 |
|
77 |
inductive |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12610
diff
changeset
|
78 |
domains "Sreg" <= redexes |
12593 | 79 |
intros |
80 |
Reg_Var: "n \<in> nat ==> regular(Var(n))" |
|
81 |
Reg_Fun: "[|regular(u)|]==> regular(Fun(u))" |
|
82 |
Reg_App1: "[|regular(Fun(u)); regular(v) |]==>regular(App(1,Fun(u),v))" |
|
83 |
Reg_App2: "[|regular(u); regular(v) |]==>regular(App(0,u,v))" |
|
84 |
type_intros redexes.intros bool_typechecks |
|
85 |
||
86 |
||
87 |
declare redexes.intros [simp] |
|
88 |
||
89 |
(* ------------------------------------------------------------------------- *) |
|
90 |
(* Specialisation of comp-rules *) |
|
91 |
(* ------------------------------------------------------------------------- *) |
|
92 |
||
93 |
lemmas compD1 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD1] |
|
94 |
lemmas compD2 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD2] |
|
95 |
lemmas regD [simp] = Sreg.dom_subset [THEN subsetD] |
|
96 |
||
97 |
(* ------------------------------------------------------------------------- *) |
|
98 |
(* Equality rules for union *) |
|
99 |
(* ------------------------------------------------------------------------- *) |
|
100 |
||
101 |
lemma union_Var [simp]: "n \<in> nat ==> Var(n) un Var(n)=Var(n)" |
|
102 |
by (simp add: union_def) |
|
103 |
||
104 |
lemma union_Fun [simp]: "v \<in> redexes ==> Fun(u) un Fun(v) = Fun(u un v)" |
|
105 |
by (simp add: union_def) |
|
106 |
||
107 |
lemma union_App [simp]: |
|
108 |
"[|b2 \<in> bool; u2 \<in> redexes; v2 \<in> redexes|] |
|
109 |
==> App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)" |
|
110 |
by (simp add: union_def) |
|
111 |
||
112 |
||
113 |
lemma or_1_right [simp]: "a or 1 = 1" |
|
114 |
by (simp add: or_def cond_def) |
|
115 |
||
116 |
lemma or_0_right [simp]: "a \<in> bool \<Longrightarrow> a or 0 = a" |
|
117 |
by (simp add: or_def cond_def bool_def, auto) |
|
118 |
||
119 |
||
120 |
||
121 |
declare Ssub.intros [simp] |
|
122 |
declare bool_typechecks [simp] |
|
123 |
declare Sreg.intros [simp] |
|
124 |
declare Scomp.intros [simp] |
|
125 |
||
126 |
declare Scomp.intros [intro] |
|
6046 | 127 |
|
12610 | 128 |
inductive_cases [elim!]: |
129 |
"regular(App(b,f,a))" |
|
130 |
"regular(Fun(b))" |
|
131 |
"regular(Var(b))" |
|
132 |
"Fun(u) ~ Fun(t)" |
|
133 |
"u ~ Fun(t)" |
|
134 |
"u ~ Var(n)" |
|
135 |
"u ~ App(b,t,a)" |
|
136 |
"Fun(t) ~ v" |
|
137 |
"App(b,f,a) ~ v" |
|
138 |
"Var(n) ~ u" |
|
12593 | 139 |
|
140 |
||
141 |
||
142 |
(* ------------------------------------------------------------------------- *) |
|
143 |
(* comp proofs *) |
|
144 |
(* ------------------------------------------------------------------------- *) |
|
145 |
||
146 |
lemma comp_refl [simp]: "u \<in> redexes ==> u ~ u" |
|
147 |
by (erule redexes.induct, blast+) |
|
148 |
||
149 |
lemma comp_sym: "u ~ v ==> v ~ u" |
|
150 |
by (erule Scomp.induct, blast+) |
|
151 |
||
152 |
lemma comp_sym_iff: "u ~ v <-> v ~ u" |
|
153 |
by (blast intro: comp_sym) |
|
154 |
||
155 |
lemma comp_trans [rule_format]: "u ~ v ==> \<forall>w. v ~ w-->u ~ w" |
|
156 |
by (erule Scomp.induct, blast+) |
|
157 |
||
158 |
(* ------------------------------------------------------------------------- *) |
|
159 |
(* union proofs *) |
|
160 |
(* ------------------------------------------------------------------------- *) |
|
161 |
||
162 |
lemma union_l: "u ~ v ==> u <== (u un v)" |
|
163 |
apply (erule Scomp.induct) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12610
diff
changeset
|
164 |
apply (erule_tac [3] boolE, simp_all) |
12593 | 165 |
done |
166 |
||
167 |
lemma union_r: "u ~ v ==> v <== (u un v)" |
|
168 |
apply (erule Scomp.induct) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12610
diff
changeset
|
169 |
apply (erule_tac [3] c = b2 in boolE, simp_all) |
12593 | 170 |
done |
171 |
||
172 |
lemma union_sym: "u ~ v ==> u un v = v un u" |
|
173 |
by (erule Scomp.induct, simp_all add: or_commute) |
|
174 |
||
175 |
(* ------------------------------------------------------------------------- *) |
|
176 |
(* regular proofs *) |
|
177 |
(* ------------------------------------------------------------------------- *) |
|
178 |
||
179 |
lemma union_preserve_regular [rule_format]: |
|
180 |
"u ~ v ==> regular(u)-->regular(v)-->regular(u un v)" |
|
13612 | 181 |
by (erule Scomp.induct, auto) |
6046 | 182 |
|
1048 | 183 |
end |
184 |