src/HOL/Subst/Subst.ML
author paulson
Wed May 21 10:54:10 1997 +0200 (1997-05-21)
changeset 3268 012c43174664
parent 3192 a75558a4ed37
child 3457 a8ab7c64817c
permissions -rw-r--r--
Mostly cosmetic changes: updated headers, ID lines, etc.
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
clasohm@968
    14
goal Subst.thy "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
clasohm@968
    21
goal Subst.thy "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
paulson@3192
    26
goal Subst.thy  "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s";
paulson@3192
    27
by (case_tac "t = Var(v)" 1);
paulson@3192
    28
be 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
clasohm@968
    36
goal Subst.thy
clasohm@968
    37
    "(t <|r = t <|s) = (! v.v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
paulson@3192
    38
by (induct_tac "t" 1);
paulson@3192
    39
by (ALLGOALS Asm_full_simp_tac);
paulson@3192
    40
by (ALLGOALS Blast_tac);
clasohm@968
    41
qed "agreement";
clasohm@968
    42
clasohm@972
    43
goal Subst.thy   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
paulson@3192
    44
by(simp_tac (!simpset addsimps [agreement]
paulson@3192
    45
                      setloop (split_tac [expand_if])) 1);
paulson@3192
    46
qed_spec_mp"repl_invariance";
clasohm@968
    47
clasohm@968
    48
val asms = goal Subst.thy 
clasohm@972
    49
     "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)";
paulson@3192
    50
by (induct_tac "t" 1);
paulson@3192
    51
by (ALLGOALS Asm_simp_tac);
paulson@3192
    52
qed_spec_mp"Var_in_subst";
paulson@3192
    53
clasohm@968
    54
clasohm@968
    55
(**** Equality between Substitutions ****)
clasohm@968
    56
paulson@3192
    57
goalw Subst.thy [subst_eq_def] "r =$= s = (! t.t <| r = t <| s)";
paulson@3192
    58
by (Simp_tac 1);
clasohm@968
    59
qed "subst_eq_iff";
clasohm@968
    60
paulson@3192
    61
paulson@3192
    62
local fun prove s = prove_goal Subst.thy s
clasohm@968
    63
                  (fn prems => [cut_facts_tac prems 1,
clasohm@968
    64
                                REPEAT (etac rev_mp 1),
paulson@3192
    65
                                simp_tac (!simpset addsimps [subst_eq_iff]) 1])
clasohm@968
    66
in 
paulson@3192
    67
  val subst_refl      = prove "r =$= r";
paulson@3192
    68
  val subst_sym       = prove "r =$= s ==> s =$= r";
paulson@3192
    69
  val subst_trans     = prove "[| q =$= r; r =$= s |] ==> q =$= s";
clasohm@968
    70
end;
clasohm@968
    71
paulson@3192
    72
paulson@3192
    73
AddIffs [subst_refl];
paulson@3192
    74
paulson@3192
    75
clasohm@968
    76
val eq::prems = goalw Subst.thy [subst_eq_def] 
paulson@3192
    77
    "[| r =$= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)";
clasohm@968
    78
by (resolve_tac [eq RS spec RS subst] 1);
clasohm@968
    79
by (resolve_tac (prems RL [eq RS spec RS subst]) 1);
clasohm@968
    80
qed "subst_subst2";
clasohm@968
    81
clasohm@968
    82
val ssubst_subst2 = subst_sym RS subst_subst2;
clasohm@968
    83
clasohm@968
    84
(**** Composition of Substitutions ****)
clasohm@968
    85
paulson@3192
    86
let fun prove s = 
paulson@3192
    87
 prove_goalw Subst.thy [comp_def,sdom_def] s (fn _ => [Simp_tac 1])
paulson@3192
    88
in 
paulson@3192
    89
Addsimps
paulson@3192
    90
 (
paulson@3192
    91
   map prove 
paulson@3192
    92
   [ "[] <> bl = bl",
paulson@3192
    93
     "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)",
paulson@3192
    94
     "sdom([]) = {}",
paulson@3192
    95
     "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"]
paulson@3192
    96
 )
paulson@3192
    97
end;
paulson@3192
    98
paulson@3192
    99
clasohm@968
   100
goal Subst.thy "s <> [] = s";
clasohm@968
   101
by (alist_ind_tac "s" 1);
paulson@3192
   102
by (ALLGOALS Asm_simp_tac);
clasohm@968
   103
qed "comp_Nil";
clasohm@968
   104
paulson@3192
   105
Addsimps [comp_Nil];
paulson@3192
   106
paulson@3192
   107
goal Subst.thy "s =$= s <> []";
paulson@3192
   108
by (Simp_tac 1);
paulson@3192
   109
qed "subst_comp_Nil";
paulson@3192
   110
clasohm@968
   111
goal Subst.thy "(t <| r <> s) = (t <| r <| s)";
paulson@3192
   112
by (induct_tac "t" 1);
paulson@3192
   113
by (ALLGOALS Asm_simp_tac);
clasohm@968
   114
by (alist_ind_tac "r" 1);
paulson@3192
   115
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
clasohm@968
   116
qed "subst_comp";
clasohm@968
   117
paulson@3192
   118
Addsimps [subst_comp];
paulson@3192
   119
paulson@3192
   120
goal Subst.thy "(q <> r) <> s =$= q <> (r <> s)";
paulson@3192
   121
by (simp_tac (!simpset addsimps [subst_eq_iff]) 1);
clasohm@968
   122
qed "comp_assoc";
clasohm@968
   123
paulson@3192
   124
goal Subst.thy "!!s. [| theta =$= theta1; sigma =$= sigma1|] ==> \
paulson@3192
   125
             \       (theta <> sigma) =$= (theta1 <> sigma1)";
