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