9 open Subst; |
9 open Subst; |
10 |
10 |
11 |
11 |
12 (**** Substitutions ****) |
12 (**** Substitutions ****) |
13 |
13 |
14 goal Subst.thy "t <| [] = t"; |
14 Goal "t <| [] = t"; |
15 by (induct_tac "t" 1); |
15 by (induct_tac "t" 1); |
16 by (ALLGOALS Asm_simp_tac); |
16 by (ALLGOALS Asm_simp_tac); |
17 qed "subst_Nil"; |
17 qed "subst_Nil"; |
18 |
18 |
19 Addsimps [subst_Nil]; |
19 Addsimps [subst_Nil]; |
20 |
20 |
21 goal Subst.thy "t <: u --> t <| s <: u <| s"; |
21 Goal "t <: u --> t <| s <: u <| s"; |
22 by (induct_tac "u" 1); |
22 by (induct_tac "u" 1); |
23 by (ALLGOALS Asm_simp_tac); |
23 by (ALLGOALS Asm_simp_tac); |
24 qed_spec_mp "subst_mono"; |
24 qed_spec_mp "subst_mono"; |
25 |
25 |
26 goal Subst.thy "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s"; |
26 Goal "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s"; |
27 by (case_tac "t = Var(v)" 1); |
27 by (case_tac "t = Var(v)" 1); |
28 by (etac rev_mp 2); |
28 by (etac rev_mp 2); |
29 by (res_inst_tac [("P", |
29 by (res_inst_tac [("P", |
30 "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")] |
30 "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")] |
31 uterm.induct 2); |
31 uterm.induct 2); |
32 by (ALLGOALS Asm_simp_tac); |
32 by (ALLGOALS Asm_simp_tac); |
33 by (Blast_tac 1); |
33 by (Blast_tac 1); |
34 qed_spec_mp "Var_not_occs"; |
34 qed_spec_mp "Var_not_occs"; |
35 |
35 |
36 goal Subst.thy |
36 Goal |
37 "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)"; |
37 "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)"; |
38 by (induct_tac "t" 1); |
38 by (induct_tac "t" 1); |
39 by (ALLGOALS Asm_full_simp_tac); |
39 by (ALLGOALS Asm_full_simp_tac); |
40 by (ALLGOALS Blast_tac); |
40 by (ALLGOALS Blast_tac); |
41 qed "agreement"; |
41 qed "agreement"; |
42 |
42 |
43 goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s"; |
43 Goal "~ v: vars_of(t) --> t <| (v,u)#s = t <| s"; |
44 by (simp_tac (simpset() addsimps [agreement]) 1); |
44 by (simp_tac (simpset() addsimps [agreement]) 1); |
45 qed_spec_mp"repl_invariance"; |
45 qed_spec_mp"repl_invariance"; |
46 |
46 |
47 val asms = goal Subst.thy |
47 val asms = goal Subst.thy |
48 "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)"; |
48 "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)"; |
94 "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"] |
94 "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"] |
95 ) |
95 ) |
96 end; |
96 end; |
97 |
97 |
98 |
98 |
99 goal Subst.thy "s <> [] = s"; |
99 Goal "s <> [] = s"; |
100 by (alist_ind_tac "s" 1); |
100 by (alist_ind_tac "s" 1); |
101 by (ALLGOALS Asm_simp_tac); |
101 by (ALLGOALS Asm_simp_tac); |
102 qed "comp_Nil"; |
102 qed "comp_Nil"; |
103 |
103 |
104 Addsimps [comp_Nil]; |
104 Addsimps [comp_Nil]; |
105 |
105 |
106 goal Subst.thy "s =$= s <> []"; |
106 Goal "s =$= s <> []"; |
107 by (Simp_tac 1); |
107 by (Simp_tac 1); |
108 qed "subst_comp_Nil"; |
108 qed "subst_comp_Nil"; |
109 |
109 |
110 goal Subst.thy "(t <| r <> s) = (t <| r <| s)"; |
110 Goal "(t <| r <> s) = (t <| r <| s)"; |
111 by (induct_tac "t" 1); |
111 by (induct_tac "t" 1); |
112 by (ALLGOALS Asm_simp_tac); |
112 by (ALLGOALS Asm_simp_tac); |
113 by (alist_ind_tac "r" 1); |
113 by (alist_ind_tac "r" 1); |
114 by (ALLGOALS Asm_simp_tac); |
114 by (ALLGOALS Asm_simp_tac); |
115 qed "subst_comp"; |
115 qed "subst_comp"; |
116 |
116 |
117 Addsimps [subst_comp]; |
117 Addsimps [subst_comp]; |
118 |
118 |
119 goal Subst.thy "(q <> r) <> s =$= q <> (r <> s)"; |
119 Goal "(q <> r) <> s =$= q <> (r <> s)"; |
120 by (simp_tac (simpset() addsimps [subst_eq_iff]) 1); |
120 by (simp_tac (simpset() addsimps [subst_eq_iff]) 1); |
121 qed "comp_assoc"; |
121 qed "comp_assoc"; |
122 |
122 |
123 goal Subst.thy "!!s. [| theta =$= theta1; sigma =$= sigma1|] ==> \ |
123 Goal "!!s. [| theta =$= theta1; sigma =$= sigma1|] ==> \ |
124 \ (theta <> sigma) =$= (theta1 <> sigma1)"; |
124 \ (theta <> sigma) =$= (theta1 <> sigma1)"; |
125 by (asm_full_simp_tac (simpset() addsimps [subst_eq_def]) 1); |
125 by (asm_full_simp_tac (simpset() addsimps [subst_eq_def]) 1); |
126 qed "subst_cong"; |
126 qed "subst_cong"; |
127 |
127 |
128 |
128 |
129 goal Subst.thy "(w, Var(w) <| s) # s =$= s"; |
129 Goal "(w, Var(w) <| s) # s =$= s"; |
130 by (simp_tac (simpset() addsimps [subst_eq_iff]) 1); |
130 by (simp_tac (simpset() addsimps [subst_eq_iff]) 1); |
131 by (rtac allI 1); |
131 by (rtac allI 1); |
132 by (induct_tac "t" 1); |
132 by (induct_tac "t" 1); |
133 by (ALLGOALS Asm_full_simp_tac); |
133 by (ALLGOALS Asm_full_simp_tac); |
134 qed "Cons_trivial"; |
134 qed "Cons_trivial"; |
135 |
135 |
136 |
136 |
137 goal Subst.thy "!!s. q <> r =$= s ==> t <| q <| r = t <| s"; |
137 Goal "!!s. q <> r =$= s ==> t <| q <| r = t <| s"; |
138 by (asm_full_simp_tac (simpset() addsimps [subst_eq_iff]) 1); |
138 by (asm_full_simp_tac (simpset() addsimps [subst_eq_iff]) 1); |
139 qed "comp_subst_subst"; |
139 qed "comp_subst_subst"; |
140 |
140 |
141 |
141 |
142 (**** Domain and range of Substitutions ****) |
142 (**** Domain and range of Substitutions ****) |
143 |
143 |
144 goal Subst.thy "(v : sdom(s)) = (Var(v) <| s ~= Var(v))"; |
144 Goal "(v : sdom(s)) = (Var(v) <| s ~= Var(v))"; |
145 by (alist_ind_tac "s" 1); |
145 by (alist_ind_tac "s" 1); |
146 by (ALLGOALS Asm_simp_tac); |
146 by (ALLGOALS Asm_simp_tac); |
147 by (Blast_tac 1); |
147 by (Blast_tac 1); |
148 qed "sdom_iff"; |
148 qed "sdom_iff"; |
149 |
149 |
150 |
150 |
151 goalw Subst.thy [srange_def] |
151 Goalw [srange_def] |
152 "v : srange(s) = (? w. w : sdom(s) & v : vars_of(Var(w) <| s))"; |
152 "v : srange(s) = (? w. w : sdom(s) & v : vars_of(Var(w) <| s))"; |
153 by (Blast_tac 1); |
153 by (Blast_tac 1); |
154 qed "srange_iff"; |
154 qed "srange_iff"; |
155 |
155 |
156 goalw thy [empty_def] "(A = {}) = (ALL a.~ a:A)"; |
156 Goalw [empty_def] "(A = {}) = (ALL a.~ a:A)"; |
157 by (Blast_tac 1); |
157 by (Blast_tac 1); |
158 qed "empty_iff_all_not"; |
158 qed "empty_iff_all_not"; |
159 |
159 |
160 goal Subst.thy "(t <| s = t) = (sdom(s) Int vars_of(t) = {})"; |
160 Goal "(t <| s = t) = (sdom(s) Int vars_of(t) = {})"; |
161 by (induct_tac "t" 1); |
161 by (induct_tac "t" 1); |
162 by (ALLGOALS |
162 by (ALLGOALS |
163 (asm_full_simp_tac (simpset() addsimps [empty_iff_all_not, sdom_iff]))); |
163 (asm_full_simp_tac (simpset() addsimps [empty_iff_all_not, sdom_iff]))); |
164 by (ALLGOALS Blast_tac); |
164 by (ALLGOALS Blast_tac); |
165 qed "invariance"; |
165 qed "invariance"; |
166 |
166 |
167 goal Subst.thy "v : sdom(s) --> v : vars_of(t <| s) --> v : srange(s)"; |
167 Goal "v : sdom(s) --> v : vars_of(t <| s) --> v : srange(s)"; |
168 by (induct_tac "t" 1); |
168 by (induct_tac "t" 1); |
169 by (case_tac "a : sdom(s)" 1); |
169 by (case_tac "a : sdom(s)" 1); |
170 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff, srange_iff]))); |
170 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff, srange_iff]))); |
171 by (ALLGOALS Blast_tac); |
171 by (ALLGOALS Blast_tac); |
172 qed_spec_mp "Var_in_srange"; |
172 qed_spec_mp "Var_in_srange"; |
173 |
173 |
174 goal Subst.thy |
174 Goal |
175 "!!v. [| v : sdom(s); v ~: srange(s) |] ==> v ~: vars_of(t <| s)"; |
175 "!!v. [| v : sdom(s); v ~: srange(s) |] ==> v ~: vars_of(t <| s)"; |
176 by (blast_tac (claset() addIs [Var_in_srange]) 1); |
176 by (blast_tac (claset() addIs [Var_in_srange]) 1); |
177 qed "Var_elim"; |
177 qed "Var_elim"; |
178 |
178 |
179 goal Subst.thy "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)"; |
179 Goal "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)"; |
180 by (induct_tac "t" 1); |
180 by (induct_tac "t" 1); |
181 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff,srange_iff]))); |
181 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff,srange_iff]))); |
182 by (Blast_tac 2); |
182 by (Blast_tac 2); |
183 by (safe_tac (claset() addSIs [exI, vars_var_iff RS iffD1 RS sym])); |
183 by (safe_tac (claset() addSIs [exI, vars_var_iff RS iffD1 RS sym])); |
184 by Auto_tac; |
184 by Auto_tac; |
185 qed_spec_mp "Var_intro"; |
185 qed_spec_mp "Var_intro"; |
186 |
186 |
187 goal Subst.thy |
187 Goal |
188 "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))"; |
188 "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))"; |
189 by (simp_tac (simpset() addsimps [srange_iff]) 1); |
189 by (simp_tac (simpset() addsimps [srange_iff]) 1); |
190 qed_spec_mp "srangeD"; |
190 qed_spec_mp "srangeD"; |
191 |
191 |
192 goal Subst.thy |
192 Goal |
193 "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})"; |
193 "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})"; |
194 by (simp_tac (simpset() addsimps [empty_iff_all_not]) 1); |
194 by (simp_tac (simpset() addsimps [empty_iff_all_not]) 1); |
195 by (fast_tac (claset() addIs [Var_in_srange] addDs [srangeD]) 1); |
195 by (fast_tac (claset() addIs [Var_in_srange] addDs [srangeD]) 1); |
196 qed "dom_range_disjoint"; |
196 qed "dom_range_disjoint"; |
197 |
197 |
198 goal Subst.thy "!!u. ~ u <| s = u ==> (? x. x : sdom(s))"; |
198 Goal "!!u. ~ u <| s = u ==> (? x. x : sdom(s))"; |
199 by (full_simp_tac (simpset() addsimps [empty_iff_all_not, invariance]) 1); |
199 by (full_simp_tac (simpset() addsimps [empty_iff_all_not, invariance]) 1); |
200 by (Blast_tac 1); |
200 by (Blast_tac 1); |
201 qed "subst_not_empty"; |
201 qed "subst_not_empty"; |
202 |
202 |
203 |
203 |
204 goal Subst.thy "(M <| [(x, Var x)]) = M"; |
204 Goal "(M <| [(x, Var x)]) = M"; |
205 by (induct_tac "M" 1); |
205 by (induct_tac "M" 1); |
206 by (ALLGOALS Asm_simp_tac); |
206 by (ALLGOALS Asm_simp_tac); |
207 qed "id_subst_lemma"; |
207 qed "id_subst_lemma"; |
208 |
208 |
209 Addsimps [id_subst_lemma]; |
209 Addsimps [id_subst_lemma]; |