src/HOL/Subst/Subst.thy
 author hoelzl Tue Jan 18 21:37:23 2011 +0100 (2011-01-18) changeset 41654 32fe42892983 parent 38140 05691ad74079 permissions -rw-r--r--
Gauge measure removed
```     1 (*  Title:      HOL/Subst/Subst.thy
```
```     2     Author:     Martin Coen, Cambridge University Computer Laboratory
```
```     3     Copyright   1993  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 header {* Substitutions on uterms *}
```
```     7
```
```     8 theory Subst
```
```     9 imports AList UTerm
```
```    10 begin
```
```    11
```
```    12 primrec
```
```    13   subst :: "'a uterm => ('a * 'a uterm) list => 'a uterm"  (infixl "<|" 55)
```
```    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
```
```    19 notation (xsymbols)
```
```    20   subst  (infixl "\<lhd>" 55)
```
```    21
```
```    22 definition
```
```    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
```
```    26 notation (xsymbols)
```
```    27   subst_eq  (infixr "\<doteq>" 52)
```
```    28
```
```    29 definition
```
```    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
```
```    34 notation (xsymbols)
```
```    35   comp  (infixl "\<lozenge>" 56)
```
```    36
```
```    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)})"
```
```    44
```
```    45
```
```    46
```
```    47 subsection {* Basic Laws *}
```
```    48
```
```    49 lemma subst_Nil [simp]: "t \<lhd> [] = t"
```
```    50   by (induct t) auto
```
```    51
```
```    52 lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
```
```    53   by (induct u) auto
```
```    54
```
```    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)+
```
```    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)
```
```    61      apply auto
```
```    62   done
```
```    63
```
```    64 lemma agreement: "(t\<lhd>r = t\<lhd>s) = (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
```
```    65   by (induct t) auto
```
```    66
```
```    67 lemma repl_invariance: "~ v: vars_of t ==> t \<lhd> (v,u)#s = t \<lhd> s"
```
```    68   by (simp add: agreement)
```
```    69
```
```    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
```
```    73
```
```    74
```
```    75 subsection{*Equality between Substitutions*}
```
```    76
```
```    77 lemma subst_eq_iff: "r \<doteq> s = (\<forall>t. t \<lhd> r = t \<lhd> s)"
```
```    78   by (simp add: subst_eq_def)
```
```    79
```
```    80 lemma subst_refl [iff]: "r \<doteq> r"
```
```    81   by (simp add: subst_eq_iff)
```
```    82
```
```    83 lemma subst_sym: "r \<doteq> s ==> s \<doteq> r"
```
```    84   by (simp add: subst_eq_iff)
```
```    85
```
```    86 lemma subst_trans: "[| q \<doteq> r; r \<doteq> s |] ==> q \<doteq> s"
```
```    87   by (simp add: subst_eq_iff)
```
```    88
```
```    89 lemma subst_subst2:
```
```    90     "[| r \<doteq> s; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
```
```    91   by (simp add: subst_eq_def)
```
```    92
```
```    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)
```
```    96
```
```    97
```
```    98 subsection{*Composition of Substitutions*}
```
```    99
```
```   100 lemma [simp]:
```
```   101      "[] \<lozenge> bl = bl"
```
```   102      "((a,b)#al) \<lozenge> bl = (a,b \<lhd> bl) # (al \<lozenge> bl)"
```
```   103      "sdom([]) = {}"
```
```   104      "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"
```
```   105   by (simp_all add: comp_def sdom_def)
```
```   106
```
```   107 lemma comp_Nil [simp]: "s \<lozenge> [] = s"
```
```   108   by (induct s) auto
```
```   109
```
```   110 lemma subst_comp_Nil: "s \<doteq> s \<lozenge> []"
```
```   111   by simp
```
```   112
```
```   113 lemma subst_comp [simp]: "(t \<lhd> r \<lozenge> s) = (t \<lhd> r \<lhd> s)"
```
```   114   apply (induct t)
```
```   115   apply simp_all
```
```   116   apply (induct r)
```
```   117    apply auto
```
```   118   done
```
```   119
```
```   120 lemma comp_assoc: "(q \<lozenge> r) \<lozenge> s \<doteq> q \<lozenge> (r \<lozenge> s)"
```
```   121   by (simp add: subst_eq_iff)
```
```   122
```
```   123 lemma subst_cong:
```
```   124   "[| theta \<doteq> theta1; sigma \<doteq> sigma1|]
```
```   125     ==> (theta \<lozenge> sigma) \<doteq> (theta1 \<lozenge> sigma1)"
```
```   126   by (simp add: subst_eq_def)
```
```   127
```
```   128
```
```   129 lemma Cons_trivial: "(w, Var(w) \<lhd> s) # s \<doteq> s"
```
```   130   apply (simp add: subst_eq_iff)
```
```   131   apply (rule allI)
```
```   132   apply (induct_tac t)
```
```   133     apply simp_all
```
```   134   done
```
```   135
```
```   136
```
```   137 lemma comp_subst_subst: "q \<lozenge> r \<doteq> s ==>  t \<lhd> q \<lhd> r = t \<lhd> s"
```
```   138   by (simp add: subst_eq_iff)
```
```   139
```
```   140
```
```   141 subsection{*Domain and range of Substitutions*}
```
```   142
```
```   143 lemma sdom_iff: "(v \<in> sdom(s)) = (Var(v) \<lhd> s ~= Var(v))"
```
```   144   apply (induct s)
```
```   145    apply (case_tac [2] a)
```
```   146    apply auto
```
```   147   done
```
```   148
```
```   149
```
```   150 lemma srange_iff:
```
```   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)
```
```   153
```
```   154 lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)"
```
```   155   unfolding empty_def by blast
```
```   156
```
```   157 lemma invariance: "(t \<lhd> s = t) = (sdom(s) Int vars_of(t) = {})"
```
```   158   apply (induct t)
```
```   159     apply (auto simp add: empty_iff_all_not sdom_iff)
```
```   160   done
```
```   161
```
```   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
```
```   168
```
```   169 lemma Var_elim: "[| v \<in> sdom(s); v \<notin> srange(s) |] ==>  v \<notin> vars_of(t \<lhd> s)"
```
```   170   by (blast intro: Var_in_srange)
```
```   171
```
```   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
```
```   179
```
```   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)
```
```   182
```
```   183 lemma dom_range_disjoint:
```
```   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
```
```   188
```
```   189 lemma subst_not_empty: "~ u \<lhd> s = u ==> (\<exists>x. x \<in> sdom(s))"
```
```   190   by (auto simp add: empty_iff_all_not invariance)
```
```   191
```
```   192
```
```   193 lemma id_subst_lemma [simp]: "(M \<lhd> [(x, Var x)]) = M"
```
```   194   by (induct M) auto
```
```   195
```
```   196 end
```