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