ex/Term.ML

-(*  Title: 	HOL/ex/term
+(*  Title: 	HOL/ex/Term
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-For term.thy.  illustrates List functor
+Terms over a given alphabet -- function applications; illustrates list functor
   (essentially the same type as in Trees & Forests)
 *)
 
 open Term;
 
 (*** Monotonicity and unfolding of the function ***)
 
-goal Term.thy "mono(%Z.  A <*> List(Z))";
-by (REPEAT (ares_tac [monoI, subset_refl, List_mono, uprod_mono] 1));
-val Term_fun_mono = result();
+goal Term.thy "term(A) = A <*> list(term(A))";
+by (fast_tac (univ_cs addSIs (equalityI :: term.intrs)
+                      addEs [term.elim]) 1);
+val term_unfold = result();
 
-val Term_unfold = Term_fun_mono RS (Term_def RS def_lfp_Tarski);
+(*This justifies using term in other recursive type definitions*)
+goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)";
+by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
+val term_mono = result();
 
-(*This justifies using Term in other recursive type definitions*)
-goalw Term.thy [Term_def] "!!A B. A<=B ==> Term(A) <= Term(B)";
-by (REPEAT (ares_tac [lfp_mono, subset_refl, List_mono, uprod_mono] 1));
-val Term_mono = result();
+(** Type checking -- term creates well-founded sets **)
 
-(** Type checking rules -- Term creates well-founded sets **)
+goalw Term.thy term.defs "term(sexp) <= sexp";
+by (rtac lfp_lowerbound 1);
+by (fast_tac (univ_cs addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
+val term_sexp = result();
 
-val prems = goalw Term.thy [Term_def] "Term(Sexp) <= Sexp";
-by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs [Sexp_SconsI, List_Sexp RS subsetD]) 1);
-val Term_Sexp = result();
-
-(* A <= Sexp ==> Term(A) <= Sexp *)
-val Term_subset_Sexp = standard
-    (Term_mono RS (Term_Sexp RSN (2,subset_trans)));
+(* A <= sexp ==> term(A) <= sexp *)
+val term_subset_sexp = standard ([term_mono, term_sexp] MRS subset_trans);
 
 
-(** Elimination -- structural induction on the set Term(A) **)
+(** Elimination -- structural induction on the set term(A) **)
 
-(*Induction for the set Term(A) *)
+(*Induction for the set term(A) *)
 val [major,minor] = goal Term.thy 
-    "[| M: Term(A);  \
-\       !!x zs. [| x: A;  zs: List(Term(A));  zs: List({x.R(x)}) \
+    "[| M: term(A);  \
+\       !!x zs. [| x: A;  zs: list(term(A));  zs: list({x.R(x)}) \
 \               |] ==> R(x$zs)  \
 \    |] ==> R(M)";
-by (rtac (major RS (Term_def RS def_induct)) 1);
-by (rtac Term_fun_mono 1);
-by (REPEAT (eresolve_tac ([uprodE, ssubst, minor] @
- 		([Int_lower1,Int_lower2] RL [List_mono RS subsetD])) 1));
-val Term_induct = result();
+by (rtac (major RS term.induct) 1);
+by (REPEAT (eresolve_tac ([minor] @
+ 		([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1));
+(*Proof could also use  mono_Int RS subsetD RS IntE *)
+val term_induct = result();
 
-(*Induction on Term(A) followed by induction on List *)
+(*Induction on term(A) followed by induction on list *)
 val major::prems = goal Term.thy
-    "[| M: Term(A);  \
+    "[| M: term(A);  \
 \       !!x.      [| x: A |] ==> R(x$NIL);  \
-\       !!x z zs. [| x: A;  z: Term(A);  zs: List(Term(A));  R(x$zs)  \
+\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  R(x$zs)  \
 \                 |] ==> R(x $ CONS(z,zs))  \
 \    |] ==> R(M)";
-by (rtac (major RS Term_induct) 1);
-by (etac List_induct 1);
+by (rtac (major RS term_induct) 1);
+by (etac list.induct 1);
 by (REPEAT (ares_tac prems 1));
-val Term_induct2 = result();
+val term_induct2 = result();
 
 (*** Structural Induction on the abstract type 'a term ***)
 
 val list_all_ss = map_ss addsimps [list_all_Nil, list_all_Cons];
 
-val Rep_Term_in_Sexp =
-    Rep_Term RS (range_Leaf_subset_Sexp RS Term_subset_Sexp RS subsetD);
+val Rep_term_in_sexp =
+    Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD);
 
 (*Induction for the abstract type 'a term*)
-val prems = goalw Term.thy [App_def,Rep_TList_def,Abs_TList_def]
+val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]
     "[| !!x ts. list_all(R,ts) ==> R(App(x,ts))  \
 \    |] ==> R(t)";
-by (rtac (Rep_Term_inverse RS subst) 1);   (*types force good instantiation*)
-by (res_inst_tac [("P","Rep_Term(t) : Sexp")] conjunct2 1);
-by (rtac (Rep_Term RS Term_induct) 1);
-by (REPEAT (ares_tac [conjI, Sexp_SconsI, Term_subset_Sexp RS 
-    List_subset_Sexp,range_Leaf_subset_Sexp] 1
+by (rtac (Rep_term_inverse RS subst) 1);   (*types force good instantiation*)
+by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);
+by (rtac (Rep_term RS term_induct) 1);
+by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS 
+    list_subset_sexp, range_Leaf_subset_sexp] 1
      ORELSE etac rev_subsetD 1));
-by (eres_inst_tac [("A1","Term(?u)"), ("f1","Rep_Term"), ("g1","Abs_Term")]
+by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")]
     	(Abs_map_inverse RS subst) 1);
-by (rtac (range_Leaf_subset_Sexp RS Term_subset_Sexp) 1);
-by (etac Abs_Term_inverse 1);
+by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1);
+by (etac Abs_term_inverse 1);
 by (etac rangeE 1);
 by (hyp_subst_tac 1);
 by (resolve_tac prems 1);
