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