src/HOL/Subst/UTerm.ML
author clasohm
Tue Jan 30 15:24:36 1996 +0100 (1996-01-30)
changeset 1465 5d7a7e439cec
parent 1266 3ae9fe3c0f68
child 1476 608483c2122a
permissions -rw-r--r--
expanded tabs
clasohm@1465
     1
(*  Title:      HOL/Subst/UTerm.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
clasohm@968
     6
Simple term structure for unifiation.
clasohm@968
     7
Binary trees with leaves that are constants or variables.
clasohm@968
     8
*)
clasohm@968
     9
clasohm@968
    10
open UTerm;
clasohm@968
    11
clasohm@968
    12
val uterm_con_defs = [VAR_def, CONST_def, COMB_def];
clasohm@968
    13
clasohm@968
    14
goal UTerm.thy "uterm(A) = A <+> A <+> (uterm(A) <*> uterm(A))";
clasohm@968
    15
let val rew = rewrite_rule uterm_con_defs in  
clasohm@968
    16
by (fast_tac (univ_cs addSIs (equalityI :: map rew uterm.intrs)
clasohm@968
    17
                      addEs [rew uterm.elim]) 1)
clasohm@968
    18
end;
clasohm@968
    19
qed "uterm_unfold";
clasohm@968
    20
clasohm@968
    21
(** the uterm functional **)
clasohm@968
    22
clasohm@968
    23
(*This justifies using uterm in other recursive type definitions*)
clasohm@968
    24
goalw UTerm.thy uterm.defs "!!A B. A<=B ==> uterm(A) <= uterm(B)";
clasohm@968
    25
by (REPEAT (ares_tac (lfp_mono::basic_monos) 1));
clasohm@968
    26
qed "uterm_mono";
clasohm@968
    27
clasohm@968
    28
(** Type checking rules -- uterm creates well-founded sets **)
clasohm@968
    29
clasohm@968
    30
goalw UTerm.thy (uterm_con_defs @ uterm.defs) "uterm(sexp) <= sexp";
clasohm@968
    31
by (rtac lfp_lowerbound 1);
clasohm@968
    32
by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
clasohm@968
    33
qed "uterm_sexp";
clasohm@968
    34
clasohm@968
    35
(* A <= sexp ==> uterm(A) <= sexp *)
clasohm@968
    36
bind_thm ("uterm_subset_sexp", ([uterm_mono, uterm_sexp] MRS subset_trans));
clasohm@968
    37
clasohm@968
    38
(** Induction **)
clasohm@968
    39
clasohm@968
    40
(*Induction for the type 'a uterm *)
clasohm@968
    41
val prems = goalw UTerm.thy [Var_def,Const_def,Comb_def]
clasohm@968
    42
    "[| !!x.P(Var(x));  !!x.P(Const(x));  \
clasohm@968
    43
\       !!u v. [|  P(u);  P(v) |] ==> P(Comb u v) |]  ==> P(t)";
clasohm@968
    44
by (rtac (Rep_uterm_inverse RS subst) 1);   (*types force good instantiation*)
clasohm@968
    45
by (rtac (Rep_uterm RS uterm.induct) 1);
clasohm@968
    46
by (REPEAT (ares_tac prems 1
clasohm@968
    47
     ORELSE eresolve_tac [rangeE, ssubst, Abs_uterm_inverse RS subst] 1));
clasohm@968
    48
qed "uterm_induct";
clasohm@968
    49
clasohm@968
    50
(*Perform induction on xs. *)
clasohm@968
    51
fun uterm_ind_tac a M = 
clasohm@968
    52
    EVERY [res_inst_tac [("t",a)] uterm_induct M,
clasohm@1465
    53
           rename_last_tac a ["1"] (M+1)];
clasohm@968
    54
clasohm@968
    55
clasohm@968
    56
(*** Isomorphisms ***)
clasohm@968
    57
clasohm@968
    58
goal UTerm.thy "inj(Rep_uterm)";
clasohm@968
    59
by (rtac inj_inverseI 1);
clasohm@968
    60
by (rtac Rep_uterm_inverse 1);
clasohm@968
    61
qed "inj_Rep_uterm";
clasohm@968
    62
clasohm@968
    63
goal UTerm.thy "inj_onto Abs_uterm (uterm (range Leaf))";
clasohm@968
    64
by (rtac inj_onto_inverseI 1);
clasohm@968
    65
by (etac Abs_uterm_inverse 1);
clasohm@968
    66
qed "inj_onto_Abs_uterm";
clasohm@968
    67