-by (etac List_induct 1);
+by (etac list.induct 1);
 by (etac CollectE 2);
 by (stac Abs_map_CONS 2);
 by (etac conjunct1 2);
 by (etac rev_subsetD 2);
-by (rtac List_subset_Sexp 2);
+by (rtac list_subset_sexp 2);
 by (fast_tac set_cs 2);
 by (ALLGOALS (asm_simp_tac list_all_ss));
 val term_induct = result();
 
 (*Induction for the abstract type 'a term*)

 fun term_ind2_tac a i = 
     EVERY [res_inst_tac [("t",a)] term_induct2 i,
 	   rename_last_tac a ["1","s"] (i+1)];
 
 
-(** Introduction rule for Term **)
 
-(* c : A <*> List(Term(A)) ==> c : Term(A) *)
-val TermI = standard (Term_unfold RS equalityD2 RS subsetD);
-
-(*The constant APP is not declared; it is simply . *)
-val prems = goal Term.thy "[| M: A;  N : List(Term(A)) |] ==> M$N : Term(A)";
-by (REPEAT (resolve_tac (prems@[TermI, ListI, uprodI]) 1));
-val APP_I = result();
-
-
-(*** Term_rec -- by wf recursion on pred_Sexp ***)
+(*** Term_rec -- by wf recursion on pred_sexp ***)
 
 val Term_rec_unfold =
-    wf_pred_Sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
+    wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
 
 (** conversion rules **)
 
 val [prem] = goal Term.thy
-    "N: List(Term(A)) ==>  \
-\    !M. <N,M>: pred_Sexp^+ --> \
-\        Abs_map(cut(h, pred_Sexp^+, M), N) = \
+    "N: list(term(A)) ==>  \
+\    !M. <N,M>: pred_sexp^+ --> \
+\        Abs_map(cut(h, pred_sexp^+, M), N) = \
 \        Abs_map(h,N)";
-by (rtac (prem RS List_induct) 1);
+by (rtac (prem RS list.induct) 1);
 by (simp_tac list_all_ss 1);
 by (strip_tac 1);
-by (etac (pred_Sexp_CONS_D RS conjE) 1);
-by (asm_simp_tac (list_all_ss addsimps [trancl_pred_SexpD1, cut_apply]) 1);
+by (etac (pred_sexp_CONS_D RS conjE) 1);
+by (asm_simp_tac (list_all_ss addsimps [trancl_pred_sexpD1, cut_apply]) 1);
 val Abs_map_lemma = result();
 
-val [prem1,prem2,A_subset_Sexp] = goal Term.thy
-    "[| M: Sexp;  N: List(Term(A));  A<=Sexp |] ==> \
+val [prem1,prem2,A_subset_sexp] = goal Term.thy
+    "[| M: sexp;  N: list(term(A));  A<=sexp |] ==> \
 \    Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
 by (rtac (Term_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps
       [Split,
-       prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl,
-       prem1, prem2 RS rev_subsetD, List_subset_Sexp,
-       Term_subset_Sexp, A_subset_Sexp])1);
+       prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl,
+       prem1, prem2 RS rev_subsetD, list_subset_sexp,
+       term_subset_sexp, A_subset_sexp])1);
 val Term_rec = result();
 
 (*** term_rec -- by Term_rec ***)
 
 local
   val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy)
-                        [("f","Rep_Term")] Rep_map_type;
-  val Rep_TList = Rep_Term RS Rep_map_type1;
-  val Rep_Term_rec = range_Leaf_subset_Sexp RSN (2,Rep_TList RSN(2,Term_rec));
+                        [("f","Rep_term")] Rep_map_type;
+  val Rep_Tlist = Rep_term RS Rep_map_type1;
+  val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec));
 
-  (*Now avoids conditional rewriting with the premise N: List(Term(A)),
+  (*Now avoids conditional rewriting with the premise N: list(term(A)),
     since A will be uninstantiated and will cause rewriting to fail. *)
   val term_rec_ss = HOL_ss 
-      addsimps [Rep_TList RS (rangeI RS APP_I RS Abs_Term_inverse),  
-	       Rep_Term_in_Sexp, Rep_Term_rec, Rep_Term_inverse,
+      addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse),  
+	       Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse,
 	       inj_Leaf, Inv_f_f,
-	       Abs_Rep_map, map_ident, Sexp_LeafI]
+	       Abs_Rep_map, map_ident, sexp.LeafI]
 in
 
 val term_rec = prove_goalw Term.thy
-	 [term_rec_def, App_def, Rep_TList_def, Abs_TList_def]
+	 [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def]
     "term_rec(App(f,ts), d) = d(f, ts, map (%t. term_rec(t,d), ts))"
  (fn _ => [simp_tac term_rec_ss 1])
 
 end;