author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 3925  90f499226ab9 
permissions  rwrr 
1461  1 
(* Title: ZF/constructor.ML 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  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 
1461  11 
val thy : theory (*parent containing constructor defs*) 
12 
val big_rec_name : string (*name of mutually recursive set*) 

516  13 
val con_ty_lists : ((string*typ*mixfix) * 
1461  14 
string * term list * term list) list list 
15 
(*description of constructors*) 

0  16 
end; 
17 

18 
signature CONSTRUCTOR_RESULT = 

19 
sig 

1461  20 
val con_defs : thm list (*definitions made in thy*) 
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*) 

0  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 = 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

31 
let 
0  32 

516  33 
(*1st element is the case definition; others are the constructors*) 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

34 
val big_case_name = Const.big_rec_name ^ "_case"; 
0  35 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

36 
val con_defs = get_def Const.thy big_case_name :: 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

37 
map (get_def Const.thy o #2) (flat Const.con_ty_lists); 
0  38 

39 
(** Prove the case theorem **) 

40 

516  41 
(*Get the case term from its definition*) 
42 
val Const("==",_) $ big_case_tm $ _ = 

543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

43 
hd con_defs > rep_thm > #prop > Logic.unvarify; 
516  44 

45 
val (_, big_case_args) = strip_comb big_case_tm; 

46 

0  47 
(*Each equation has the form 
48 
rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) 

516  49 
fun mk_case_equation (((id,T,syn), name, args, prems), case_free) = 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

50 
Ind_Syntax.mk_tprop 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

51 
(Ind_Syntax.eq_const $ (big_case_tm $ (list_comb (Const(name,T), args))) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

52 
$ (list_comb (case_free, args))) ; 
0  53 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

54 
val case_trans = hd con_defs RS Ind_Syntax.def_trans 
1103
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 [] 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

67 
(cterm_of (sign_of Const.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 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

70 
val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff]; 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

71 

f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

72 
in 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

73 
struct 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

74 
val con_defs = con_defs 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

75 

f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

76 
val free_iffs = con_iffs @ 
0  77 
[Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]; 
78 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

79 
val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs; 
0  80 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

81 
(*Typical theorems have the form ~con1=con2, con1=con2==>False, 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

82 
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <> x=y, etc. *) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

83 
fun mk_free s = 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

84 
prove_goalw Const.thy con_defs s 
1461  85 
(fn prems => [cut_facts_tac prems 1, 
86 
fast_tac (ZF_cs addSEs free_SEs) 1]); 

0  87 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

88 
val case_eqns = map prove_case_equation 
1461  89 
(flat Const.con_ty_lists ~~ big_case_args ~~ tl con_defs); 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1103
diff
changeset

90 
end 
0  91 
end; 
92 

93 