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