Subst/AList.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Subst/AList.ML	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,52 @@
+(*  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;
+*)