Subst/uterm.ML

changed "." to "$" and Cons to infix "#" to eliminate ambiguity

(*  Title: 	Substitutions/uterm.ML
    Author: 	Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

For uterm.thy.  
*)

open UTerm;

(** the uterm functional **)

goal UTerm.thy "mono(%Z. A <+> A <+> Z <*> Z)";
by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono] 1));
val UTerm_fun_mono = result();

val UTerm_unfold = UTerm_fun_mono RS (UTerm_def RS def_lfp_Tarski);

(*This justifies using UTerm in other recursive type definitions*)
val prems = goalw UTerm.thy [UTerm_def] "[| A<=B |] ==> UTerm(A) <= UTerm(B)";
by (REPEAT (ares_tac (prems@[monoI, subset_refl, lfp_mono, 
			     usum_mono, uprod_mono]) 1));
val UTerm_mono = result();

(** Type checking rules -- UTerm creates well-founded sets **)

val prems = goalw UTerm.thy [UTerm_def] "UTerm(Sexp) <= Sexp";
by (rtac lfp_lowerbound 1);
by (fast_tac (univ_cs addIs [Sexp_In0I,Sexp_In1I,Sexp_SconsI]) 1);
val UTerm_Sexp = result();

(* A <= Sexp ==> UTerm(A) <= Sexp *)
val UTerm_subset_Sexp = standard
    (UTerm_mono RS (UTerm_Sexp RSN (2,subset_trans)));

(** Induction **)

(*Induction for the set UTerm(A) *)
val major::prems = goalw UTerm.thy [VAR_def,CONST_def,COMB_def]
    "[| M: UTerm(A);  !!M.M : A ==> P(VAR(M));  !!M.M : A ==> P(CONST(M));   \
\       !!M N. [| M: UTerm(A);  N: UTerm(A);  P(M);  P(N) |] ==> P(COMB(M,N)) |]  \
\    ==> P(M)";
by (rtac (major RS (UTerm_def RS def_induct)) 1);
by (rtac UTerm_fun_mono 1);
by (fast_tac (set_cs addIs prems addEs [usumE,uprodE]) 1);
val UTerm_induct = result();

