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