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