author | paulson |
Wed, 21 May 1997 10:54:10 +0200 | |
changeset 3268 | 012c43174664 |
parent 3192 | a75558a4ed37 |
child 3457 | a8ab7c64817c |
permissions | -rw-r--r-- |
3268
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
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 |
||
3268
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
6 |
Substitutions on uterms |
968 | 7 |
*) |
8 |
||
9 |
open Subst; |
|
10 |
||
11 |
||
12 |
(**** Substitutions ****) |
|
13 |
||
14 |
goal Subst.thy "t <| [] = t"; |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
15 |
by (induct_tac "t" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
16 |
by (ALLGOALS Asm_simp_tac); |
968 | 17 |
qed "subst_Nil"; |
18 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
19 |
Addsimps [subst_Nil]; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
20 |
|
968 | 21 |
goal Subst.thy "t <: u --> t <| s <: u <| s"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
22 |
by (induct_tac "u" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
23 |
by (ALLGOALS Asm_simp_tac); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
24 |
qed_spec_mp "subst_mono"; |
968 | 25 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
26 |
goal Subst.thy "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
27 |
by (case_tac "t = Var(v)" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
28 |
be rev_mp 2; |
968 | 29 |
by (res_inst_tac [("P", |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
30 |
"%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")] |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
31 |
uterm.induct 2); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
32 |
by (ALLGOALS Asm_simp_tac); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
33 |
by (Blast_tac 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
34 |
qed_spec_mp "Var_not_occs"; |
968 | 35 |
|
36 |
goal Subst.thy |
|
37 |
"(t <|r = t <|s) = (! v.v : vars_of(t) --> Var(v) <|r = Var(v) <|s)"; |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
38 |
by (induct_tac "t" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
39 |
by (ALLGOALS Asm_full_simp_tac); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
40 |
by (ALLGOALS Blast_tac); |
968 | 41 |
qed "agreement"; |
42 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
43 |
goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
44 |
by(simp_tac (!simpset addsimps [agreement] |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
45 |
setloop (split_tac [expand_if])) 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
46 |
qed_spec_mp"repl_invariance"; |
968 | 47 |
|
48 |
val asms = goal Subst.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
49 |
"v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
50 |
by (induct_tac "t" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
51 |
by (ALLGOALS Asm_simp_tac); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
52 |
qed_spec_mp"Var_in_subst"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
53 |
|
968 | 54 |
|
55 |
(**** Equality between Substitutions ****) |
|
56 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
57 |
goalw Subst.thy [subst_eq_def] "r =$= s = (! t.t <| r = t <| s)"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
58 |
by (Simp_tac 1); |
968 | 59 |
qed "subst_eq_iff"; |
60 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
61 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
62 |
local fun prove s = prove_goal Subst.thy s |
968 | 63 |
(fn prems => [cut_facts_tac prems 1, |
64 |
REPEAT (etac rev_mp 1), |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
65 |
simp_tac (!simpset addsimps [subst_eq_iff]) 1]) |
968 | 66 |
in |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
67 |
val subst_refl = prove "r =$= r"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
68 |
val subst_sym = prove "r =$= s ==> s =$= r"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
69 |
val subst_trans = prove "[| q =$= r; r =$= s |] ==> q =$= s"; |
968 | 70 |
end; |
71 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
72 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
73 |
AddIffs [subst_refl]; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
74 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
75 |
|
968 | 76 |
val eq::prems = goalw Subst.thy [subst_eq_def] |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
77 |
"[| r =$= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)"; |
968 | 78 |
by (resolve_tac [eq RS spec RS subst] 1); |
79 |
by (resolve_tac (prems RL [eq RS spec RS subst]) 1); |
|
80 |
qed "subst_subst2"; |
|
81 |
||
82 |
val ssubst_subst2 = subst_sym RS subst_subst2; |
|
83 |
||
84 |
(**** Composition of Substitutions ****) |
|
85 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
86 |
let fun prove s = |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
87 |
prove_goalw Subst.thy [comp_def,sdom_def] s (fn _ => [Simp_tac 1]) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
88 |
in |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
89 |
Addsimps |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
90 |
( |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
91 |
map prove |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
92 |
[ "[] <> bl = bl", |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
93 |
"((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)", |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
94 |
"sdom([]) = {}", |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
95 |
"sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"] |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
96 |
) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
97 |
end; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
98 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
99 |
|
968 | 100 |
goal Subst.thy "s <> [] = s"; |
101 |
by (alist_ind_tac "s" 1); |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
102 |
by (ALLGOALS Asm_simp_tac); |
968 | 103 |
qed "comp_Nil"; |
104 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
105 |
Addsimps [comp_Nil]; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
106 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
107 |
goal Subst.thy "s =$= s <> []"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
108 |
by (Simp_tac 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
109 |
qed "subst_comp_Nil"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
110 |
|
968 | 111 |
goal Subst.thy "(t <| r <> s) = (t <| r <| s)"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
112 |
by (induct_tac "t" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
113 |
by (ALLGOALS Asm_simp_tac); |
968 | 114 |
by (alist_ind_tac "r" 1); |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
115 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
968 | 116 |
qed "subst_comp"; |
117 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
118 |
Addsimps [subst_comp]; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
119 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
120 |
goal Subst.thy "(q <> r) <> s =$= q <> (r <> s)"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
121 |
by (simp_tac (!simpset addsimps [subst_eq_iff]) 1); |
968 | 122 |
qed "comp_assoc"; |
123 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
124 |
goal Subst.thy "!!s. [| theta =$= theta1; sigma =$= sigma1|] ==> \ |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
125 |
\ (theta <> sigma) =$= (theta1 <> sigma1)"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
126 |
by (asm_full_simp_tac (!simpset addsimps [subst_eq_def]) 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
127 |
qed "subst_cong"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
128 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
129 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
130 |
goal Subst.thy "(w, Var(w) <| s) # s =$= s"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
131 |
by (simp_tac (!simpset addsimps [subst_eq_iff]) 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
132 |
by (rtac allI 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
133 |
by (induct_tac "t" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
134 |
by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])))); |
968 | 135 |
qed "Cons_trivial"; |
136 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
137 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
138 |
goal Subst.thy "!!s. q <> r =$= s ==> t <| q <| r = t <| s"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
139 |
by (asm_full_simp_tac (!simpset addsimps [subst_eq_iff]) 1); |
968 | 140 |
qed "comp_subst_subst"; |
141 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
142 |
|
968 | 143 |
(**** Domain and range of Substitutions ****) |
144 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
145 |
goal Subst.thy "(v : sdom(s)) = (Var(v) <| s ~= Var(v))"; |
968 | 146 |
by (alist_ind_tac "s" 1); |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
147 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if])))); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
148 |
by (Blast_tac 1); |
968 | 149 |
qed "sdom_iff"; |
150 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
151 |
|
968 | 152 |
goalw Subst.thy [srange_def] |
153 |
"v : srange(s) = (? w.w : sdom(s) & v : vars_of(Var(w) <| s))"; |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
154 |
by (Blast_tac 1); |
968 | 155 |
qed "srange_iff"; |
156 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
157 |
goalw Set.thy [empty_def] "(A = {}) = (ALL a.~ a:A)"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
158 |
by (Blast_tac 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
159 |
qed "empty_iff_all_not"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
160 |
|
968 | 161 |
goal Subst.thy "(t <| s = t) = (sdom(s) Int vars_of(t) = {})"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
162 |
by (induct_tac "t" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
163 |
by (ALLGOALS |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
164 |
(asm_full_simp_tac (!simpset addsimps [empty_iff_all_not, sdom_iff]))); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
165 |
by (ALLGOALS Blast_tac); |
968 | 166 |
qed "invariance"; |
167 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
168 |
goal Subst.thy "v : sdom(s) --> v : vars_of(t <| s) --> v : srange(s)"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
169 |
by (induct_tac "t" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
170 |
by (case_tac "a : sdom(s)" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
171 |
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [sdom_iff, srange_iff]))); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
172 |
by (ALLGOALS Blast_tac); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
173 |
qed_spec_mp "Var_in_srange"; |
968 | 174 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
175 |
goal Subst.thy |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
176 |
"!!v. [| v : sdom(s); v ~: srange(s) |] ==> v ~: vars_of(t <| s)"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
177 |
by (blast_tac (!claset addIs [Var_in_srange]) 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
178 |
qed "Var_elim"; |
968 | 179 |
|
180 |
goal Subst.thy "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)"; |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
181 |
by (induct_tac "t" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
182 |
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [sdom_iff,srange_iff]))); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
183 |
by (Blast_tac 2); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
184 |
by (REPEAT (step_tac (!claset addIs [vars_var_iff RS iffD1 RS sym]) 1)); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
185 |
by (Auto_tac()); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
186 |
qed_spec_mp "Var_intro"; |
968 | 187 |
|
188 |
goal Subst.thy |
|
189 |
"v : srange(s) --> (? w.w : sdom(s) & v : vars_of(Var(w) <| s))"; |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
190 |
by (simp_tac (!simpset addsimps [srange_iff]) 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
191 |
qed_spec_mp "srangeD"; |
968 | 192 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
193 |
goal Subst.thy |
968 | 194 |
"sdom(s) Int srange(s) = {} = (! t.sdom(s) Int vars_of(t <| s) = {})"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
195 |
by (simp_tac (!simpset addsimps [empty_iff_all_not]) 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
196 |
by (fast_tac (!claset addIs [Var_in_srange] addDs [srangeD]) 1); |
968 | 197 |
qed "dom_range_disjoint"; |
198 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
199 |
goal Subst.thy "!!u. ~ u <| s = u ==> (? x. x : sdom(s))"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
200 |
by (full_simp_tac (!simpset addsimps [empty_iff_all_not, invariance]) 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
201 |
by (Blast_tac 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
202 |
qed "subst_not_empty"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
203 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
204 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
205 |
goal Subst.thy "(M <| [(x, Var x)]) = M"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
206 |
by (induct_tac "M" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
207 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
208 |
qed "id_subst_lemma"; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
209 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2087
diff
changeset
|
210 |
Addsimps [id_subst_lemma]; |