clasohm@968
    68
(** Distinctness of constructors **)
clasohm@968
    69
clasohm@968
    70
goalw UTerm.thy uterm_con_defs "~ CONST(c) = COMB u v";
clasohm@968
    71
by (rtac notI 1);
clasohm@968
    72
by (etac (In1_inject RS (In0_not_In1 RS notE)) 1);
clasohm@968
    73
qed "CONST_not_COMB";
clasohm@968
    74
bind_thm ("COMB_not_CONST", (CONST_not_COMB RS not_sym));
clasohm@968
    75
bind_thm ("CONST_neq_COMB", (CONST_not_COMB RS notE));
clasohm@968
    76
val COMB_neq_CONST = sym RS CONST_neq_COMB;
clasohm@968
    77
clasohm@968
    78
goalw UTerm.thy uterm_con_defs "~ COMB u v = VAR(x)";
clasohm@968
    79
by (rtac In1_not_In0 1);
clasohm@968
    80
qed "COMB_not_VAR";
clasohm@968
    81
bind_thm ("VAR_not_COMB", (COMB_not_VAR RS not_sym));
clasohm@968
    82
bind_thm ("COMB_neq_VAR", (COMB_not_VAR RS notE));
clasohm@968
    83
val VAR_neq_COMB = sym RS COMB_neq_VAR;
clasohm@968
    84
clasohm@968
    85
goalw UTerm.thy uterm_con_defs "~ VAR(x) = CONST(c)";
clasohm@968
    86
by (rtac In0_not_In1 1);
clasohm@968
    87
qed "VAR_not_CONST";
clasohm@968
    88
bind_thm ("CONST_not_VAR", (VAR_not_CONST RS not_sym));
clasohm@968
    89
bind_thm ("VAR_neq_CONST", (VAR_not_CONST RS notE));
clasohm@968
    90
val CONST_neq_VAR = sym RS VAR_neq_CONST;
clasohm@968
    91
clasohm@968
    92
clasohm@968
    93
goalw UTerm.thy [Const_def,Comb_def] "~ Const(c) = Comb u v";
clasohm@968
    94
