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