0
|
1 |
(* Title: ZF/constructor.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
516
|
6 |
Constructor function module -- for (Co)Datatype Definitions
|
0
|
7 |
*)
|
|
8 |
|
516
|
9 |
signature CONSTRUCTOR_ARG =
|
0
|
10 |
sig
|
516
|
11 |
val thy : theory (*parent containing constructor defs*)
|
|
12 |
val big_rec_name : string (*name of mutually recursive set*)
|
|
13 |
val con_ty_lists : ((string*typ*mixfix) *
|
|
14 |
string * term list * term list) list list
|
|
15 |
(*description of constructors*)
|
0
|
16 |
end;
|
|
17 |
|
|
18 |
signature CONSTRUCTOR_RESULT =
|
|
19 |
sig
|
516
|
20 |
val con_defs : thm list (*definitions made in thy*)
|
0
|
21 |
val case_eqns : thm list (*equations for case operator*)
|
|
22 |
val free_iffs : thm list (*freeness rewrite rules*)
|
|
23 |
val free_SEs : thm list (*freeness destruct rules*)
|
|
24 |
val mk_free : string -> thm (*makes freeness theorems*)
|
|
25 |
end;
|
|
26 |
|
|
27 |
|
516
|
28 |
(*Proves theorems relating to constructors*)
|
|
29 |
functor Constructor_Fun (structure Const: CONSTRUCTOR_ARG and
|
0
|
30 |
Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
|
|
31 |
struct
|
516
|
32 |
open Logic Const Ind_Syntax;
|
0
|
33 |
|
516
|
34 |
(*1st element is the case definition; others are the constructors*)
|
0
|
35 |
val big_case_name = big_rec_name ^ "_case";
|
|
36 |
|
516
|
37 |
val con_defs = get_def thy big_case_name ::
|
|
38 |
map (get_def thy o #2) (flat con_ty_lists);
|
0
|
39 |
|
|
40 |
(** Prove the case theorem **)
|
|
41 |
|
516
|
42 |
(*Get the case term from its definition*)
|
|
43 |
val Const("==",_) $ big_case_tm $ _ =
|
|
44 |
hd con_defs |> rep_thm |> #prop |> unvarify;
|
|
45 |
|
|
46 |
val (_, big_case_args) = strip_comb big_case_tm;
|
|
47 |
|
0
|
48 |
(*Each equation has the form
|
|
49 |
rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
|
516
|
50 |
fun mk_case_equation (((id,T,syn), name, args, prems), case_free) =
|
|
51 |
mk_tprop (eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
|
|
52 |
$ (list_comb (case_free, args))) ;
|
0
|
53 |
|
|
54 |
val case_trans = hd con_defs RS def_trans;
|
|
55 |
|
516
|
56 |
(*Proves a single case equation. Could use simp_tac, but it's slower!*)
|
0
|
57 |
fun case_tacsf con_def _ =
|
|
58 |
[rewtac con_def,
|
|
59 |
rtac case_trans 1,
|
|
60 |
REPEAT (resolve_tac [refl, Pr.split_eq RS trans,
|
|
61 |
Su.case_inl RS trans,
|
|
62 |
Su.case_inr RS trans] 1)];
|
|
63 |
|
|
64 |
fun prove_case_equation (arg,con_def) =
|
516
|
65 |
prove_term (sign_of thy) []
|
0
|
66 |
(mk_case_equation arg, case_tacsf con_def);
|
|
67 |
|
|
68 |
val free_iffs =
|
|
69 |
map standard (con_defs RL [def_swap_iff]) @
|
|
70 |
[Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
|
|
71 |
|
|
72 |
val free_SEs = map (gen_make_elim [conjE,FalseE]) (free_iffs RL [iffD1]);
|
|
73 |
|
|
74 |
val free_cs = ZF_cs addSEs free_SEs;
|
|
75 |
|
|
76 |
(*Typical theorems have the form ~con1=con2, con1=con2==>False,
|
|
77 |
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
|
|
78 |
fun mk_free s =
|
516
|
79 |
prove_goalw thy con_defs s
|
0
|
80 |
(fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]);
|
|
81 |
|
|
82 |
val case_eqns = map prove_case_equation
|
|
83 |
(flat con_ty_lists ~~ big_case_args ~~ tl con_defs);
|
|
84 |
|
|
85 |
end;
|
|
86 |
|
|
87 |
|