author | clasohm |
Fri, 17 Nov 1995 13:22:50 +0100 | |
changeset 1341 | 69fec018854c |
parent 1103 | 08fda5148971 |
child 1418 | f5f97ee67cbb |
permissions | -rw-r--r-- |
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 $ _ = |
|
543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset
|
44 |
hd con_defs |> rep_thm |> #prop |> Logic.unvarify; |
516 | 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 |
|
1103
08fda5148971
prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents:
543
diff
changeset
|
54 |
val case_trans = hd con_defs RS def_trans |
08fda5148971
prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents:
543
diff
changeset
|
55 |
and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans; |
0 | 56 |
|
516 | 57 |
(*Proves a single case equation. Could use simp_tac, but it's slower!*) |
0 | 58 |
fun case_tacsf con_def _ = |
59 |
[rewtac con_def, |
|
60 |
rtac case_trans 1, |
|
1103
08fda5148971
prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents:
543
diff
changeset
|
61 |
REPEAT (resolve_tac [refl, split_trans, |
08fda5148971
prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents:
543
diff
changeset
|
62 |
Su.case_inl RS trans, |
08fda5148971
prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents:
543
diff
changeset
|
63 |
Su.case_inr RS trans] 1)]; |
0 | 64 |
|
65 |
fun prove_case_equation (arg,con_def) = |
|
543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset
|
66 |
prove_goalw_cterm [] |
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset
|
67 |
(cterm_of (sign_of thy) (mk_case_equation arg)) |
1103
08fda5148971
prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents:
543
diff
changeset
|
68 |
(case_tacsf con_def); |
0 | 69 |
|
70 |
val free_iffs = |
|
71 |
map standard (con_defs RL [def_swap_iff]) @ |
|
72 |
[Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]; |
|
73 |
||
74 |
val free_SEs = map (gen_make_elim [conjE,FalseE]) (free_iffs RL [iffD1]); |
|
75 |
||
76 |
val free_cs = ZF_cs addSEs free_SEs; |
|
77 |
||
78 |
(*Typical theorems have the form ~con1=con2, con1=con2==>False, |
|
79 |
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *) |
|
80 |
fun mk_free s = |
|
516 | 81 |
prove_goalw thy con_defs s |
0 | 82 |
(fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]); |
83 |
||
84 |
val case_eqns = map prove_case_equation |
|
85 |
(flat con_ty_lists ~~ big_case_args ~~ tl con_defs); |
|
86 |
||
87 |
end; |
|
88 |
||
89 |