author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 48891  c0eafbd55de3 
child 51717  9e7d1c139569 
permissions  rwrr 
41777  1 
(* Title: ZF/Datatype_ZF.thy 
26056
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 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
41777
diff
changeset

10 
keywords "datatype" "codatatype" :: thy_decl 
26056
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 

48891  13 
ML_file "Tools/datatype_package.ML" 
14 

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

16 
(*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

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

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

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

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

21 
@{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

22 
@{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

23 

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

24 

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

25 
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

26 
@{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

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

28 

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

29 

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

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

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

32 
(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

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

34 
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

35 
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

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

37 

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

38 

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

39 
(*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

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

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

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

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

44 
@{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

45 
@{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

46 

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

47 
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

48 
@{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

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

50 

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

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

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

53 
(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

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

55 
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

56 
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

57 
val coind = true); 
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 

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

60 

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

61 
(*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

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

63 
struct 
32740  64 
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

65 

38522  66 
fun mk_new ([],[]) = Const(@{const_name True},FOLogic.oT) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

67 
 mk_new (largs,rargs) = 
32765  68 
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

69 
(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

70 

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

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

72 

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

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

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

75 
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

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

77 
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

78 
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

79 
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

80 
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

81 
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

82 
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

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

84 
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

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

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

87 
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

88 
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

89 
if lname = rname then mk_new (largs, rargs) 
38522  90 
else Const(@{const_name False},FOLogic.oT) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

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

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

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

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

95 
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

96 
val thm = Goal.prove (Simplifier.the_context ss) [] [] goal 
35409  97 
(fn _ => rtac @{thm iff_reflection} 1 THEN 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

98 
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

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

100 
(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

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

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

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

104 

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

105 

38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
38522
diff
changeset

106 
val conv = Simplifier.simproc_global @{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

107 

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

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

109 

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 
Addsimprocs [DataFree.conv]; 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

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

113 

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

114 
end 