author | paulson |
Tue, 29 Mar 2005 12:30:48 +0200 | |
changeset 15635 | 8408a06590a6 |
parent 5184 | 9b8547a9496a |
child 15648 | f6da795ee27a |
permissions | -rw-r--r-- |
3268
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
1 |
(* Title: Subst/Subst.thy |
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
2 |
ID: $Id$ |
1476 | 3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
968 | 4 |
Copyright 1993 University of Cambridge |
5 |
*) |
|
6 |
||
15635 | 7 |
header{*Substitutions on uterms*} |
8 |
||
9 |
theory Subst |
|
10 |
imports AList UTerm |
|
11 |
begin |
|
968 | 12 |
|
13 |
consts |
|
14 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
15 |
"=$=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
16 |
"<|" :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl 55) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
17 |
"<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
18 |
=> ('a*('a uterm)) list" (infixl 56) |
968 | 19 |
sdom :: "('a*('a uterm)) list => 'a set" |
20 |
srange :: "('a*('a uterm)) list => 'a set" |
|
21 |
||
22 |
||
5184 | 23 |
primrec |
15635 | 24 |
subst_Var: "(Var v <| s) = assoc v (Var v) s" |
25 |
subst_Const: "(Const c <| s) = Const c" |
|
26 |
subst_Comb: "(Comb M N <| s) = Comb (M <| s) (N <| s)" |
|
968 | 27 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
28 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
29 |
defs |
968 | 30 |
|
15635 | 31 |
subst_eq_def: "r =$= s == ALL t. t <| r = t <| s" |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
32 |
|
15635 | 33 |
comp_def: "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)" |
968 | 34 |
|
15635 | 35 |
sdom_def: |
1151 | 36 |
"sdom(al) == alist_rec al {} |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
37 |
(%x y xs g. if Var(x)=y then g - {x} else g Un {x})" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
38 |
|
15635 | 39 |
srange_def: |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
40 |
"srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})" |
968 | 41 |
|
15635 | 42 |
|
43 |
||
44 |
subsection{*Basic Laws*} |
|
45 |
||
46 |
lemma subst_Nil [simp]: "t <| [] = t" |
|
47 |
by (induct_tac "t", auto) |
|
48 |
||
49 |
lemma subst_mono [rule_format]: "t <: u --> t <| s <: u <| s" |
|
50 |
by (induct_tac "u", auto) |
|
51 |
||
52 |
lemma Var_not_occs [rule_format]: |
|
53 |
"~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s" |
|
54 |
apply (case_tac "t = Var v") |
|
55 |
apply (erule_tac [2] rev_mp) |
|
56 |
apply (rule_tac [2] P = "%x.~x=Var (v) --> ~ (Var (v) <: x) --> x <| (v,t<|s) #s=x<|s" in uterm.induct) |
|
57 |
apply auto |
|
58 |
done |
|
59 |
||
60 |
lemma agreement: "(t <|r = t <|s) = (\<forall>v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)" |
|
61 |
by (induct_tac "t", auto) |
|
62 |
||
63 |
lemma repl_invariance: "~ v: vars_of(t) ==> t <| (v,u)#s = t <| s" |
|
64 |
by (simp add: agreement) |
|
65 |
||
66 |
lemma Var_in_subst [rule_format]: |
|
67 |
"v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)" |
|
68 |
by (induct_tac "t", auto) |
|
69 |
||
70 |
||
71 |
subsection{*Equality between Substitutions*} |
|
72 |
||
73 |
lemma subst_eq_iff: "r =$= s = (\<forall>t. t <| r = t <| s)" |
|
74 |
by (simp add: subst_eq_def) |
|
75 |
||
76 |
lemma subst_refl [iff]: "r =$= r" |
|
77 |
by (simp add: subst_eq_iff) |
|
78 |
||
79 |
lemma subst_sym: "r =$= s ==> s =$= r" |
|
80 |
by (simp add: subst_eq_iff) |
|
81 |
||
82 |
lemma subst_trans: "[| q =$= r; r =$= s |] ==> q =$= s" |
|
83 |
by (simp add: subst_eq_iff) |
|
84 |
||
85 |
lemma subst_subst2: |
|
86 |
"[| r =$= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)" |
|
87 |
by (simp add: subst_eq_def) |
|
88 |
||
89 |
lemmas ssubst_subst2 = subst_sym [THEN subst_subst2] |
|
90 |
||
91 |
||
92 |
subsection{*Composition of Substitutions*} |
|
93 |
||
94 |
lemma [simp]: |
|
95 |
"[] <> bl = bl" |
|
96 |
"((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)" |
|
97 |
"sdom([]) = {}" |
|
98 |
"sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})" |
|
99 |
by (simp_all add: comp_def sdom_def) |
|
100 |
||
101 |
lemma comp_Nil [simp]: "s <> [] = s" |
|
102 |
by (induct "s", auto) |
|
103 |
||
104 |
lemma subst_comp_Nil: "s =$= s <> []" |
|
105 |
by simp |
|
106 |
||
107 |
lemma subst_comp [simp]: "(t <| r <> s) = (t <| r <| s)" |
|
108 |
apply (induct_tac "t") |
|
109 |
apply (simp_all (no_asm_simp)) |
|
110 |
apply (induct "r", auto) |
|
111 |
done |
|
112 |
||
113 |
lemma comp_assoc: "(q <> r) <> s =$= q <> (r <> s)" |
|
114 |
apply (simp (no_asm) add: subst_eq_iff) |
|
115 |
done |
|
116 |
||
117 |
lemma subst_cong: |
|
118 |
"[| theta =$= theta1; sigma =$= sigma1|] |
|
119 |
==> (theta <> sigma) =$= (theta1 <> sigma1)" |
|
120 |
by (simp add: subst_eq_def) |
|
121 |
||
122 |
||
123 |
lemma Cons_trivial: "(w, Var(w) <| s) # s =$= s" |
|
124 |
apply (simp add: subst_eq_iff) |
|
125 |
apply (rule allI) |
|
126 |
apply (induct_tac "t", simp_all) |
|
127 |
done |
|
128 |
||
129 |
||
130 |
lemma comp_subst_subst: "q <> r =$= s ==> t <| q <| r = t <| s" |
|
131 |
by (simp add: subst_eq_iff) |
|
132 |
||
133 |
||
134 |
subsection{*Domain and range of Substitutions*} |
|
135 |
||
136 |
lemma sdom_iff: "(v : sdom(s)) = (Var(v) <| s ~= Var(v))" |
|
137 |
apply (induct "s") |
|
138 |
apply (case_tac [2] a, auto) |
|
139 |
done |
|
140 |
||
141 |
||
142 |
lemma srange_iff: |
|
143 |
"v : srange(s) = (\<exists>w. w : sdom(s) & v : vars_of(Var(w) <| s))" |
|
144 |
by (auto simp add: srange_def) |
|
145 |
||
146 |
lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)" |
|
147 |
by (unfold empty_def, blast) |
|
148 |
||
149 |
lemma invariance: "(t <| s = t) = (sdom(s) Int vars_of(t) = {})" |
|
150 |
apply (induct_tac "t") |
|
151 |
apply (auto simp add: empty_iff_all_not sdom_iff) |
|
152 |
done |
|
153 |
||
154 |
lemma Var_in_srange [rule_format]: |
|
155 |
"v : sdom(s) --> v : vars_of(t <| s) --> v : srange(s)" |
|
156 |
apply (induct_tac "t") |
|
157 |
apply (case_tac "a : sdom (s) ") |
|
158 |
apply (auto simp add: sdom_iff srange_iff) |
|
159 |
done |
|
160 |
||
161 |
lemma Var_elim: "[| v : sdom(s); v ~: srange(s) |] ==> v ~: vars_of(t <| s)" |
|
162 |
by (blast intro: Var_in_srange) |
|
163 |
||
164 |
lemma Var_intro [rule_format]: |
|
165 |
"v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)" |
|
166 |
apply (induct_tac "t") |
|
167 |
apply (auto simp add: sdom_iff srange_iff) |
|
168 |
apply (rule_tac x=a in exI, auto) |
|
169 |
done |
|
170 |
||
171 |
lemma srangeD [rule_format]: |
|
172 |
"v : srange(s) --> (\<exists>w. w : sdom(s) & v : vars_of(Var(w) <| s))" |
|
173 |
apply (simp (no_asm) add: srange_iff) |
|
174 |
done |
|
175 |
||
176 |
lemma dom_range_disjoint: |
|
177 |
"sdom(s) Int srange(s) = {} = (\<forall>t. sdom(s) Int vars_of(t <| s) = {})" |
|
178 |
apply (simp (no_asm) add: empty_iff_all_not) |
|
179 |
apply (force intro: Var_in_srange dest: srangeD) |
|
180 |
done |
|
181 |
||
182 |
lemma subst_not_empty: "~ u <| s = u ==> (\<exists>x. x : sdom(s))" |
|
183 |
by (auto simp add: empty_iff_all_not invariance) |
|
184 |
||
185 |
||
186 |
lemma id_subst_lemma [simp]: "(M <| [(x, Var x)]) = M" |
|
187 |
by (induct_tac "M", auto) |
|
188 |
||
189 |
||
968 | 190 |
end |