(*Induction for the type 'a uterm *)
val prems = goalw UTerm.thy [Var_def,Const_def,Comb_def]
    "[| !!x.P(Var(x));  !!x.P(Const(x));  \
\       !!u v. [|  P(u);  P(v) |] ==> P(Comb(u,v)) |]  ==> P(t)";
by (rtac (Rep_UTerm_inverse RS subst) 1);   (*types force good instantiation*)
by (rtac (Rep_UTerm RS UTerm_induct) 1);
by (REPEAT (ares_tac prems 1
     ORELSE eresolve_tac [rangeE, ssubst, Abs_UTerm_inverse RS subst] 1));
val uterm_induct = result();

(*Perform induction on xs. *)
fun uterm_ind_tac a M = 
    EVERY [res_inst_tac [("t",a)] uterm_induct M,
	   rename_last_tac a ["1"] (M+1)];

(** Introduction rules for UTerm constructors **)

(* c : A <+> A <+> UTerm(A) <*> UTerm(A) ==> c : UTerm(A) *)
val UTermI = UTerm_unfold RS equalityD2 RS subsetD;

(* Nil is a UTerm -- this also justifies the type definition*)
val prems = goalw UTerm.thy [VAR_def] "v:A ==> VAR(v) : UTerm(A)";
by (REPEAT (resolve_tac ([singletonI, UTermI, usum_In0I]@prems) 1));
val VAR_I = result();

val prems = goalw UTerm.thy [CONST_def] "c:A ==> CONST(c) : UTerm(A)";
by (REPEAT (resolve_tac ([singletonI, UTermI, usum_In0I, usum_In1I]@prems) 1));
val CONST_I = result();

val prems = goalw UTerm.thy [COMB_def]
    "[| M:UTerm(A);  N:UTerm(A) |] ==> COMB(M,N) : UTerm(A)";
by (REPEAT (resolve_tac (prems@[UTermI, uprodI, usum_In1I]) 1));
val COMB_I = result();

(*** Isomorphisms ***)

goal UTerm.thy "inj(Rep_UTerm)";
by (rtac inj_inverseI 1);
by (rtac Rep_UTerm_inverse 1);
val inj_Rep_UTerm = result();

goal UTerm.thy "inj_onto(Abs_UTerm,UTerm(range(Leaf)))";
by (rtac inj_onto_inverseI 1);
by (etac Abs_UTerm_inverse 1);
val inj_onto_Abs_UTerm = result();

(** Distinctness of constructors **)

goalw UTerm.thy [CONST_def,COMB_def] "~ CONST(c) = COMB(u,v)";
by (rtac notI 1);
by (etac (In1_inject RS (In0_not_In1 RS notE)) 1);
val CONST_not_COMB = result();
val COMB_not_CONST = standard (CONST_not_COMB RS not_sym);
val CONST_neq_COMB = standard (CONST_not_COMB RS notE);
val COMB_neq_CONST = sym RS CONST_neq_COMB;

goalw UTerm.thy [COMB_def,VAR_def] "~ COMB(u,v) = VAR(x)";
by (rtac In1_not_In0 1);
val COMB_not_VAR = result();
val VAR_not_COMB = standard (COMB_not_VAR RS not_sym);
val COMB_neq_VAR = standard (COMB_not_VAR RS notE);
val VAR_neq_COMB = sym RS COMB_neq_VAR;

goalw UTerm.thy [VAR_def,CONST_def] "~ VAR(x) = CONST(c)";
by (rtac In0_not_In1 1);
val VAR_not_CONST = result();
val CONST_not_VAR = standard (VAR_not_CONST RS not_sym);
val VAR_neq_CONST = standard (VAR_not_CONST RS notE);
val CONST_neq_VAR = sym RS VAR_neq_CONST;


goalw UTerm.thy [Const_def,Comb_def] "~ Const(c) = Comb(u,v)";
by (rtac (CONST_not_COMB RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1);
by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1));
val Const_not_Comb = result();
val Comb_not_Const = standard (Const_not_Comb RS not_sym);
val Const_neq_Comb = standard (Const_not_Comb RS notE);
val Comb_neq_Const = sym RS Const_neq_Comb;

goalw UTerm.thy [Comb_def,Var_def] "~ Comb(u,v) = Var(x)";
by (rtac (COMB_not_VAR RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1);
by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1));
val Comb_not_Var = result();
val Var_not_Comb = standard (Comb_not_Var RS not_sym);
val Comb_neq_Var = standard (Comb_not_Var RS notE);
val Var_neq_Comb = sym RS Comb_neq_Var;

goalw UTerm.thy [Var_def,Const_def] "~ Var(x) = Const(c)";
by (rtac (VAR_not_CONST RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1);
by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1));
val Var_not_Const = result();
val Const_not_Var = standard (Var_not_Const RS not_sym);
val Var_neq_Const = standard (Var_not_Const RS notE);
val Const_neq_Var = sym RS Var_neq_Const;


(** Injectiveness of CONST and Const **)

val inject_cs = HOL_cs addSEs [Scons_inject] 
                       addSDs [In0_inject,In1_inject];

goalw UTerm.thy [VAR_def] "(VAR(M)=VAR(N)) = (M=N)";
by (fast_tac inject_cs 1);
val VAR_VAR_eq = result();

goalw UTerm.thy [CONST_def] "(CONST(M)=CONST(N)) = (M=N)";
by (fast_tac inject_cs 1);
val CONST_CONST_eq = result();

goalw UTerm.thy [COMB_def] "(COMB(K,L)=COMB(M,N)) = (K=M & L=N)";
by (fast_tac inject_cs 1);
val COMB_COMB_eq = result();

