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