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 |
|
12593
|
8 |
theory Redex = Main:
|
1048
|
9 |
consts
|
1401
|
10 |
redexes :: i
|
1048
|
11 |
|
|
12 |
datatype
|
12593
|
13 |
"redexes" = Var ("n \<in> nat")
|
|
14 |
| Fun ("t \<in> redexes")
|
|
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"
|
|
22 |
union_aux :: "i=>i"
|
|
23 |
regular :: "i=>o"
|
6046
|
24 |
|
12593
|
25 |
(*syntax??*)
|
|
26 |
un :: "[i,i]=>i" (infixl 70)
|
|
27 |
"<==" :: "[i,i]=>o" (infixl 70)
|
|
28 |
"~" :: "[i,i]=>o" (infixl 70)
|
|
29 |
|
|
30 |
|
9284
|
31 |
translations
|
12593
|
32 |
"a<==b" == "<a,b> \<in> Ssub"
|
|
33 |
"a ~ b" == "<a,b> \<in> Scomp"
|
|
34 |
"regular(a)" == "a \<in> Sreg"
|
9284
|
35 |
|
|
36 |
|
6046
|
37 |
primrec (*explicit lambda is required because both arguments of "un" vary*)
|
|
38 |
"union_aux(Var(n)) =
|
12593
|
39 |
(\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
|
6046
|
40 |
|
|
41 |
"union_aux(Fun(u)) =
|
12593
|
42 |
(\<lambda>t \<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
|
6046
|
43 |
%b y z. 0, t))"
|
|
44 |
|
|
45 |
"union_aux(App(b,f,a)) =
|
12593
|
46 |
(\<lambda>t \<in> redexes.
|
6046
|
47 |
redexes_case(%j. 0, %y. 0,
|
9284
|
48 |
%c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
|
6046
|
49 |
|
1048
|
50 |
defs
|
12593
|
51 |
union_def: "u un v == union_aux(u)`v"
|
6046
|
52 |
|
12593
|
53 |
syntax (xsymbols)
|
|
54 |
"op un" :: "[i,i]=>i" (infixl "\<squnion>" 70)
|
|
55 |
"op <==" :: "[i,i]=>o" (infixl "\<Longleftarrow>" 70)
|
|
56 |
"op ~" :: "[i,i]=>o" (infixl "\<sim>" 70)
|
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
|
|
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 |
|
12593
|
128 |
inductive_cases [elim!]: "regular(App(b,f,a))"
|
|
129 |
inductive_cases [elim!]: "regular(Fun(b))"
|
|
130 |
inductive_cases [elim!]: "regular(Var(b))"
|
|
131 |
inductive_cases [elim!]: "Fun(u) ~ Fun(t)"
|
|
132 |
inductive_cases [elim!]: "u ~ Fun(t)"
|
|
133 |
inductive_cases [elim!]: "u ~ Var(n)"
|
|
134 |
inductive_cases [elim!]: "u ~ App(b,t,a)"
|
|
135 |
inductive_cases [elim!]: "Fun(t) ~ v"
|
|
136 |
inductive_cases [elim!]: "App(b,f,a) ~ v"
|
|
137 |
inductive_cases [elim!]: "Var(n) ~ u"
|
|
138 |
|
|
139 |
|
|
140 |
|
|
141 |
(* ------------------------------------------------------------------------- *)
|
|
142 |
(* comp proofs *)
|
|
143 |
(* ------------------------------------------------------------------------- *)
|
|
144 |
|
|
145 |
lemma comp_refl [simp]: "u \<in> redexes ==> u ~ u"
|
|
146 |
by (erule redexes.induct, blast+)
|
|
147 |
|
|
148 |
lemma comp_sym: "u ~ v ==> v ~ u"
|
|
149 |
by (erule Scomp.induct, blast+)
|
|
150 |
|
|
151 |
lemma comp_sym_iff: "u ~ v <-> v ~ u"
|
|
152 |
by (blast intro: comp_sym)
|
|
153 |
|
|
154 |
lemma comp_trans [rule_format]: "u ~ v ==> \<forall>w. v ~ w-->u ~ w"
|
|
155 |
by (erule Scomp.induct, blast+)
|
|
156 |
|
|
157 |
(* ------------------------------------------------------------------------- *)
|
|
158 |
(* union proofs *)
|
|
159 |
(* ------------------------------------------------------------------------- *)
|
|
160 |
|
|
161 |
lemma union_l: "u ~ v ==> u <== (u un v)"
|
|
162 |
apply (erule Scomp.induct)
|
|
163 |
apply (erule_tac [3] boolE)
|
|
164 |
apply simp_all
|
|
165 |
done
|
|
166 |
|
|
167 |
lemma union_r: "u ~ v ==> v <== (u un v)"
|
|
168 |
apply (erule Scomp.induct)
|
|
169 |
apply (erule_tac [3] c = "b2" in boolE)
|
|
170 |
apply simp_all
|
|
171 |
done
|
|
172 |
|
|
173 |
lemma union_sym: "u ~ v ==> u un v = v un u"
|
|
174 |
by (erule Scomp.induct, simp_all add: or_commute)
|
|
175 |
|
|
176 |
(* ------------------------------------------------------------------------- *)
|
|
177 |
(* regular proofs *)
|
|
178 |
(* ------------------------------------------------------------------------- *)
|
|
179 |
|
|
180 |
lemma union_preserve_regular [rule_format]:
|
|
181 |
"u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"
|
|
182 |
apply (erule Scomp.induct)
|
|
183 |
apply auto
|
|
184 |
(*select the given assumption for simplification*)
|
|
185 |
apply (erule_tac P = "regular (Fun (?u) un ?v) " in rev_mp)
|
|
186 |
apply simp
|
|
187 |
done
|
6046
|
188 |
|
1048
|
189 |
end
|
|
190 |
|