author | paulson |
Thu, 10 Oct 1996 11:58:40 +0200 | |
changeset 2087 | 6405a3bb490b |
parent 1465 | 5d7a7e439cec |
child 3192 | a75558a4ed37 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Subst/subst.ML |
1266 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
968 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
For subst.thy. |
|
7 |
*) |
|
8 |
||
9 |
open Subst; |
|
10 |
||
11 |
(***********) |
|
12 |
||
13 |
val subst_defs = [subst_def,comp_def,sdom_def]; |
|
14 |
||
1266 | 15 |
val raw_subst_ss = simpset_of "UTLemmas" addsimps al_rews; |
968 | 16 |
|
17 |
local fun mk_thm s = prove_goalw Subst.thy subst_defs s |
|
18 |
(fn _ => [simp_tac raw_subst_ss 1]) |
|
19 |
in val subst_rews = map mk_thm |
|
20 |
["Const(c) <| al = Const(c)", |
|
21 |
"Comb t u <| al = Comb (t <| al) (u <| al)", |
|
22 |
"[] <> bl = bl", |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
23 |
"((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)", |
968 | 24 |
"sdom([]) = {}", |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
25 |
"sdom((a,b)#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \ |
968 | 26 |
\ else (sdom al) Un {a})" |
27 |
]; |
|
28 |
(* This rewrite isn't always desired *) |
|
29 |
val Var_subst = mk_thm "Var(x) <| al = assoc x (Var x) al"; |
|
30 |
end; |
|
31 |
||
2087 | 32 |
val subst_ss = raw_subst_ss addsimps subst_rews |
33 |
delsimps [de_Morgan_conj, de_Morgan_disj]; |
|
968 | 34 |
|
35 |
(**** Substitutions ****) |
|
36 |
||
37 |
goal Subst.thy "t <| [] = t"; |
|
38 |
by (uterm_ind_tac "t" 1); |
|
39 |
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst]))); |
|
40 |
qed "subst_Nil"; |
|
41 |
||
42 |
goal Subst.thy "t <: u --> t <| s <: u <| s"; |
|
43 |
by (uterm_ind_tac "u" 1); |
|
44 |
by (ALLGOALS (asm_simp_tac subst_ss)); |
|
45 |
val subst_mono = store_thm("subst_mono", result() RS mp); |
|
46 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
47 |
goal Subst.thy "~ (Var(v) <: t) --> t <| (v,t <| s)#s = t <| s"; |
968 | 48 |
by (imp_excluded_middle_tac "t = Var(v)" 1); |
49 |
by (res_inst_tac [("P", |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
50 |
"%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")] |
968 | 51 |
uterm_induct 2); |
52 |
by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst]))); |
|
53 |
by (fast_tac HOL_cs 1); |
|
54 |
val Var_not_occs = store_thm("Var_not_occs", result() RS mp); |
|
55 |
||
56 |
goal Subst.thy |
|
57 |
"(t <|r = t <|s) = (! v.v : vars_of(t) --> Var(v) <|r = Var(v) <|s)"; |
|
58 |
by (uterm_ind_tac "t" 1); |
|
59 |
by (REPEAT (etac rev_mp 3)); |
|
60 |
by (ALLGOALS (asm_simp_tac subst_ss)); |
|
61 |
by (ALLGOALS (fast_tac HOL_cs)); |
|
62 |
qed "agreement"; |
|
63 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
64 |
goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s"; |
968 | 65 |
by(simp_tac(subst_ss addsimps [agreement,Var_subst] |
66 |
setloop (split_tac [expand_if])) 1); |
|
67 |
val repl_invariance = store_thm("repl_invariance", result() RS mp); |
|
68 |
||
69 |
val asms = goal Subst.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
70 |
"v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)"; |
968 | 71 |
by (uterm_ind_tac "t" 1); |
72 |
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst]))); |
|
73 |
val Var_in_subst = store_thm("Var_in_subst", result() RS mp); |
|
74 |
||
75 |
(**** Equality between Substitutions ****) |
|
76 |
||
77 |
goalw Subst.thy [subst_eq_def] "r =s= s = (! t.t <| r = t <| s)"; |
|
78 |
by (simp_tac subst_ss 1); |
|
79 |
qed "subst_eq_iff"; |
|
80 |
||
81 |
local fun mk_thm s = prove_goal Subst.thy s |
|
82 |
(fn prems => [cut_facts_tac prems 1, |
|
83 |
REPEAT (etac rev_mp 1), |
|
84 |
simp_tac (subst_ss addsimps [subst_eq_iff]) 1]) |
|
85 |
in |
|
86 |
val subst_refl = mk_thm "r = s ==> r =s= s"; |
|
87 |
val subst_sym = mk_thm "r =s= s ==> s =s= r"; |
|
88 |
val subst_trans = mk_thm "[| q =s= r; r =s= s |] ==> q =s= s"; |
|
89 |
end; |
|
90 |
||
91 |
val eq::prems = goalw Subst.thy [subst_eq_def] |
|
92 |
"[| r =s= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)"; |
|
93 |
by (resolve_tac [eq RS spec RS subst] 1); |
|
94 |
by (resolve_tac (prems RL [eq RS spec RS subst]) 1); |
|
95 |
qed "subst_subst2"; |
|
96 |
||
97 |
val ssubst_subst2 = subst_sym RS subst_subst2; |
|
98 |
||
99 |
(**** Composition of Substitutions ****) |
|
100 |
||
101 |
goal Subst.thy "s <> [] = s"; |
|
102 |
by (alist_ind_tac "s" 1); |
|
103 |
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [subst_Nil]))); |
|
104 |
qed "comp_Nil"; |
|
105 |
||
106 |
goal Subst.thy "(t <| r <> s) = (t <| r <| s)"; |
|
107 |
by (uterm_ind_tac "t" 1); |
|
108 |
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst]))); |
|
109 |
by (alist_ind_tac "r" 1); |
|
110 |
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst,subst_Nil] |
|
111 |
setloop (split_tac [expand_if])))); |
|
112 |
qed "subst_comp"; |
|
113 |
||
114 |
goal Subst.thy "(q <> r) <> s =s= q <> (r <> s)"; |
|
115 |
by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1); |
|
116 |
qed "comp_assoc"; |
|
117 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
118 |
goal Subst.thy "(w,Var(w) <| s)#s =s= s"; |
968 | 119 |
by (rtac (allI RS (subst_eq_iff RS iffD2)) 1); |
120 |
by (uterm_ind_tac "t" 1); |
|
121 |
by (REPEAT (etac rev_mp 3)); |
|
122 |
by (ALLGOALS (simp_tac (subst_ss addsimps[Var_subst] |
|
123 |
setloop (split_tac [expand_if])))); |
|
124 |
qed "Cons_trivial"; |
|
125 |
||
126 |
val [prem] = goal Subst.thy "q <> r =s= s ==> t <| q <| r = t <| s"; |
|
127 |
by (simp_tac (subst_ss addsimps [prem RS (subst_eq_iff RS iffD1), |
|
1465 | 128 |
subst_comp RS sym]) 1); |
968 | 129 |
qed "comp_subst_subst"; |
130 |
||
131 |
(**** Domain and range of Substitutions ****) |
|
132 |
||
133 |
goal Subst.thy "(v : sdom(s)) = (~ Var(v) <| s = Var(v))"; |
|
134 |
by (alist_ind_tac "s" 1); |
|
135 |
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst] |
|
136 |
setloop (split_tac[expand_if])))); |
|
137 |
by (fast_tac HOL_cs 1); |
|
138 |
qed "sdom_iff"; |
|
139 |
||
140 |
goalw Subst.thy [srange_def] |
|
141 |
"v : srange(s) = (? w.w : sdom(s) & v : vars_of(Var(w) <| s))"; |
|
142 |
by (fast_tac set_cs 1); |
|
143 |
qed "srange_iff"; |
|
144 |
||
145 |
goal Subst.thy "(t <| s = t) = (sdom(s) Int vars_of(t) = {})"; |
|
146 |
by (uterm_ind_tac "t" 1); |
|
147 |
by (REPEAT (etac rev_mp 3)); |
|
148 |
by (ALLGOALS (simp_tac (subst_ss addsimps [sdom_iff,Var_subst]))); |
|
149 |
by (ALLGOALS (fast_tac set_cs)); |
|
150 |
qed "invariance"; |
|
151 |
||
152 |
goal Subst.thy "v : sdom(s) --> ~v : srange(s) --> ~v : vars_of(t <| s)"; |
|
153 |
by (uterm_ind_tac "t" 1); |
|
154 |
by (imp_excluded_middle_tac "x : sdom(s)" 1); |
|
155 |
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [sdom_iff,srange_iff]))); |
|
156 |
by (ALLGOALS (fast_tac set_cs)); |
|
157 |
val Var_elim = store_thm("Var_elim", result() RS mp RS mp); |
|
158 |
||
159 |
val asms = goal Subst.thy |
|
160 |
"[| v : sdom(s); v : vars_of(t <| s) |] ==> v : srange(s)"; |
|
161 |
by (REPEAT (ares_tac (asms @ [Var_elim RS swap RS classical]) 1)); |
|
162 |
qed "Var_elim2"; |
|
163 |
||
164 |
goal Subst.thy "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)"; |
|
165 |
by (uterm_ind_tac "t" 1); |
|
166 |
by (REPEAT_SOME (etac rev_mp )); |
|
167 |
by (ALLGOALS (simp_tac (subst_ss addsimps [sdom_iff,srange_iff]))); |
|
168 |
by (REPEAT (step_tac (set_cs addIs [vars_var_iff RS iffD1 RS sym]) 1)); |
|
169 |
by (etac notE 1); |
|
170 |
by (etac subst 1); |
|
171 |
by (ALLGOALS (fast_tac set_cs)); |
|
172 |
val Var_intro = store_thm("Var_intro", result() RS mp); |
|
173 |
||
174 |
goal Subst.thy |
|
175 |
"v : srange(s) --> (? w.w : sdom(s) & v : vars_of(Var(w) <| s))"; |
|
176 |
by (simp_tac (subst_ss addsimps [srange_iff]) 1); |
|
177 |
val srangeE = store_thm("srangeE", make_elim (result() RS mp)); |
|
178 |
||
179 |
val asms = goal Subst.thy |
|
180 |
"sdom(s) Int srange(s) = {} = (! t.sdom(s) Int vars_of(t <| s) = {})"; |
|
181 |
by (simp_tac subst_ss 1); |
|
182 |
by (fast_tac (set_cs addIs [Var_elim2] addEs [srangeE]) 1); |
|
183 |
qed "dom_range_disjoint"; |
|
184 |
||
185 |
val asms = goal Subst.thy "~ u <| s = u --> (? x.x : sdom(s))"; |
|
186 |
by (simp_tac (subst_ss addsimps [invariance]) 1); |
|
187 |
by (fast_tac set_cs 1); |
|
188 |
val subst_not_empty = store_thm("subst_not_empty", result() RS mp); |