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