Subst/alist.ML
author convert-repo
Thu, 23 Jul 2009 14:03:20 +0000
changeset 255 435bf30c29a5
parent 48 21291189b51e
permissions -rw-r--r--
update tags
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	Substitutions/alist.ML
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     2
    Author: 	Martin Coen, Cambridge University Computer Laboratory
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     4
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     5
For alist.thy.
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     6
*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     7
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     8
open AList;
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     9
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    10
(*********)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    11
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    12
val al_defs = [alist_rec_def,assoc_def];
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    13
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    14
val alist_ss = pair_ss addsimps [Nil_not_Cons,Cons_not_Nil,Cons_Cons_eq,
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    15
                                list_rec_Nil,list_rec_Cons];
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    16
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    17
val al_rews = 
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    18
  let fun mk_thm s = prove_goalw AList.thy al_defs s 
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    19
                            (fn _ => [simp_tac alist_ss 1])
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    20
  in map mk_thm 
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    21
     ["alist_rec(Nil,c,d) = c",
48
21291189b51e changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents: 0
diff changeset
    22
      "alist_rec(<a,b>#al,c,d) = d(a,b,al,alist_rec(al,c,d))",
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    23
      "assoc(v,d,Nil) = d",
48
21291189b51e changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents: 0
diff changeset
    24
      "assoc(v,d,<a,b>#al) = if(v=a,b,assoc(v,d,al))"] end;
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    25
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    26
(*********)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    27
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    28
val prems = goal AList.thy
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    29
    "[| P(Nil);   \
48
21291189b51e changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents: 0
diff changeset
    30
\       !!x y xs. P(xs) ==> P(<x,y>#xs) |]  ==> P(l)";
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    31
by (list_ind_tac "l" 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    32
by (resolve_tac prems 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    33
by (rtac PairE 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    34
by (etac ssubst 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    35
by (resolve_tac prems 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    36
by (assume_tac 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    37
val alist_induct = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    38
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    39
(*Perform induction on xs. *)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    40
fun alist_ind_tac a M = 
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    41
    EVERY [res_inst_tac [("l",a)] alist_induct M,
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    42
	   rename_last_tac a ["1"] (M+1)];
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    43
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    44
(*
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    45
val prems = goal AList.thy
48
21291189b51e changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents: 0
diff changeset
    46
    "[| P(Nil);  !! x y xs. P(xs) --> P(<x,y>#xs) |] ==> P(a)";
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    47
by (alist_ind_tac "a" 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    48
by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    49
val alist_induct2 = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    50
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    51
add_inds alist_induct2;
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    52
*)