author | haftmann |
Tue, 10 Jul 2007 09:24:43 +0200 | |
changeset 23693 | d92637b15a45 |
parent 15648 | f6da795ee27a |
child 24823 | bfb619994060 |
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 |
||
15648 | 23 |
syntax (xsymbols) |
24 |
"op =$=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" |
|
25 |
(infixr "\<doteq>" 52) |
|
26 |
"op <|" :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl "\<lhd>" 55) |
|
27 |
"op <>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] |
|
28 |
=> ('a*('a uterm)) list" (infixl "\<lozenge>" 56) |
|
29 |
||
30 |
||
5184 | 31 |
primrec |
15648 | 32 |
subst_Var: "(Var v \<lhd> s) = assoc v (Var v) s" |
33 |
subst_Const: "(Const c \<lhd> s) = Const c" |
|
34 |
subst_Comb: "(Comb M N \<lhd> s) = Comb (M \<lhd> s) (N \<lhd> s)" |
|
968 | 35 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
36 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
37 |
defs |
968 | 38 |
|
15648 | 39 |
subst_eq_def: "r =$= s == ALL t. t \<lhd> r = t \<lhd> s" |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
40 |
|
15648 | 41 |
comp_def: "al \<lozenge> bl == alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)" |
968 | 42 |
|
15635 | 43 |
sdom_def: |
1151 | 44 |
"sdom(al) == alist_rec al {} |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
45 |
(%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
|
46 |
|
15635 | 47 |
srange_def: |
15648 | 48 |
"srange(al) == Union({y. \<exists>x \<in> sdom(al). y = vars_of(Var(x) \<lhd> al)})" |
968 | 49 |
|
15635 | 50 |
|
51 |
||
52 |
subsection{*Basic Laws*} |
|
53 |
||
15648 | 54 |
lemma subst_Nil [simp]: "t \<lhd> [] = t" |
15635 | 55 |
by (induct_tac "t", auto) |
56 |
||
15648 | 57 |
lemma subst_mono [rule_format]: "t \<prec> u --> t \<lhd> s \<prec> u \<lhd> s" |
15635 | 58 |
by (induct_tac "u", auto) |
59 |
||
60 |
lemma Var_not_occs [rule_format]: |
|
15648 | 61 |
"~ (Var(v) \<prec> t) --> t \<lhd> (v,t \<lhd> s) # s = t \<lhd> s" |
15635 | 62 |
apply (case_tac "t = Var v") |
63 |
apply (erule_tac [2] rev_mp) |
|
15648 | 64 |
apply (rule_tac [2] P = |
65 |
"%x. x \<noteq> Var v --> ~(Var v \<prec> x) --> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s" |
|
66 |
in uterm.induct) |
|
15635 | 67 |
apply auto |
68 |
done |
|
69 |
||
15648 | 70 |
lemma agreement: "(t\<lhd>r = t\<lhd>s) = (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)" |
15635 | 71 |
by (induct_tac "t", auto) |
72 |
||
15648 | 73 |
lemma repl_invariance: "~ v: vars_of(t) ==> t \<lhd> (v,u)#s = t \<lhd> s" |
15635 | 74 |
by (simp add: agreement) |
75 |
||
76 |
lemma Var_in_subst [rule_format]: |
|
15648 | 77 |
"v \<in> vars_of(t) --> w \<in> vars_of(t \<lhd> (v,Var(w))#s)" |
15635 | 78 |
by (induct_tac "t", auto) |
79 |
||
80 |
||
81 |
subsection{*Equality between Substitutions*} |
|
82 |
||
15648 | 83 |
lemma subst_eq_iff: "r \<doteq> s = (\<forall>t. t \<lhd> r = t \<lhd> s)" |
15635 | 84 |
by (simp add: subst_eq_def) |
85 |
||
15648 | 86 |
lemma subst_refl [iff]: "r \<doteq> r" |
15635 | 87 |
by (simp add: subst_eq_iff) |
88 |
||
15648 | 89 |
lemma subst_sym: "r \<doteq> s ==> s \<doteq> r" |
15635 | 90 |
by (simp add: subst_eq_iff) |
91 |
||
15648 | 92 |
lemma subst_trans: "[| q \<doteq> r; r \<doteq> s |] ==> q \<doteq> s" |
15635 | 93 |
by (simp add: subst_eq_iff) |
94 |
||
95 |
lemma subst_subst2: |
|
15648 | 96 |
"[| r \<doteq> s; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)" |
15635 | 97 |
by (simp add: subst_eq_def) |
98 |
||
99 |
lemmas ssubst_subst2 = subst_sym [THEN subst_subst2] |
|
100 |
||
101 |
||
102 |
subsection{*Composition of Substitutions*} |
|
103 |
||
104 |
lemma [simp]: |
|
15648 | 105 |
"[] \<lozenge> bl = bl" |
106 |
"((a,b)#al) \<lozenge> bl = (a,b \<lhd> bl) # (al \<lozenge> bl)" |
|
15635 | 107 |
"sdom([]) = {}" |
108 |
"sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})" |
|
109 |
by (simp_all add: comp_def sdom_def) |
|
110 |
||
15648 | 111 |
lemma comp_Nil [simp]: "s \<lozenge> [] = s" |
15635 | 112 |
by (induct "s", auto) |
113 |
||
15648 | 114 |
lemma subst_comp_Nil: "s \<doteq> s \<lozenge> []" |
15635 | 115 |
by simp |
116 |
||
15648 | 117 |
lemma subst_comp [simp]: "(t \<lhd> r \<lozenge> s) = (t \<lhd> r \<lhd> s)" |
15635 | 118 |
apply (induct_tac "t") |
119 |
apply (simp_all (no_asm_simp)) |
|
120 |
apply (induct "r", auto) |
|
121 |
done |
|
122 |
||
15648 | 123 |
lemma comp_assoc: "(q \<lozenge> r) \<lozenge> s \<doteq> q \<lozenge> (r \<lozenge> s)" |
124 |
by (simp add: subst_eq_iff) |
|
15635 | 125 |
|
126 |
lemma subst_cong: |
|
15648 | 127 |
"[| theta \<doteq> theta1; sigma \<doteq> sigma1|] |
128 |
==> (theta \<lozenge> sigma) \<doteq> (theta1 \<lozenge> sigma1)" |
|
15635 | 129 |
by (simp add: subst_eq_def) |
130 |
||
131 |
||
15648 | 132 |
lemma Cons_trivial: "(w, Var(w) \<lhd> s) # s \<doteq> s" |
15635 | 133 |
apply (simp add: subst_eq_iff) |
134 |
apply (rule allI) |
|
135 |
apply (induct_tac "t", simp_all) |
|
136 |
done |
|
137 |
||
138 |
||
15648 | 139 |
lemma comp_subst_subst: "q \<lozenge> r \<doteq> s ==> t \<lhd> q \<lhd> r = t \<lhd> s" |
15635 | 140 |
by (simp add: subst_eq_iff) |
141 |
||
142 |
||
143 |
subsection{*Domain and range of Substitutions*} |
|
144 |
||
15648 | 145 |
lemma sdom_iff: "(v \<in> sdom(s)) = (Var(v) \<lhd> s ~= Var(v))" |
15635 | 146 |
apply (induct "s") |
147 |
apply (case_tac [2] a, auto) |
|
148 |
done |
|
149 |
||
150 |
||
151 |
lemma srange_iff: |
|
15648 | 152 |
"v \<in> srange(s) = (\<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s))" |
15635 | 153 |
by (auto simp add: srange_def) |
154 |
||
155 |
lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)" |
|
156 |
by (unfold empty_def, blast) |
|
157 |
||
15648 | 158 |
lemma invariance: "(t \<lhd> s = t) = (sdom(s) Int vars_of(t) = {})" |
15635 | 159 |
apply (induct_tac "t") |
160 |
apply (auto simp add: empty_iff_all_not sdom_iff) |
|
161 |
done |
|
162 |
||
163 |
lemma Var_in_srange [rule_format]: |
|
15648 | 164 |
"v \<in> sdom(s) --> v \<in> vars_of(t \<lhd> s) --> v \<in> srange(s)" |
15635 | 165 |
apply (induct_tac "t") |
15648 | 166 |
apply (case_tac "a \<in> sdom s") |
15635 | 167 |
apply (auto simp add: sdom_iff srange_iff) |
168 |
done |
|
169 |
||
15648 | 170 |
lemma Var_elim: "[| v \<in> sdom(s); v \<notin> srange(s) |] ==> v \<notin> vars_of(t \<lhd> s)" |
15635 | 171 |
by (blast intro: Var_in_srange) |
172 |
||
173 |
lemma Var_intro [rule_format]: |
|
15648 | 174 |
"v \<in> vars_of(t \<lhd> s) --> v \<in> srange(s) | v \<in> vars_of(t)" |
15635 | 175 |
apply (induct_tac "t") |
176 |
apply (auto simp add: sdom_iff srange_iff) |
|
177 |
apply (rule_tac x=a in exI, auto) |
|
178 |
done |
|
179 |
||
15648 | 180 |
lemma srangeD: "v \<in> srange(s) ==> \<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s)" |
181 |
by (simp add: srange_iff) |
|
15635 | 182 |
|
183 |
lemma dom_range_disjoint: |
|
15648 | 184 |
"sdom(s) Int srange(s) = {} = (\<forall>t. sdom(s) Int vars_of(t \<lhd> s) = {})" |
185 |
apply (simp add: empty_iff_all_not) |
|
15635 | 186 |
apply (force intro: Var_in_srange dest: srangeD) |
187 |
done |
|
188 |
||
15648 | 189 |
lemma subst_not_empty: "~ u \<lhd> s = u ==> (\<exists>x. x \<in> sdom(s))" |
15635 | 190 |
by (auto simp add: empty_iff_all_not invariance) |
191 |
||
192 |
||
15648 | 193 |
lemma id_subst_lemma [simp]: "(M \<lhd> [(x, Var x)]) = M" |
15635 | 194 |
by (induct_tac "M", auto) |
195 |
||
196 |
||
968 | 197 |
end |