paulson@3192
   126
by (asm_full_simp_tac (!simpset addsimps [subst_eq_def]) 1);
paulson@3192
   127
qed "subst_cong";
paulson@3192
   128
paulson@3192
   129
paulson@3192
   130
goal Subst.thy "(w, Var(w) <| s) # s =$= s"; 
paulson@3192
   131
by (simp_tac (!simpset addsimps [subst_eq_iff]) 1);
paulson@3192
   132
by (rtac allI 1);
paulson@3192
   133
by (induct_tac "t" 1);
paulson@3192
   134
by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac [expand_if]))));
clasohm@968
   135
qed "Cons_trivial";
clasohm@968
   136
paulson@3192
   137
paulson@3192
   138
goal Subst.thy "!!s. q <> r =$= s ==>  t <| q <| r = t <| s";
paulson@3192
   139
by (asm_full_simp_tac (!simpset addsimps [subst_eq_iff]) 1);
clasohm@968
   140
qed "comp_subst_subst";
clasohm@968
   141
paulson@3192
   142
clasohm@968
   143
(****  Domain and range of Substitutions ****)
clasohm@968
   144
paulson@3192
   145
goal Subst.thy  "(v : sdom(s)) = (Var(v) <| s ~= Var(v))";
clasohm@968
   146
by (alist_ind_tac "s" 1);
paulson@3192
   147
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
paulson@3192
   148
by (Blast_tac 1);
clasohm@968
   149
qed "sdom_iff";
clasohm@968
   150
paulson@3192
   151
clasohm@968
   152
goalw Subst.thy [srange_def]  
clasohm@968
   153
   "v : srange(s) = (? w.w : sdom(s) & v : vars_of(Var(w) <| s))";
paulson@3192
   154
by (Blast_tac 1);
clasohm@968
   155
qed "srange_iff";
clasohm@968
   156
paulson@3192
   157
goalw Set.thy [empty_def] "(A = {}) = (ALL a.~ a:A)";
paulson@3192
   158
by (Blast_tac 1);
paulson@3192
   159
qed "empty_iff_all_not";
paulson@3192
   160
clasohm@968
   161
goal Subst.thy  "(t <| s = t) = (sdom(s) Int vars_of(t) = {})";
paulson@3192
   162
by (induct_tac "t" 1);
paulson@3192
   163
by (ALLGOALS
paulson@3192
   164
    (asm_full_simp_tac (!simpset addsimps [empty_iff_all_not, sdom_iff])));
paulson@3192
   165
by (ALLGOALS Blast_tac);
clasohm@968
   166
qed "invariance";
clasohm@968
   167
paulson@3192
   168
goal Subst.thy  "v : sdom(s) -->  v : vars_of(t <| s) --> v : srange(s)";
paulson@3192
   169
by (induct_tac "t" 1);
paulson@3192
   170
by (case_tac "a : sdom(s)" 1);
paulson@3192
   171
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [sdom_iff, srange_iff])));
paulson@3192
   172
by (ALLGOALS Blast_tac);
paulson@3192
   173
qed_spec_mp "Var_in_srange";
clasohm@968
   174
paulson@3192
   175
goal Subst.thy 
paulson@3192
   176
     "!!v. [| v : sdom(s); v ~: srange(s) |] ==>  v ~: vars_of(t <| s)";
paulson@3192
   177
by (blast_tac (!claset addIs [Var_in_srange]) 1);
paulson@3192
   178
qed "Var_elim";
clasohm@968
   179
clasohm@968
   180
goal Subst.thy  "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
paulson@3192
   181
by (induct_tac "t" 1);
paulson@3192
   182
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [sdom_iff,srange_iff])));
paulson@3192
   183
by (Blast_tac 2);
paulson@3192
   184
by (REPEAT (step_tac (!claset addIs [vars_var_iff RS iffD1 RS sym]) 1));
paulson@3192
   185
by (Auto_tac());
paulson@3192
   186
qed_spec_mp "Var_intro";
clasohm@968
   187
clasohm@968
   188
goal Subst.thy
clasohm@968
   189
    "v : srange(s) --> (? w.w : sdom(s) & v : vars_of(Var(w) <| s))";
paulson@3192
   190
by (simp_tac (!simpset addsimps [srange_iff]) 1);
paulson@3192
   191
qed_spec_mp "srangeD";
clasohm@968
   192
paulson@3192
   193
goal Subst.thy
clasohm@968
   194
   "sdom(s) Int srange(s) = {} = (! t.sdom(s) Int vars_of(t <| s) = {})";
paulson@3192
   195
by (simp_tac (!simpset addsimps [empty_iff_all_not]) 1);
paulson@3192
   196
by (fast_tac (!claset addIs [Var_in_srange] addDs [srangeD]) 1);
clasohm@968
   197
qed "dom_range_disjoint";
clasohm@968
   198
paulson@3192
   199
goal Subst.thy "!!u. ~ u <| s = u ==> (? x. x : sdom(s))";
paulson@3192
   200
by (full_simp_tac (!simpset addsimps [empty_iff_all_not, invariance]) 1);
paulson@3192
   201
by (Blast_tac 1);
paulson@3192
   202
qed "subst_not_empty";
paulson@3192
   203
paulson@3192
   204
paulson@3192
   205
goal Subst.thy "(M <| [(x, Var x)]) = M";
paulson@3192
   206
by (induct_tac "M" 1);
paulson@3192
   207
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
paulson@3192
   208
qed "id_subst_lemma";
paulson@3192
   209
paulson@3192
   210
Addsimps [id_subst_lemma];