author  huffman 
Tue, 02 Mar 2010 17:21:10 0800  
changeset 35525  fa231b86cb1e 
parent 35517  0e2ef13796a4 
child 35529  089e438b925b 
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 : 
35497  13 
Domain_Library.eq list > int > Domain_Library.eq > 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

14 
string * (string * term) list 
31227  15 

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

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

18 
(binding * (bool * binding option * typ) list * mixfix) list) list > 
35497  19 
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

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

21 

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

22 

33245  23 
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

24 
struct 
23152  25 

31227  26 
open Domain_Library; 
23152  27 

28 
infixr 0 ===>;infixr 0 ==>;infix 0 == ; 

29 
infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; 

30 
infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; 

31 

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

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

33 
val copy_tab : string Symtab.table = 
35525  34 
Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}), 
35 
(@{type_name ssum}, @{const_name "ssum_map"}), 

36 
(@{type_name sprod}, @{const_name "sprod_map"}), 

33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
33396
diff
changeset

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

38 
(@{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

39 

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

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

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

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

31288  47 
 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

48 

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

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

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

52 
(eqn as ((dname,_),cons) : eq) 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

53 
: string * (string * term) list = 
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset

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

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

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

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

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

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

60 

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

61 
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

62 
val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

63 
in 
35517  64 
(dnam, [abs_iso_ax, rep_iso_ax]) 
65 
end; 

23152  66 

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

67 

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

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

69 

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

70 
fun legacy_infer_term thy t = 
31227  71 
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

72 

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

73 
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

74 

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

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

76 

23152  77 

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

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

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

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

84 
val x_name = idx_name dnames "x"; 
23152  85 

35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

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

87 
Sign.add_path dnam 
33245  88 
#> add_axioms_infer axs 
89 
#> Sign.parent_path; 

31227  90 

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

92 
val thy = thy' > fold add_one axs; 
33801  93 

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

94 
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

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

96 
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

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

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

99 
 _ => 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

100 
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

101 
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

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

103 
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

104 
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

105 
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

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

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

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

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

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

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

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

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

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

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

116 
val dom_binds = map (Binding.name o Long_Name.base_name) dnames; 
35517  117 
val (take_info, thy) = 
118 
Domain_Take_Proofs.define_take_functions 

119 
(dom_binds ~~ map get_iso_info eqs') thy; 

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

120 

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

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

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

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

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

125 
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

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

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

128 
val image = %%: @{const_name image}; 
35499  129 
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

130 
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

131 
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

132 
in 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

133 
add_one (dnam, [("lub_take", ax)]) 
35494
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 
in 
35517  136 
val thy = fold ax_lub_take dnames thy 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

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

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

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

140 
end; (* let (add_axioms) *) 
31227  141 

23152  142 
end; (* struct *) 