src/HOL/Subst/Subst.thy
 author haftmann Fri Jan 02 08:12:46 2009 +0100 (2009-01-02) changeset 29332 edc1e2a56398 parent 25382 72cfe89f7b21 child 38140 05691ad74079 permissions -rw-r--r--
named code theorem for Fract_norm
```     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
```