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