src/HOL/Subst/Subst.thy
author wenzelm
Tue Aug 03 18:52:42 2010 +0200 (2010-08-03)
changeset 38140 05691ad74079
parent 25382 72cfe89f7b21
permissions -rw-r--r--
modernized specifications;
tuned headers;
     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