src/HOL/Subst/Subst.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 5278 a903b66822e2
permissions -rw-r--r--
import -> imports
paulson@3268
     1
(*  Title:      HOL/Subst/Subst.ML
clasohm@1266
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     4
    Copyright   1993  University of Cambridge
clasohm@968
     5
paulson@3268
     6
Substitutions on uterms
clasohm@968
     7
*)
clasohm@968
     8
clasohm@968
     9
open Subst;
clasohm@968
    10
clasohm@968
    11
clasohm@968
    12
(**** Substitutions ****)
clasohm@968
    13
wenzelm@5069
    14
Goal "t <| [] = t";
paulson@3192
    15
by (induct_tac "t" 1);
paulson@3192
    16
by (ALLGOALS Asm_simp_tac);
clasohm@968
    17
qed "subst_Nil";
clasohm@968
    18
paulson@3192
    19
Addsimps [subst_Nil];
paulson@3192
    20
wenzelm@5069
    21
Goal "t <: u --> t <| s <: u <| s";
paulson@3192
    22
by (induct_tac "u" 1);
paulson@3192
    23
by (ALLGOALS Asm_simp_tac);
paulson@3192
    24
qed_spec_mp "subst_mono";
clasohm@968
    25
wenzelm@5069
    26
Goal  "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s";
paulson@3192
    27
by (case_tac "t = Var(v)" 1);
paulson@3457
    28
by (etac rev_mp 2);
clasohm@968
    29
