Subst/AList.ML

Initial revision

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

For alist.thy.
*)

open AList;

(*********)

val al_defs = [alist_rec_def,assoc_def];

val alist_ss = pair_ss addsimps [Nil_not_Cons,Cons_not_Nil,Cons_Cons_eq,
                                list_rec_Nil,list_rec_Cons];

val al_rews = 
  let fun mk_thm s = prove_goalw AList.thy al_defs s 
                            (fn _ => [simp_tac alist_ss 1])
  in map mk_thm 
     ["alist_rec(Nil,c,d) = c",
      "alist_rec(Cons(<a,b>,al),c,d) = d(a,b,al,alist_rec(al,c,d))",
      "assoc(v,d,Nil) = d",
      "assoc(v,d,Cons(<a,b>,al)) = if(v=a,b,assoc(v,d,al))"] end;

(*********)

val prems = goal AList.thy
    "[| P(Nil);   \
\       !!x y xs. P(xs) ==> P(Cons(<x,y>,xs)) |]  ==> P(l)";
by (list_ind_tac "l" 1);
by (resolve_tac prems 1);
by (rtac PairE 1);
by (etac ssubst 1);
by (resolve_tac prems 1);
by (assume_tac 1);
val alist_induct = result();

(*Perform induction on xs. *)
fun alist_ind_tac a M = 
    EVERY [res_inst_tac [("l",a)] alist_induct M,
	   rename_last_tac a ["1"] (M+1)];

(*
val prems = goal AList.thy
    "[| P(Nil);  !! x y xs. P(xs) --> P(Cons(<x,y>,xs)) |] ==> P(a)";
by (alist_ind_tac "a" 1);
by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
val alist_induct2 = result();

add_inds alist_induct2;
*)