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