by (res_inst_tac [("P",
clasohm@972
    30
    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")]
paulson@3192
    31
    uterm.induct 2);
paulson@3192
    32
by (ALLGOALS Asm_simp_tac);
paulson@3192
    33
by (Blast_tac 1);
paulson@3192
    34
qed_spec_mp "Var_not_occs";
clasohm@968
    35
paulson@5278
    36
Goal "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
paulson@3192
    37
by (induct_tac "t" 1);
paulson@3192
    38
by (ALLGOALS Asm_full_simp_tac);
paulson@3192
    39
by (ALLGOALS Blast_tac);
clasohm@968
    40
qed "agreement";
clasohm@968
    41
wenzelm@5069
    42
Goal   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
nipkow@4686
    43
by (simp_tac (simpset() addsimps [agreement]) 1);
paulson@3192
    44
qed_spec_mp"repl_invariance";
clasohm@968
    45
clasohm@968
    46
val asms = goal Subst.thy 
clasohm@972
    47
     "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)";
paulson@3192
    48
by (induct_tac "t" 1);
paulson@3192
    49
by (ALLGOALS Asm_simp_tac);
paulson@3192
    50
qed_spec_mp"Var_in_subst";
paulson@3192
    51
clasohm@968
    52
clasohm@968
    53
(**** Equality between Substitutions ****)
clasohm@968
    54
wenzelm@5069
    55
Goalw [subst_eq_def] "r =$= s = (! t. t <| r = t <| s)";
paulson@3192
    56
by (Simp_tac 1);
clasohm@968
    57
qed "subst_eq_iff";
clasohm@968
    58
paulson@3192
    59
paulson@3192
    60
local fun prove s = prove_goal Subst.thy s
clasohm@968
    61
                  (fn prems => [cut_facts_tac prems 1,
clasohm@968
    62
                                REPEAT (etac rev_mp 1),
wenzelm@4089
    63
                                simp_tac (simpset() addsimps [subst_eq_iff]) 1])
clasohm@968
    64
in 
paulson@3192
    65
  val subst_refl      = prove "r =$= r";
paulson@3192
    66
  val subst_sym       = prove "r =$= s ==> s =$= r";
paulson@3192
    67
  val subst_trans     = prove "[| q =$= r; r =$= s |] ==> q =$= s";
clasohm@968
    68
end;
clasohm@968
    69
paulson@3192
    70
paulson@3192
    71
AddIffs [subst_refl];
paulson@3192
    72
paulson@3192
    73
clasohm@968
    74
val eq::prems = goalw Subst.thy [subst_eq_def] 
paulson@3192
    75
    "[| r =$= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)";
clasohm@968
    76
by (resolve_tac [eq RS spec RS subst] 1);
clasohm@968
    77
by (resolve_tac (prems RL [eq RS spec RS subst]) 1);
clasohm@968
    78
qed "subst_subst2";
clasohm@968
    79
clasohm@968
    80
val ssubst_subst2 = subst_sym RS subst_subst2;
clasohm@968
    81
clasohm@968
    82
(**** Composition of Substitutions ****)
clasohm@968
    83
paulson@3192
    84
let fun prove s = 
paulson@3192
    85
 prove_goalw Subst.thy [comp_def,sdom_def] s (fn _ => [Simp_tac 1])
paulson@3192
    86
in 
paulson@3192
    87
Addsimps
paulson@3192
    88
 (
paulson@3192
    89
   map prove 
paulson@3192
    90
   [ "[] <> bl = bl",
paulson@3192
    91
     "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)",
paulson@3192
    92
     "sdom([]) = {}",
paulson@3192
    93
     "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"]
paulson@3192
    94
 )
paulson@3192
    95
end;
paulson@3192
    96
paulson@3192
    97
wenzelm@5069
    98
Goal "s <> [] = s";
clasohm@968
    99
by (alist_ind_tac "s" 1);
paulson@3192
   100
by (ALLGOALS Asm_simp_tac);
clasohm@968
   101
qed "comp_Nil";
clasohm@968
   102
paulson@3192
   103
Addsimps [comp_Nil];
paulson@3192
   104
wenzelm@5069
   105
Goal "s =$= s <> []";
paulson@3192
   106
by (Simp_tac 1);
paulson@3192
   107
qed "subst_comp_Nil";
paulson@3192
   108
wenzelm@5069
   109
Goal "(t <| r <> s) = (t <| r <| s)";
paulson@3192
   110
by (induct_tac "t" 1);
paulson@3192
   111
by (ALLGOALS Asm_simp_tac);
clasohm@968
   112
by (alist_ind_tac "r" 1);
nipkow@4686
   113
by (ALLGOALS Asm_simp_tac);
clasohm@968
   114
qed "subst_comp";
clasohm@968
   115
paulson@3192
   116
Addsimps [subst_comp];
paulson@3192
   117
wenzelm@5069
   118
Goal "(q <> r) <> s =$= q <> (r <> s)";
wenzelm@4089
   119
by (simp_tac (simpset() addsimps [subst_eq_iff]) 1);
clasohm@968
   120
qed "comp_assoc";
clasohm@968
   121
nipkow@5119
   122
Goal "[| theta =$= theta1; sigma =$= sigma1|] ==> \
nipkow@5119
   123
\     (theta <> sigma) =$= (theta1 <> sigma1)";
wenzelm@4089
   124
by (asm_full_simp_tac (simpset() addsimps [subst_eq_def]) 1);
paulson@3192
   125
qed "subst_cong";
paulson@3192
   126
paulson@3192
   127
wenzelm@5069
   128
Goal "(w, Var(w) <| s) # s =$= s"; 
wenzelm@4089
   129
by (simp_tac (simpset() addsimps [subst_eq_iff]) 1);
paulson@3192
   130
by (rtac allI 1);
paulson@3192
   131
by (induct_tac "t" 1);
nipkow@4686
   132
by (ALLGOALS Asm_full_simp_tac);
clasohm@968
   133
qed "Cons_trivial";
clasohm@968
   134
paulson@3192
   135
nipkow@5119
   136
Goal "q <> r =$= s ==>  t <| q <| r = t <| s";
wenzelm@4089
   137
by (asm_full_simp_tac (simpset() addsimps [subst_eq_iff]) 1);
clasohm@968
   138
qed "comp_subst_subst";
clasohm@968
   139
paulson@3192
   140
clasohm@968
   141
(****  Domain and range of Substitutions ****)
clasohm@968
   142
wenzelm@5069
   143
Goal  "(v : sdom(s)) = (Var(v) <| s ~= Var(v))";
clasohm@968
   144
by (alist_ind_tac "s" 1);
nipkow@4686
   145
by (ALLGOALS Asm_simp_tac);
paulson@3192
   146
by (Blast_tac 1);
clasohm@968
   147
qed "sdom_iff";
clasohm@968
   148
paulson@3192
   149
wenzelm@5069
   150
Goalw [srange_def]  
wenzelm@3842
   151
   "v : srange(s) = (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
paulson@3192
   152
by (Blast_tac 1);
clasohm@968
   153
qed "srange_iff";
clasohm@968
   154
wenzelm@5069
   155
Goalw [empty_def] "(A = {}) = (ALL a.~ a:A)";
paulson@3192
   156
by (Blast_tac 1);
paulson@3192
   157
qed "empty_iff_all_not";
paulson@3192
   158
wenzelm@5069
   159
Goal  "(t <| s = t) = (sdom(s) Int vars_of(t) = {})";
paulson@3192
   160
by (induct_tac "t" 1);
paulson@3192
   161
by (ALLGOALS
wenzelm@4089
   162
    (asm_full_simp_tac (simpset() addsimps [empty_iff_all_not, sdom_iff])));
paulson@3192
   163
by (ALLGOALS Blast_tac);
clasohm@968
   164
qed "invariance";
clasohm@968
   165
wenzelm@5069
   166
Goal  "v : sdom(s) -->  v : vars_of(t <| s) --> v : srange(s)";
paulson@3192
   167
by (induct_tac "t" 1);
paulson@3192
   168
by (case_tac "a : sdom(s)" 1);
wenzelm@4089
   169
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff, srange_iff])));
paulson@3192
   170