by (rtac (CONST_not_COMB RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
clasohm@968
    95
by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
clasohm@968
    96
qed "Const_not_Comb";
clasohm@968
    97
bind_thm ("Comb_not_Const", (Const_not_Comb RS not_sym));
clasohm@968
    98
bind_thm ("Const_neq_Comb", (Const_not_Comb RS notE));
clasohm@968
    99
val Comb_neq_Const = sym RS Const_neq_Comb;
clasohm@968
   100
clasohm@968
   101
goalw UTerm.thy [Comb_def,Var_def] "~ Comb u v = Var(x)";
clasohm@968
   102
by (rtac (COMB_not_VAR RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
clasohm@968
   103
by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
clasohm@968
   104
qed "Comb_not_Var";
clasohm@968
   105
bind_thm ("Var_not_Comb", (Comb_not_Var RS not_sym));
clasohm@968
   106
bind_thm ("Comb_neq_Var", (Comb_not_Var RS notE));
clasohm@968
   107
val Var_neq_Comb = sym RS Comb_neq_Var;
clasohm@968
   108
clasohm@968
   109
goalw UTerm.thy [Var_def,Const_def] "~ Var(x) = Const(c)";
clasohm@968
   110
by (rtac (VAR_not_CONST RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
clasohm@968
   111
by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
clasohm@968
   112
qed "Var_not_Const";
clasohm@968
   113
bind_thm ("Const_not_Var", (Var_not_Const RS not_sym));
clasohm@968
   114
bind_thm ("Var_neq_Const", (Var_not_Const RS notE));
clasohm@968
   115
val Const_neq_Var = sym RS Var_neq_Const;
clasohm@968
   116
clasohm@968
   117
clasohm@968
   118
(** Injectiveness of CONST and Const **)
clasohm@968
   119
clasohm@968
   120
val inject_cs = HOL_cs addSEs [Scons_inject] 
clasohm@968
   121
                       addSDs [In0_inject,In1_inject];
clasohm@968
   122
clasohm@968
   123
goalw UTerm.thy [VAR_def] "(VAR(M)=VAR(N)) = (M=N)";
clasohm@968
   124
by (fast_tac inject_cs 1);
clasohm@968
   125
qed "VAR_VAR_eq";
clasohm@968
   126
clasohm@968
   127
goalw UTerm.thy [CONST_def] "(CONST(M)=CONST(N)) = (M=N)";
clasohm@968
   128
by (fast_tac inject_cs 1);
clasohm@968
   129
qed "CONST_CONST_eq";
clasohm@968
   130
clasohm@968
   131
goalw UTerm.thy [COMB_def] "(COMB K L = COMB M N) = (K=M & L=N)";
clasohm@968
   132
by (fast_tac inject_cs 1);
clasohm@968
   133
qed "COMB_COMB_eq";
clasohm@968
   134
clasohm@968
   135
bind_thm ("VAR_inject", (VAR_VAR_eq RS iffD1));
clasohm@968
   136
bind_thm ("CONST_inject", (CONST_CONST_eq RS iffD1));
clasohm@968
   137
bind_thm ("COMB_inject", (COMB_COMB_eq RS iffD1 RS conjE));
clasohm@968
   138
clasohm@968
   139
clasohm@968
   140
(*For reasoning about abstract uterm constructors*)
clasohm@968
   141
val uterm_cs = set_cs addIs uterm.intrs @ [Rep_uterm]
clasohm@1465
   142
                      addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST,
clasohm@1465
   143
                              COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR,
clasohm@1465
   144
                              COMB_inject]
clasohm@1465
   145
                      addSDs [VAR_inject,CONST_inject,
clasohm@1465
   146
                              inj_onto_Abs_uterm RS inj_ontoD,
clasohm@1465
   147
                              inj_Rep_uterm RS injD, Leaf_inject];
clasohm@968
   148
clasohm@968
   149
goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)";
clasohm@968
   150
by (fast_tac uterm_cs 1);
clasohm@968
   151
qed "Var_Var_eq";
clasohm@968
   152
bind_thm ("Var_inject", (Var_Var_eq RS iffD1));
clasohm@968
   153
clasohm@968
   154
goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)";
clasohm@968
   155
by (fast_tac uterm_cs 1);
clasohm@968
   156
qed "Const_Const_eq";
clasohm@968
   157
bind_thm ("Const_inject", (Const_Const_eq RS iffD1));
clasohm@968
   158
clasohm@968
   159
goalw UTerm.thy [Comb_def] "(Comb u v =Comb x y) = (u=x & v=y)";
clasohm@968
   160
by (fast_tac uterm_cs 1);
clasohm@968
   161
qed "Comb_Comb_eq";
clasohm@968
   162
bind_thm ("Comb_inject", (Comb_Comb_eq RS iffD1 RS conjE));
clasohm@968
   163
clasohm@968
   164
val [major] = goal UTerm.thy "VAR(M): uterm(A) ==> M : A";
clasohm@968
   165
by (rtac (major RS setup_induction) 1);
clasohm@968
   166
by (etac uterm.induct 1);
clasohm@968
   167
by (ALLGOALS (fast_tac uterm_cs));
clasohm@968
   168
qed "VAR_D";
clasohm@968
   169
clasohm@968
   170
val [major] = goal UTerm.thy "CONST(M): uterm(A) ==> M : A";
clasohm@968
   171
by (rtac (major RS setup_induction) 1);
clasohm@968
   172
by (etac uterm.induct 1);
clasohm@968
   173
by (ALLGOALS (fast_tac uterm_cs));
clasohm@968
   174
qed "CONST_D";
clasohm@968
   175
clasohm@968
   176
val [major] = goal UTerm.thy
clasohm@968
   177
    "COMB M N: uterm(A) ==> M: uterm(A) & N: uterm(A)";
clasohm@968
   178
by (rtac (major RS setup_induction) 1);
clasohm@968
   179
by (etac uterm.induct 1);
clasohm@968
   180
by (ALLGOALS (fast_tac uterm_cs));
clasohm@968
   181
qed "COMB_D";
clasohm@968
   182
clasohm@968
   183
(*Basic ss with constructors and their freeness*)
clasohm@1266
   184
Addsimps (uterm.intrs @
clasohm@1266
   185
          [Const_not_Comb,Comb_not_Var,Var_not_Const,
clasohm@1266
   186
           Comb_not_Const,Var_not_Comb,Const_not_Var,
clasohm@1266
   187
           Var_Var_eq,Const_Const_eq,Comb_Comb_eq,
clasohm@1266
   188
           CONST_not_COMB,COMB_not_VAR,VAR_not_CONST,
clasohm@1266
   189
           COMB_not_CONST,VAR_not_COMB,CONST_not_VAR,
clasohm@1266
   190
           VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq]);
clasohm@968
   191
clasohm@968
   192
goal UTerm.thy "!u. t~=Comb t u";
clasohm@968
   193
by (uterm_ind_tac "t" 1);
clasohm@968
   194
by (rtac (Var_not_Comb RS allI) 1);
clasohm@968
   195
by (rtac (Const_not_Comb RS allI) 1);
clasohm@1266
   196
by (Asm_simp_tac 1);
clasohm@968
   197
qed "t_not_Comb_t";
clasohm@968
   198
clasohm@968
   199
goal UTerm.thy "!t. u~=Comb t u";
clasohm@968
   200
by (uterm_ind_tac "u" 1);
clasohm@968
   201
by (rtac (Var_not_Comb RS allI) 1);
clasohm@968
   202
by (rtac (Const_not_Comb RS allI) 1);
clasohm@1266
   203
by (Asm_simp_tac 1);
clasohm@968
   204
qed "u_not_Comb_u";
clasohm@968
   205
clasohm@968
   206
clasohm@968
   207
(*** UTerm_rec -- by wf recursion on pred_sexp ***)
clasohm@968
   208
clasohm@968
   209
val UTerm_rec_unfold =
clasohm@968
   210
    [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec;
clasohm@968
   211
clasohm@968
   212
(** conversion rules **)
clasohm@968
   213
clasohm@968
   214
goalw UTerm.thy [VAR_def] "UTerm_rec (VAR x) b c d = b(x)";
clasohm@968
   215
by (rtac (UTerm_rec_unfold RS trans) 1);
clasohm@1266
   216
by (simp_tac (!simpset addsimps [Case_In0]) 1);
clasohm@968
   217
qed "UTerm_rec_VAR";
clasohm@968
   218
clasohm@968
   219
goalw UTerm.thy [CONST_def] "UTerm_rec (CONST x) b c d = c(x)";
clasohm@968
   220
by (rtac (UTerm_rec_unfold RS trans) 1);
clasohm@1266
   221
by (simp_tac (!simpset addsimps [Case_In0,Case_In1]) 1);
clasohm@968
   222
qed "UTerm_rec_CONST";
clasohm@968
   223
clasohm@968
   224
goalw UTerm.thy [COMB_def]
clasohm@1465
   225
    "!!M N. [| M: sexp;  N: sexp |] ==>         \
clasohm@968
   226
\           UTerm_rec (COMB M N) b c d = \
clasohm@968
   227
\           d M N (UTerm_rec M b c d) (UTerm_rec N b c d)";
clasohm@968
   228
by (rtac (UTerm_rec_unfold RS trans) 1);
clasohm@1266
   229
by (simp_tac (!simpset addsimps [Split,Case_In1]) 1);
clasohm@1266
   230
by (asm_simp_tac (!simpset addsimps [In1_def]) 1);
clasohm@968
   231
qed "UTerm_rec_COMB";
clasohm@968
   232
clasohm@968
   233
(*** uterm_rec -- by UTerm_rec ***)
clasohm@968
   234
clasohm@968
   235
val Rep_uterm_in_sexp =
clasohm@968
   236
    Rep_uterm RS (range_Leaf_subset_sexp RS uterm_subset_sexp RS subsetD);
clasohm@968
   237
clasohm@1266
   238
Addsimps [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, 
clasohm@1266
   239
          Abs_uterm_inverse, Rep_uterm_inverse, 
clasohm@1266
   240
          Rep_uterm, rangeI, inj_Leaf, Inv_f_f, Rep_uterm_in_sexp];
clasohm@968
   241
clasohm@968
   242
goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec (Var x) b c d = b(x)";
clasohm@1266
   243
by (Simp_tac 1);
clasohm@968
   244
qed "uterm_rec_Var";
clasohm@968
   245
clasohm@968
   246
goalw UTerm.thy [uterm_rec_def, Const_def] "uterm_rec (Const x) b c d = c(x)";
clasohm@1266
   247
by (Simp_tac 1);
clasohm@968
   248
qed "uterm_rec_Const";
clasohm@968
   249
clasohm@968
   250
goalw UTerm.thy [uterm_rec_def, Comb_def]
clasohm@1266
   251
  "uterm_rec (Comb u v) b c d = d u v (uterm_rec u b c d) (uterm_rec v b c d)";
clasohm@1266
   252
by (Simp_tac 1);
clasohm@968
   253
qed "uterm_rec_Comb";
clasohm@968
   254
clasohm@1266
   255
Addsimps [uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb];
clasohm@968
   256
clasohm@968
   257
clasohm@968
   258
(**********)
clasohm@968
   259
clasohm@1266
   260
val uterm_rews = [t_not_Comb_t,u_not_Comb_u];