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