by (ALLGOALS Blast_tac);
paulson@3192
   171
qed_spec_mp "Var_in_srange";
clasohm@968
   172
paulson@5278
   173
Goal "[| v : sdom(s); v ~: srange(s) |] ==>  v ~: vars_of(t <| s)";
wenzelm@4089
   174
by (blast_tac (claset() addIs [Var_in_srange]) 1);
paulson@3192
   175
qed "Var_elim";
clasohm@968
   176
paulson@5278
   177
Goal "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
paulson@3192
   178
by (induct_tac "t" 1);
wenzelm@4089
   179
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff,srange_iff])));
paulson@3192
   180
by (Blast_tac 2);
wenzelm@4089
   181
by (safe_tac (claset() addSIs [exI, vars_var_iff RS iffD1 RS sym]));
paulson@4477
   182
by Auto_tac;
paulson@3192
   183
qed_spec_mp "Var_intro";
clasohm@968
   184
paulson@5278
   185
Goal "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
wenzelm@4089
   186
by (simp_tac (simpset() addsimps [srange_iff]) 1);
paulson@3192
   187
qed_spec_mp "srangeD";
clasohm@968
   188
paulson@5278
   189
Goal "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})";
wenzelm@4089
   190
by (simp_tac (simpset() addsimps [empty_iff_all_not]) 1);
wenzelm@4089
   191
by (fast_tac (claset() addIs [Var_in_srange] addDs [srangeD]) 1);
clasohm@968
   192
qed "dom_range_disjoint";
clasohm@968
   193
nipkow@5119
   194
Goal "~ u <| s = u ==> (? x. x : sdom(s))";
wenzelm@4089
   195
by (full_simp_tac (simpset() addsimps [empty_iff_all_not, invariance]) 1);
paulson@3192
   196
by (Blast_tac 1);
paulson@3192
   197
qed "subst_not_empty";
paulson@3192
   198
paulson@3192
   199
wenzelm@5069
   200
Goal "(M <| [(x, Var x)]) = M";
paulson@3192
   201
by (induct_tac "M" 1);
nipkow@4686
   202
by (ALLGOALS Asm_simp_tac);
paulson@3192
   203
qed "id_subst_lemma";
paulson@3192
   204
paulson@3192
   205
Addsimps [id_subst_lemma];