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