author  wenzelm 
Tue, 29 Sep 2009 22:48:24 +0200  
changeset 32765  3032c0308019 
parent 32740  9dd0a2f83429 
child 35409  5c5bb83f2bae 
permissions  rwrr 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1 
(* Title: ZF/Datatype.thy 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

3 
Copyright 1997 University of Cambridge 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

4 
*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

5 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

6 
header{*Datatype and CoDatatype Definitions*} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

7 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

8 
theory Datatype_ZF 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

9 
imports Inductive_ZF Univ QUniv 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

10 
uses "Tools/datatype_package.ML" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

11 
begin 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

12 

26480  13 
ML {* 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

14 
(*Typechecking rules for most datatypes involving univ*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

15 
structure Data_Arg = 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

16 
struct 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

17 
val intrs = 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

18 
[@{thm SigmaI}, @{thm InlI}, @{thm InrI}, 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

19 
@{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ}, 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

20 
@{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}]; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

21 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

22 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

23 
val elims = [make_elim @{thm InlD}, make_elim @{thm InrD}, (*for mutual recursion*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

24 
@{thm SigmaE}, @{thm sumE}]; (*allows * and + in spec*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

25 
end; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

26 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

27 

32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

28 
structure Data_Package = 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

29 
Add_datatype_def_Fun 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

30 
(structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

31 
and Su=Standard_Sum 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

32 
and Ind_Package = Ind_Package 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

33 
and Datatype_Arg = Data_Arg 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

34 
val coind = false); 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

35 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

36 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

37 
(*Typechecking rules for most codatatypes involving quniv*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

38 
structure CoData_Arg = 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

39 
struct 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

40 
val intrs = 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

41 
[@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI}, 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

42 
@{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv}, 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

43 
@{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}]; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

44 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

45 
val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD}, (*for mutual recursion*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

46 
@{thm QSigmaE}, @{thm qsumE}]; (*allows * and + in spec*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

47 
end; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

48 

32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

49 
structure CoData_Package = 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

50 
Add_datatype_def_Fun 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

51 
(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

52 
and Su=Quine_Sum 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

53 
and Ind_Package = CoInd_Package 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

54 
and Datatype_Arg = CoData_Arg 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

55 
val coind = true); 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

56 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

57 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

58 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

59 
(*Simproc for freeness reasoning: compare datatype constructors for equality*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

60 
structure DataFree = 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

61 
struct 
32740  62 
val trace = Unsynchronized.ref false; 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

63 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

64 
fun mk_new ([],[]) = Const("True",FOLogic.oT) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

65 
 mk_new (largs,rargs) = 
32765  66 
Balanced_Tree.make FOLogic.mk_conj 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

67 
(map FOLogic.mk_eq (ListPair.zip (largs,rargs))); 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

68 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

69 
val datatype_ss = @{simpset}; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

70 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

71 
fun proc sg ss old = 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

72 
let val _ = 
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

73 
if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term_global sg old) 
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

74 
else () 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

75 
val (lhs,rhs) = FOLogic.dest_eq old 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

76 
val (lhead, largs) = strip_comb lhs 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

77 
and (rhead, rargs) = strip_comb rhs 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

78 
val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

79 
val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

80 
val lcon_info = the (Symtab.lookup (ConstructorsData.get sg) lname) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

81 
handle Option => raise Match; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

82 
val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

83 
handle Option => raise Match; 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

84 
val new = 
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

85 
if #big_rec_name lcon_info = #big_rec_name rcon_info 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

86 
andalso not (null (#free_iffs lcon_info)) then 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

87 
if lname = rname then mk_new (largs, rargs) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

88 
else Const("False",FOLogic.oT) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

89 
else raise Match 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

90 
val _ = 
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

91 
if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new) 
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32010
diff
changeset

92 
else (); 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

93 
val goal = Logic.mk_equals (old, new) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

94 
val thm = Goal.prove (Simplifier.the_context ss) [] [] goal 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

95 
(fn _ => rtac iff_reflection 1 THEN 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

96 
simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

97 
handle ERROR msg => 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26928
diff
changeset

98 
(warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term_global sg goal); 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

99 
raise Match) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

100 
in SOME thm end 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

101 
handle Match => NONE; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

102 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

103 

32010  104 
val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc; 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

105 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

106 
end; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

107 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

108 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

109 
Addsimprocs [DataFree.conv]; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

110 
*} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

111 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

112 
end 