src/HOL/Subst/Subst.ML
author nipkow
Mon Oct 21 09:50:50 1996 +0200 (1996-10-21)
changeset 2115 9709f9188549
parent 2087 6405a3bb490b
child 3192 a75558a4ed37
permissions -rw-r--r--
Added trans_tac (see Provers/nat_transitive.ML)
     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 For subst.thy.  
     7 *)
     8 
     9 open Subst;
    10 
    11 (***********)
    12 
    13 val subst_defs = [subst_def,comp_def,sdom_def];
    14 
    15 val raw_subst_ss = simpset_of "UTLemmas" addsimps al_rews;
    16 
    17 local fun mk_thm s = prove_goalw Subst.thy subst_defs s 
    18                                  (fn _ => [simp_tac raw_subst_ss 1])
    19 in val subst_rews = map mk_thm 
    20 ["Const(c) <| al = Const(c)",
    21  "Comb t u <| al = Comb (t <| al) (u <| al)",
    22  "[] <> bl = bl",
    23  "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)",
    24  "sdom([]) = {}",
    25  "sdom((a,b)#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \
    26 \                               else (sdom al) Un {a})"
    27 ];
    28    (* This rewrite isn't always desired *)
    29    val Var_subst = mk_thm "Var(x) <| al = assoc x (Var x) al";
    30 end;
    31 
    32 val subst_ss = raw_subst_ss addsimps subst_rews 
    33                             delsimps [de_Morgan_conj, de_Morgan_disj];
    34 
    35 (**** Substitutions ****)
    36 
    37 goal Subst.thy "t <| [] = t";
    38 by (uterm_ind_tac "t" 1);
    39 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
    40 qed "subst_Nil";
    41 
    42 goal Subst.thy "t <: u --> t <| s <: u <| s";
    43 by (uterm_ind_tac "u" 1);
    44 by (ALLGOALS (asm_simp_tac subst_ss));
    45 val subst_mono  = store_thm("subst_mono", result() RS mp);
    46 
    47 goal Subst.thy  "~ (Var(v) <: t) --> t <| (v,t <| s)#s = t <| s";
    48 by (imp_excluded_middle_tac "t = Var(v)" 1);
    49 by (res_inst_tac [("P",
    50     "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")]
    51     uterm_induct 2);
    52 by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst])));
    53 by (fast_tac HOL_cs 1);
    54 val Var_not_occs  = store_thm("Var_not_occs", result() RS mp);
    55 
    56 goal Subst.thy
    57     "(t <|r = t <|s) = (! v.v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
    58 by (uterm_ind_tac "t" 1);
    59 by (REPEAT (etac rev_mp 3));
    60 by (ALLGOALS (asm_simp_tac subst_ss));
    61 by (ALLGOALS (fast_tac HOL_cs));
    62 qed "agreement";
    63 
    64 goal Subst.thy   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
    65 by(simp_tac(subst_ss addsimps [agreement,Var_subst]
    66                      setloop (split_tac [expand_if])) 1);
    67 val repl_invariance  = store_thm("repl_invariance", result() RS mp);
    68 
    69 val asms = goal Subst.thy 
    70      "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)";
    71 by (uterm_ind_tac "t" 1);
    72 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
    73 val Var_in_subst  = store_thm("Var_in_subst", result() RS mp);
    74 
    75 (**** Equality between Substitutions ****)
    76 
    77 goalw Subst.thy [subst_eq_def] "r =s= s = (! t.t <| r = t <| s)";
    78 by (simp_tac subst_ss 1);
    79 qed "subst_eq_iff";
    80 
    81 local fun mk_thm s = prove_goal Subst.thy s
    82                   (fn prems => [cut_facts_tac prems 1,
    83                                 REPEAT (etac rev_mp 1),
    84                                 simp_tac (subst_ss addsimps [subst_eq_iff]) 1])
    85 in 
    86   val subst_refl      = mk_thm "r = s ==> r =s= s";
    87   val subst_sym       = mk_thm "r =s= s ==> s =s= r";
    88   val subst_trans     = mk_thm "[| q =s= r; r =s= s |] ==> q =s= s";
    89 end;
    90 
    91 val eq::prems = goalw Subst.thy [subst_eq_def] 
    92     "[| r =s= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)";
    93 by (resolve_tac [eq RS spec RS subst] 1);
    94 by (resolve_tac (prems RL [eq RS spec RS subst]) 1);
    95 qed "subst_subst2";
    96 
    97 val ssubst_subst2 = subst_sym RS subst_subst2;
    98 
    99 (**** Composition of Substitutions ****)
   100 
   101 goal Subst.thy "s <> [] = s";
   102 by (alist_ind_tac "s" 1);
   103 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [subst_Nil])));
   104 qed "comp_Nil";
   105 
   106 goal Subst.thy "(t <| r <> s) = (t <| r <| s)";
   107 by (uterm_ind_tac "t" 1);
   108 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
   109 by (alist_ind_tac "r" 1);
   110 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst,subst_Nil]
   111                                      setloop (split_tac [expand_if]))));
   112 qed "subst_comp";
   113 
   114 goal Subst.thy "(q <> r) <> s =s= q <> (r <> s)";
   115 by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
   116 qed "comp_assoc";
   117 
   118 goal Subst.thy "(w,Var(w) <| s)#s =s= s"; 
   119 by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
   120 by (uterm_ind_tac "t" 1);
   121 by (REPEAT (etac rev_mp 3));
   122 by (ALLGOALS (simp_tac (subst_ss addsimps[Var_subst]
   123                                  setloop (split_tac [expand_if]))));
   124 qed "Cons_trivial";
   125 
   126 val [prem] = goal Subst.thy "q <> r =s= s ==>  t <| q <| r = t <| s";
   127 by (simp_tac (subst_ss addsimps [prem RS (subst_eq_iff RS iffD1),
   128                                 subst_comp RS sym]) 1);
   129 qed "comp_subst_subst";
   130 
   131 (****  Domain and range of Substitutions ****)
   132 
   133 goal Subst.thy  "(v : sdom(s)) = (~ Var(v) <| s = Var(v))";
   134 by (alist_ind_tac "s" 1);
   135 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst]
   136                             setloop (split_tac[expand_if]))));
   137 by (fast_tac HOL_cs 1);
   138 qed "sdom_iff";
   139 
   140 goalw Subst.thy [srange_def]  
   141    "v : srange(s) = (? w.w : sdom(s) & v : vars_of(Var(w) <| s))";
   142 by (fast_tac set_cs 1);
   143 qed "srange_iff";
   144 
   145 goal Subst.thy  "(t <| s = t) = (sdom(s) Int vars_of(t) = {})";
   146 by (uterm_ind_tac "t" 1);
   147 by (REPEAT (etac rev_mp 3));
   148 by (ALLGOALS (simp_tac (subst_ss addsimps [sdom_iff,Var_subst])));
   149 by (ALLGOALS (fast_tac set_cs));
   150 qed "invariance";
   151 
   152 goal Subst.thy  "v : sdom(s) -->  ~v : srange(s) --> ~v : vars_of(t <| s)";
   153 by (uterm_ind_tac "t" 1);
   154 by (imp_excluded_middle_tac "x : sdom(s)" 1);
   155 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [sdom_iff,srange_iff])));
   156 by (ALLGOALS (fast_tac set_cs));
   157 val Var_elim  = store_thm("Var_elim", result() RS mp RS mp);
   158 
   159 val asms = goal Subst.thy 
   160      "[| v : sdom(s); v : vars_of(t <| s) |] ==>  v : srange(s)";
   161 by (REPEAT (ares_tac (asms @ [Var_elim RS swap RS classical]) 1));
   162 qed "Var_elim2";
   163 
   164 goal Subst.thy  "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
   165 by (uterm_ind_tac "t" 1);
   166 by (REPEAT_SOME (etac rev_mp ));
   167 by (ALLGOALS (simp_tac (subst_ss addsimps [sdom_iff,srange_iff])));
   168 by (REPEAT (step_tac (set_cs addIs [vars_var_iff RS iffD1 RS sym]) 1));
   169 by (etac notE 1);
   170 by (etac subst 1);
   171 by (ALLGOALS (fast_tac set_cs));
   172 val Var_intro  = store_thm("Var_intro", result() RS mp);
   173 
   174 goal Subst.thy
   175     "v : srange(s) --> (? w.w : sdom(s) & v : vars_of(Var(w) <| s))";
   176 by (simp_tac (subst_ss addsimps [srange_iff]) 1);
   177 val srangeE  = store_thm("srangeE", make_elim (result() RS mp));
   178 
   179 val asms = goal Subst.thy
   180    "sdom(s) Int srange(s) = {} = (! t.sdom(s) Int vars_of(t <| s) = {})";
   181 by (simp_tac subst_ss 1);
   182 by (fast_tac (set_cs addIs [Var_elim2] addEs [srangeE]) 1);
   183 qed "dom_range_disjoint";
   184 
   185 val asms = goal Subst.thy "~ u <| s = u --> (? x.x : sdom(s))";
   186 by (simp_tac (subst_ss addsimps [invariance]) 1);
   187 by (fast_tac set_cs 1);
   188 val subst_not_empty  = store_thm("subst_not_empty", result() RS mp);