val VAR_inject = standard (VAR_VAR_eq RS iffD1);
val CONST_inject = standard (CONST_CONST_eq RS iffD1);
val COMB_inject = standard (COMB_COMB_eq RS iffD1 RS conjE);


(*For reasoning about abstract uterm constructors*)
val UTerm_cs = set_cs addIs [Rep_UTerm, VAR_I, CONST_I, COMB_I]
	             addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST,
                             COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR,
                             COMB_inject]
		     addSDs [VAR_inject,CONST_inject,
                             inj_onto_Abs_UTerm RS inj_ontoD,
			     inj_Rep_UTerm RS injD, Leaf_inject];

goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)";
by (fast_tac UTerm_cs 1);
val Var_Var_eq = result();
val Var_inject = standard (Var_Var_eq RS iffD1);

goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)";
by (fast_tac UTerm_cs 1);
val Const_Const_eq = result();
val Const_inject = standard (Const_Const_eq RS iffD1);

goalw UTerm.thy [Comb_def] "(Comb(u,v)=Comb(x,y)) = (u=x & v=y)";
by (fast_tac UTerm_cs 1);
val Comb_Comb_eq = result();
val Comb_inject = standard (Comb_Comb_eq RS iffD1 RS conjE);

val [major] = goal UTerm.thy "VAR(M): UTerm(A) ==> M : A";
by (rtac (major RS setup_induction) 1);
by (etac UTerm_induct 1);
by (ALLGOALS (fast_tac UTerm_cs));
val VAR_D = result();

val [major] = goal UTerm.thy "CONST(M): UTerm(A) ==> M : A";
by (rtac (major RS setup_induction) 1);
by (etac UTerm_induct 1);
by (ALLGOALS (fast_tac UTerm_cs));
val CONST_D = result();

val [major] = goal UTerm.thy
    "COMB(M,N): UTerm(A) ==> M: UTerm(A) & N: UTerm(A)";
by (rtac (major RS setup_induction) 1);
by (etac UTerm_induct 1);
by (ALLGOALS (fast_tac UTerm_cs));
val COMB_D = result();

(*Basic ss with constructors and their freeness*)
val uterm_free_simps = [Const_not_Comb,Comb_not_Var,Var_not_Const,
                    Comb_not_Const,Var_not_Comb,Const_not_Var,
                    Var_Var_eq,Const_Const_eq,Comb_Comb_eq,
		    CONST_not_COMB,COMB_not_VAR,VAR_not_CONST,
                    COMB_not_CONST,VAR_not_COMB,CONST_not_VAR,
		    VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq,
		    VAR_I, CONST_I, COMB_I];
val uterm_free_ss = HOL_ss addsimps uterm_free_simps;

goal UTerm.thy "!u. ~(t=Comb(t,u))";
by (uterm_ind_tac "t" 1);
by (rtac (Var_not_Comb RS allI) 1);
by (rtac (Const_not_Comb RS allI) 1);
by (asm_simp_tac uterm_free_ss 1);
val t_not_Comb_t = result();

goal UTerm.thy "!t. ~(u=Comb(t,u))";
by (uterm_ind_tac "u" 1);
by (rtac (Var_not_Comb RS allI) 1);
by (rtac (Const_not_Comb RS allI) 1);
by (asm_simp_tac uterm_free_ss 1);
val u_not_Comb_u = result();


(*** UTerm_rec -- by wf recursion on pred_Sexp ***)

val UTerm_rec_unfold =
    wf_pred_Sexp RS wf_trancl RS (UTerm_rec_def RS def_wfrec);

(** conversion rules **)

goalw UTerm.thy [VAR_def] "UTerm_rec(VAR(x),b,c,d) = b(x)";
by (rtac (UTerm_rec_unfold RS trans) 1);
by (rtac Case_In0 1);
val UTerm_rec_VAR = result();

