author  huffman 
Tue, 02 Mar 2010 13:50:23 0800  
changeset 35514  a2cfa413eaab 
parent 35513  89eddccbb93d 
child 35515  d631dc53ede0 
permissions  rwrr 
32126  1 
(* Title: HOLCF/Tools/Domain/domain_axioms.ML 
23152  2 
Author: David von Oheimb 
3 

4 
Syntax generator for domain command. 

5 
*) 

6 

30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

7 
signature DOMAIN_AXIOMS = 
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

8 
sig 
33801  9 
val copy_of_dtyp : 
10 
string Symtab.table > (int > term) > Datatype.dtyp > term 

31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

11 

31288  12 
val calc_axioms : 
35513  13 
bool > 
35497  14 
Domain_Library.eq list > int > Domain_Library.eq > 
31288  15 
string * (string * term) list * (string * term) list 
31227  16 

31288  17 
val add_axioms : 
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

18 
bool > 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

19 
((string * typ list) * 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

20 
(binding * (bool * binding option * typ) list * mixfix) list) list > 
35497  21 
Domain_Library.eq list > theory > theory 
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

22 
end; 
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

23 

dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

24 

33245  25 
structure Domain_Axioms : DOMAIN_AXIOMS = 
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

26 
struct 
23152  27 

31227  28 
open Domain_Library; 
23152  29 

30 
infixr 0 ===>;infixr 0 ==>;infix 0 == ; 

31 
infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; 

32 
infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; 

33 

31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

34 
(* FIXME: use theory data for this *) 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

35 
val copy_tab : string Symtab.table = 
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
33396
diff
changeset

36 
Symtab.make [(@{type_name ">"}, @{const_name "cfun_map"}), 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
33396
diff
changeset

37 
(@{type_name "++"}, @{const_name "ssum_map"}), 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
33396
diff
changeset

38 
(@{type_name "**"}, @{const_name "sprod_map"}), 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
33396
diff
changeset

39 
(@{type_name "*"}, @{const_name "cprod_map"}), 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
33396
diff
changeset

40 
(@{type_name "u"}, @{const_name "u_map"})]; 
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

41 

33801  42 
fun copy_of_dtyp tab r dt = 
33971  43 
if Datatype_Aux.is_rec_type dt then copy tab r dt else ID 
44 
and copy tab r (Datatype_Aux.DtRec i) = r i 

45 
 copy tab r (Datatype_Aux.DtTFree a) = ID 

46 
 copy tab r (Datatype_Aux.DtType (c, ds)) = 

33801  47 
case Symtab.lookup tab c of 
48 
SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds) 

31288  49 
 NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); 
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

50 

31227  51 
fun calc_axioms 
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

52 
(definitional : bool) 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

53 
(eqs : eq list) 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

54 
(n : int) 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

55 
(eqn as ((dname,_),cons) : eq) 
31227  56 
: string * (string * term) list * (string * term) list = 
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

57 
let 
23152  58 

33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

59 
(*  axioms and definitions concerning the isomorphism  *) 
31227  60 

33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

61 
val dc_abs = %%:(dname^"_abs"); 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

62 
val dc_rep = %%:(dname^"_rep"); 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

63 
val x_name'= "x"; 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

64 
val x_name = idx_name eqs x_name' (n+1); 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

65 
val dnam = Long_Name.base_name dname; 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

66 

46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

67 
val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

68 
val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); 
23152  69 

33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

70 
(*  axiom and definitions concerning induction  *) 
23152  71 

33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

72 
val finite_def = 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

73 
("finite_def", 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

74 
%%:(dname^"_finite") == 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

75 
mk_lam(x_name, 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

76 
mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); 
23152  77 

33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

78 
in (dnam, 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

79 
(if definitional then [] else [abs_iso_ax, rep_iso_ax]), 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

80 
[finite_def]) 
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

81 
end; (* let (calc_axioms) *) 
23152  82 

30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

83 

0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

84 
(* legacy type inference *) 
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

85 

0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

86 
fun legacy_infer_term thy t = 
31227  87 
singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); 
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

88 

0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

89 
fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); 
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

90 

0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

91 
fun infer_props thy = map (apsnd (legacy_infer_prop thy)); 
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

92 

23152  93 

29585  94 
fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x); 
23152  95 
fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; 
96 

29585  97 
fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); 
23152  98 
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; 
99 

35497  100 
fun add_axioms definitional eqs' (eqs : eq list) thy' = 
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

101 
let 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

102 
val dnames = map (fst o fst) eqs; 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

103 
val x_name = idx_name dnames "x"; 
23152  104 

33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

105 
fun add_one (dnam, axs, dfs) = 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

106 
Sign.add_path dnam 
33245  107 
#> add_axioms_infer axs 
108 
#> Sign.parent_path; 

31227  109 

35513  110 
val axs = mapn (calc_axioms definitional eqs) 0 eqs; 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

111 
val thy = thy' > fold add_one axs; 
33801  112 

35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

113 
fun get_iso_info ((dname, tyvars), cons') = 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

114 
let 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

115 
fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

116 
fun prod (_,args,_) = 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

117 
case args of [] => oneT 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

118 
 _ => foldr1 mk_sprodT (map opt_lazy args); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

119 
val ax_abs_iso = PureThy.get_thm thy (dname ^ ".abs_iso"); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

120 
val ax_rep_iso = PureThy.get_thm thy (dname ^ ".rep_iso"); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

121 
val lhsT = Type(dname,tyvars); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

122 
val rhsT = foldr1 mk_ssumT (map prod cons'); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

123 
val rep_const = Const(dname^"_rep", lhsT >> rhsT); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

124 
val abs_const = Const(dname^"_abs", rhsT >> lhsT); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

125 
in 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

126 
{ 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

127 
absT = lhsT, 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

128 
repT = rhsT, 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

129 
abs_const = abs_const, 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

130 
rep_const = rep_const, 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

131 
abs_inverse = ax_abs_iso, 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

132 
rep_inverse = ax_rep_iso 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

133 
} 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

134 
end; 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

135 
val dom_binds = map (Binding.name o Long_Name.base_name) dnames; 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

136 
val thy = 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

137 
if definitional then thy 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35513
diff
changeset

138 
else snd (Domain_Take_Proofs.define_take_functions 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

139 
(dom_binds ~~ map get_iso_info eqs') thy); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

140 

45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

141 
fun add_one' (dnam, axs, dfs) = 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

142 
Sign.add_path dnam 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

143 
#> add_defs_infer dfs 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

144 
#> Sign.parent_path; 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

145 
val thy = fold add_one' axs thy; 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

146 

45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

147 
(* declare lub_take axioms *) 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

148 
local 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

149 
fun ax_lub_take dname = 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

150 
let 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

151 
val dnam : string = Long_Name.base_name dname; 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

152 
val take_const = %%:(dname^"_take"); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

153 
val lub = %%: @{const_name lub}; 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

154 
val image = %%: @{const_name image}; 
35499  155 
val UNIV = @{term "UNIV :: nat set"}; 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

156 
val lhs = lub $ (image $ take_const $ UNIV); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

157 
val ax = mk_trp (lhs === ID); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

158 
in 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

159 
add_one (dnam, [("lub_take", ax)], []) 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

160 
end 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

161 
in 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

162 
val thy = 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

163 
if definitional then thy 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

164 
else fold ax_lub_take dnames thy 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

165 
end; 
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

166 
in 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

167 
thy 
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

168 
end; (* let (add_axioms) *) 
31227  169 

23152  170 
end; (* struct *) 