goalw UTerm.thy [CONST_def] "UTerm_rec(CONST(x),b,c,d) = c(x)";
by (rtac (UTerm_rec_unfold RS trans) 1);
by (simp_tac (HOL_ss addsimps [Case_In0,Case_In1]) 1);
val UTerm_rec_CONST = result();

val prems = goalw UTerm.thy [COMB_def]
    "[| M: Sexp;  N: Sexp |] ==> 	\
\    UTerm_rec(COMB(M,N), b, c, d) = \
\    d(M, N, UTerm_rec(M,b,c,d), UTerm_rec(N,b,c,d))";
by (rtac (UTerm_rec_unfold RS trans) 1);
by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1);
by (simp_tac (pred_Sexp_ss addsimps (In1_def::prems)) 1);
val UTerm_rec_COMB = result();

(*** uterm_rec -- by UTerm_rec ***)

val Rep_UTerm_in_Sexp =
    Rep_UTerm RS (range_Leaf_subset_Sexp RS UTerm_subset_Sexp RS subsetD);

val uterm_rec_simps = [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, 
		 Abs_UTerm_inverse, Rep_UTerm_inverse, VAR_I, CONST_I, COMB_I,
		 Rep_UTerm, rangeI, inj_Leaf, Inv_f_f, Rep_UTerm_in_Sexp];
val uterm_rec_ss = HOL_ss addsimps uterm_rec_simps;

goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec(Var(x),b,c,d) = b(x)";
by (simp_tac uterm_rec_ss 1);
val uterm_rec_Var = result();

goalw UTerm.thy [uterm_rec_def, Const_def] "uterm_rec(Const(x),b,c,d) = c(x)";
by (simp_tac uterm_rec_ss 1);
val uterm_rec_Const = result();

goalw UTerm.thy [uterm_rec_def, Comb_def]
   "uterm_rec(Comb(u,v),b,c,d) = d(u,v,uterm_rec(u,b,c,d),uterm_rec(v,b,c,d))";
by (simp_tac uterm_rec_ss 1);
val uterm_rec_Comb = result();

val uterm_simps = [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB,
		 uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb];
val uterm_ss = uterm_free_ss addsimps uterm_simps;

(*Type checking.  Useful?*)
val major::A_subset_Sexp::prems = goal UTerm.thy
    "[| M: UTerm(A);    \
\       A<=Sexp;      	\
\       !!x.x:A ==> b(x): C(VAR(x));       \
\       !!x.x:A ==> c(x): C(CONST(x));       \
\       !!x y q r. [| x: UTerm(A); y: UTerm(A); q: C(x); r: C(y) |] ==> \
\                  d(x,y,q,r): C(COMB(x,y)) \
\    |] ==> UTerm_rec(M,b,c,d) : C(M)";
val Sexp_UTermA_I = A_subset_Sexp RS UTerm_subset_Sexp RS subsetD;
val Sexp_A_I = A_subset_Sexp RS subsetD;
by (rtac (major RS UTerm_induct) 1);
by (ALLGOALS
    (asm_simp_tac (uterm_ss addsimps ([Sexp_A_I,Sexp_UTermA_I] @ prems))));
val UTerm_rec_type = result();


(**********)

val uterm_rews = [uterm_rec_Var,uterm_rec_Const,uterm_rec_Comb,
		  t_not_Comb_t,u_not_Comb_u,
                  Const_not_Comb,Comb_not_Var,Var_not_Const,
                  Comb_not_Const,Var_not_Comb,Const_not_Var,
                  Var_Var_eq,Const_Const_eq,Comb_Comb_eq];

(*
val prems = goal Subst.thy
    "[| !!x.P(Var(x));  !!x.P(Const(x));  \
\       !!u v. P(u) --> P(v) --> P(Comb(u,v)) |]  ==> P(a)";
by (uterm_ind_tac "a" 1);
by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
val uterm_induct2 = result();

add_inds uterm_induct2;
*)