author  haftmann 
Wed, 05 May 2010 18:25:34 +0200  
changeset 36692  54b64d4ad524 
parent 36241  2a4cec6bcae2 
child 37078  a1656804fcad 
permissions  rwrr 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

1 
(* Title: HOLCF/Tools/domain/domain_take_proofs.ML 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

2 
Author: Brian Huffman 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

3 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

4 
Defines take functions for the given domain equation 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

5 
and proves related theorems. 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

6 
*) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

7 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

8 
signature DOMAIN_TAKE_PROOFS = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

9 
sig 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

10 
type iso_info = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

11 
{ 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

12 
absT : typ, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

13 
repT : typ, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

14 
abs_const : term, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

15 
rep_const : term, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

16 
abs_inverse : thm, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

17 
rep_inverse : thm 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

18 
} 
35651  19 
type take_info = 
35659  20 
{ 
21 
take_consts : term list, 

35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

22 
take_defs : thm list, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

23 
chain_take_thms : thm list, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

24 
take_0_thms : thm list, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

25 
take_Suc_thms : thm list, 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

26 
deflation_take_thms : thm list, 
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

27 
finite_consts : term list, 
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

28 
finite_defs : thm list 
35651  29 
} 
35656  30 
type take_induct_info = 
31 
{ 

35659  32 
take_consts : term list, 
33 
take_defs : thm list, 

34 
chain_take_thms : thm list, 

35 
take_0_thms : thm list, 

36 
take_Suc_thms : thm list, 

37 
deflation_take_thms : thm list, 

38 
finite_consts : term list, 

39 
finite_defs : thm list, 

40 
lub_take_thms : thm list, 

41 
reach_thms : thm list, 

42 
take_lemma_thms : thm list, 

43 
is_finite : bool, 

44 
take_induct_thms : thm list 

35656  45 
} 
35651  46 
val define_take_functions : 
47 
(binding * iso_info) list > theory > take_info * theory 

35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

48 

35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

49 
val add_lub_take_theorems : 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

50 
(binding * iso_info) list > take_info > thm list > 
35656  51 
theory > take_induct_info * theory 
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

52 

35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

53 
val map_of_typ : 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

54 
theory > (typ * term) list > typ > term 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

55 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

56 
val add_map_function : 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

57 
(string * string * thm) > theory > theory 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

58 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

59 
val get_map_tab : theory > string Symtab.table 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

60 
val get_deflation_thms : theory > thm list 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

61 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

62 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

63 
structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

64 
struct 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

65 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

66 
type iso_info = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

67 
{ 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

68 
absT : typ, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

69 
repT : typ, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

70 
abs_const : term, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

71 
rep_const : term, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

72 
abs_inverse : thm, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

73 
rep_inverse : thm 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

74 
}; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

75 

35651  76 
type take_info = 
77 
{ take_consts : term list, 

78 
take_defs : thm list, 

79 
chain_take_thms : thm list, 

80 
take_0_thms : thm list, 

81 
take_Suc_thms : thm list, 

82 
deflation_take_thms : thm list, 

83 
finite_consts : term list, 

84 
finite_defs : thm list 

85 
}; 

86 

35656  87 
type take_induct_info = 
88 
{ 

35659  89 
take_consts : term list, 
90 
take_defs : thm list, 

91 
chain_take_thms : thm list, 

92 
take_0_thms : thm list, 

93 
take_Suc_thms : thm list, 

94 
deflation_take_thms : thm list, 

95 
finite_consts : term list, 

96 
finite_defs : thm list, 

97 
lub_take_thms : thm list, 

98 
reach_thms : thm list, 

99 
take_lemma_thms : thm list, 

100 
is_finite : bool, 

101 
take_induct_thms : thm list 

35656  102 
}; 
103 

35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

104 
val beta_ss = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

105 
HOL_basic_ss 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

106 
addsimps simp_thms 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

107 
addsimps [@{thm beta_cfun}] 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

108 
addsimprocs [@{simproc cont_proc}]; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

109 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

110 
val beta_tac = simp_tac beta_ss; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

111 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

112 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

113 
(******************************** theory data *********************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

114 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

115 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

116 
structure MapData = Theory_Data 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

117 
( 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

118 
(* constant names like "foo_map" *) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

119 
type T = string Symtab.table; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

120 
val empty = Symtab.empty; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

121 
val extend = I; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

122 
fun merge data = Symtab.merge (K true) data; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

123 
); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

124 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

125 
structure DeflMapData = Theory_Data 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

126 
( 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

127 
(* theorems like "deflation a ==> deflation (foo_map$a)" *) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

128 
type T = thm list; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

129 
val empty = []; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

130 
val extend = I; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

131 
val merge = Thm.merge_thms; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

132 
); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

133 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

134 
fun add_map_function (tname, map_name, deflation_map_thm) = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

135 
MapData.map (Symtab.insert (K true) (tname, map_name)) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

136 
#> DeflMapData.map (Thm.add_thm deflation_map_thm); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

137 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

138 
val get_map_tab = MapData.get; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

139 
val get_deflation_thms = DeflMapData.get; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

140 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

141 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

142 
(************************** building types and terms **************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

143 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

144 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

145 
open HOLCF_Library; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

146 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

147 
infixr 6 >>; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

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

149 
infix 9 `; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

150 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

151 
fun mapT (T as Type (_, Ts)) = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

152 
(map (fn T => T >> T) Ts) >> (T >> T) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

153 
 mapT T = T >> T; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

154 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

155 
fun mk_deflation t = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

156 
Const (@{const_name deflation}, Term.fastype_of t > boolT) $ t; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

157 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

158 
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

159 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

160 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

161 
(****************************** isomorphism info ******************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

162 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

163 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

164 
fun deflation_abs_rep (info : iso_info) : thm = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

165 
let 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

166 
val abs_iso = #abs_inverse info; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

167 
val rep_iso = #rep_inverse info; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

168 
val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

169 
in 
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset

170 
Drule.zero_var_indexes thm 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

171 
end 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

172 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

173 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

174 
(********************* building map functions over types **********************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

175 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

176 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

177 
fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

178 
let 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

179 
val map_tab = get_map_tab thy; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

180 
fun auto T = T >> T; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

181 
fun map_of T = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

182 
case AList.lookup (op =) sub T of 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

183 
SOME m => (m, true)  NONE => map_of' T 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

184 
and map_of' (T as (Type (c, Ts))) = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

185 
(case Symtab.lookup map_tab c of 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

186 
SOME map_name => 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

187 
let 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

188 
val map_type = map auto Ts >> auto T; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

189 
val (ms, bs) = map_split map_of Ts; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

190 
in 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

191 
if exists I bs 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

192 
then (list_ccomb (Const (map_name, map_type), ms), true) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

193 
else (mk_ID T, false) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

194 
end 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

195 
 NONE => (mk_ID T, false)) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

196 
 map_of' T = (mk_ID T, false); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

197 
in 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

198 
fst (map_of T) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

199 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

200 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

201 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

202 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

203 
(********************* declaring definitions and theorems *********************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

204 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

205 

35773  206 
fun add_qualified_def name (dbind, eqn) = 
207 
yield_singleton (PureThy.add_defs false) 

208 
((Binding.qualified true name dbind, eqn), []); 

35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

209 

35773  210 
fun add_qualified_thm name (dbind, thm) = 
211 
yield_singleton PureThy.add_thms 

212 
((Binding.qualified true name dbind, thm), []); 

35650  213 

35773  214 
fun add_qualified_simp_thm name (dbind, thm) = 
215 
yield_singleton PureThy.add_thms 

216 
((Binding.qualified true name dbind, thm), [Simplifier.simp_add]); 

35573  217 

35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

218 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

219 
(************************** defining take functions ***************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

220 
(******************************************************************************) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

221 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

222 
fun define_take_functions 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

223 
(spec : (binding * iso_info) list) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

224 
(thy : theory) = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

225 
let 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

226 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

227 
(* retrieve components of spec *) 
35773  228 
val dbinds = map fst spec; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

229 
val iso_infos = map snd spec; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

230 
val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

231 
val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

232 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

233 
(* get table of map functions *) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

234 
val map_tab = MapData.get thy; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

235 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

236 
fun mk_projs [] t = [] 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

237 
 mk_projs (x::[]) t = [(x, t)] 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

238 
 mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

239 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

240 
fun mk_cfcomp2 ((rep_const, abs_const), f) = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

241 
mk_cfcomp (abs_const, mk_cfcomp (f, rep_const)); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

242 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

243 
(* define take functional *) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

244 
val newTs : typ list = map fst dom_eqns; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

245 
val copy_arg_type = mk_tupleT (map (fn T => T >> T) newTs); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

246 
val copy_arg = Free ("f", copy_arg_type); 
35773  247 
val copy_args = map snd (mk_projs dbinds copy_arg); 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

248 
fun one_copy_rhs (rep_abs, (lhsT, rhsT)) = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

249 
let 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

250 
val body = map_of_typ thy (newTs ~~ copy_args) rhsT; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

251 
in 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

252 
mk_cfcomp2 (rep_abs, body) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

253 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

254 
val take_functional = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

255 
big_lambda copy_arg 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

256 
(mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns))); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

257 
val take_rhss = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

258 
let 
35557
5da670d57118
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset

259 
val n = Free ("n", HOLogic.natT); 
5da670d57118
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset

260 
val rhs = mk_iterate (n, take_functional); 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

261 
in 
35773  262 
map (lambda n o snd) (mk_projs dbinds rhs) 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

263 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

264 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

265 
(* define take constants *) 
35773  266 
fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy = 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

267 
let 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

268 
val take_type = HOLogic.natT > lhsT >> lhsT; 
35773  269 
val take_bind = Binding.suffix_name "_take" dbind; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

270 
val (take_const, thy) = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

271 
Sign.declare_const ((take_bind, take_type), NoSyn) thy; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

272 
val take_eqn = Logic.mk_equals (take_const, take_rhs); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

273 
val (take_def_thm, thy) = 
35773  274 
add_qualified_def "take_def" (dbind, take_eqn) thy; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

275 
in ((take_const, take_def_thm), thy) end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

276 
val ((take_consts, take_defs), thy) = thy 
35773  277 
> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns) 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

278 
>> ListPair.unzip; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

279 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

280 
(* prove chain_take lemmas *) 
35773  281 
fun prove_chain_take (take_const, dbind) thy = 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

282 
let 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

283 
val goal = mk_trp (mk_chain take_const); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

284 
val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd}; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

285 
val tac = simp_tac (HOL_basic_ss addsimps rules) 1; 
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

286 
val thm = Goal.prove_global thy [] [] goal (K tac); 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

287 
in 
35773  288 
add_qualified_simp_thm "chain_take" (dbind, thm) thy 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

289 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

290 
val (chain_take_thms, thy) = 
35773  291 
fold_map prove_chain_take (take_consts ~~ dbinds) thy; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

292 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

293 
(* prove take_0 lemmas *) 
35773  294 
fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy = 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

295 
let 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

296 
val lhs = take_const $ @{term "0::nat"}; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

297 
val goal = mk_eqs (lhs, mk_bottom (lhsT >> lhsT)); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

298 
val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict}; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

299 
val tac = simp_tac (HOL_basic_ss addsimps rules) 1; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

300 
val take_0_thm = Goal.prove_global thy [] [] goal (K tac); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

301 
in 
35773  302 
add_qualified_thm "take_0" (dbind, take_0_thm) thy 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

303 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

304 
val (take_0_thms, thy) = 
35773  305 
fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

306 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

307 
(* prove take_Suc lemmas *) 
35557
5da670d57118
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset

308 
val n = Free ("n", natT); 
5da670d57118
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset

309 
val take_is = map (fn t => t $ n) take_consts; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

310 
fun prove_take_Suc 
35773  311 
(((take_const, rep_abs), dbind), (lhsT, rhsT)) thy = 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

312 
let 
35557
5da670d57118
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset

313 
val lhs = take_const $ (@{term Suc} $ n); 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

314 
val body = map_of_typ thy (newTs ~~ take_is) rhsT; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

315 
val rhs = mk_cfcomp2 (rep_abs, body); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

316 
val goal = mk_eqs (lhs, rhs); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

317 
val simps = @{thms iterate_Suc fst_conv snd_conv} 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

318 
val rules = take_defs @ simps; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

319 
val tac = simp_tac (beta_ss addsimps rules) 1; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

320 
val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

321 
in 
35773  322 
add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

323 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

324 
val (take_Suc_thms, thy) = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

325 
fold_map prove_take_Suc 
35773  326 
(take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

327 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

328 
(* prove deflation theorems for take functions *) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

329 
val deflation_abs_rep_thms = map deflation_abs_rep iso_infos; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

330 
val deflation_take_thm = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

331 
let 
35557
5da670d57118
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset

332 
val n = Free ("n", natT); 
5da670d57118
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset

333 
fun mk_goal take_const = mk_deflation (take_const $ n); 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

334 
val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)); 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

335 
val adm_rules = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

336 
@{thms adm_conj adm_subst [OF _ adm_deflation] 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

337 
cont2cont_fst cont2cont_snd cont_id}; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

338 
val bottom_rules = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

339 
take_0_thms @ @{thms deflation_UU simp_thms}; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

340 
val deflation_rules = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

341 
@{thms conjI deflation_ID} 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

342 
@ deflation_abs_rep_thms 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

343 
@ DeflMapData.get thy; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

344 
in 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

345 
Goal.prove_global thy [] [] goal (fn _ => 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

346 
EVERY 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

347 
[rtac @{thm nat.induct} 1, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

348 
simp_tac (HOL_basic_ss addsimps bottom_rules) 1, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

349 
asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

350 
REPEAT (etac @{thm conjE} 1 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

351 
ORELSE resolve_tac deflation_rules 1 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

352 
ORELSE atac 1)]) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

353 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

354 
fun conjuncts [] thm = [] 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

355 
 conjuncts (n::[]) thm = [(n, thm)] 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

356 
 conjuncts (n::ns) thm = let 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

357 
val thmL = thm RS @{thm conjunct1}; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

358 
val thmR = thm RS @{thm conjunct2}; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

359 
in (n, thmL):: conjuncts ns thmR end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

360 
val (deflation_take_thms, thy) = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

361 
fold_map (add_qualified_thm "deflation_take") 
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset

362 
(map (apsnd Drule.zero_var_indexes) 
35773  363 
(conjuncts dbinds deflation_take_thm)) thy; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

364 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

365 
(* prove strictness of take functions *) 
35773  366 
fun prove_take_strict (deflation_take, dbind) thy = 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

367 
let 
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

368 
val take_strict_thm = 
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset

369 
Drule.zero_var_indexes 
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset

370 
(@{thm deflation_strict} OF [deflation_take]); 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

371 
in 
35773  372 
add_qualified_thm "take_strict" (dbind, take_strict_thm) thy 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

373 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

374 
val (take_strict_thms, thy) = 
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

375 
fold_map prove_take_strict 
35773  376 
(deflation_take_thms ~~ dbinds) thy; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

377 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

378 
(* prove take/take rules *) 
35773  379 
fun prove_take_take ((chain_take, deflation_take), dbind) thy = 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

380 
let 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

381 
val take_take_thm = 
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset

382 
Drule.zero_var_indexes 
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset

383 
(@{thm deflation_chain_min} OF [chain_take, deflation_take]); 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

384 
in 
35773  385 
add_qualified_thm "take_take" (dbind, take_take_thm) thy 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

386 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

387 
val (take_take_thms, thy) = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

388 
fold_map prove_take_take 
35773  389 
(chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy; 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

390 

35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

391 
(* prove take_below rules *) 
35773  392 
fun prove_take_below (deflation_take, dbind) thy = 
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

393 
let 
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

394 
val take_below_thm = 
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset

395 
Drule.zero_var_indexes 
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset

396 
(@{thm deflation.below} OF [deflation_take]); 
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

397 
in 
35773  398 
add_qualified_thm "take_below" (dbind, take_below_thm) thy 
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

399 
end; 
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

400 
val (take_below_thms, thy) = 
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

401 
fold_map prove_take_below 
35773  402 
(deflation_take_thms ~~ dbinds) thy; 
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset

403 

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

404 
(* define finiteness predicates *) 
35773  405 
fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy = 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

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

407 
val finite_type = lhsT > boolT; 
35773  408 
val finite_bind = Binding.suffix_name "_finite" dbind; 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

409 
val (finite_const, thy) = 
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

410 
Sign.declare_const ((finite_bind, finite_type), NoSyn) thy; 
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

411 
val x = Free ("x", lhsT); 
35557
5da670d57118
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset

412 
val n = Free ("n", natT); 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

413 
val finite_rhs = 
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

414 
lambda x (HOLogic.exists_const natT $ 
35557
5da670d57118
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset

415 
(lambda n (mk_eq (mk_capply (take_const $ n, x), x)))); 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

416 
val finite_eqn = Logic.mk_equals (finite_const, finite_rhs); 
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

417 
val (finite_def_thm, thy) = 
35773  418 
add_qualified_def "finite_def" (dbind, finite_eqn) thy; 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

419 
in ((finite_const, finite_def_thm), thy) end; 
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

420 
val ((finite_consts, finite_defs), thy) = thy 
35773  421 
> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns) 
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

422 
>> ListPair.unzip; 
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

423 

35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

424 
val result = 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

425 
{ 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

426 
take_consts = take_consts, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

427 
take_defs = take_defs, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

428 
chain_take_thms = chain_take_thms, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

429 
take_0_thms = take_0_thms, 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

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

431 
deflation_take_thms = deflation_take_thms, 
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

432 
finite_consts = finite_consts, 
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset

433 
finite_defs = finite_defs 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

434 
}; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

435 

a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

436 
in 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

437 
(result, thy) 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

438 
end; 
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

439 

35655  440 
fun prove_finite_take_induct 
441 
(spec : (binding * iso_info) list) 

442 
(take_info : take_info) 

443 
(lub_take_thms : thm list) 

444 
(thy : theory) = 

445 
let 

35773  446 
val dbinds = map fst spec; 
35655  447 
val iso_infos = map snd spec; 
448 
val absTs = map #absT iso_infos; 

449 
val {take_consts, ...} = take_info; 

450 
val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info; 

451 
val {finite_consts, finite_defs, ...} = take_info; 

452 

453 
val decisive_lemma = 

454 
let 

455 
fun iso_locale info = 

456 
@{thm iso.intro} OF [#abs_inverse info, #rep_inverse info]; 

457 
val iso_locale_thms = map iso_locale iso_infos; 

458 
val decisive_abs_rep_thms = 

459 
map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms; 

460 
val n = Free ("n", @{typ nat}); 

461 
fun mk_decisive t = 

462 
Const (@{const_name decisive}, fastype_of t > boolT) $ t; 

463 
fun f take_const = mk_decisive (take_const $ n); 

464 
val goal = mk_trp (foldr1 mk_conj (map f take_consts)); 

465 
val rules0 = @{thm decisive_bottom} :: take_0_thms; 

466 
val rules1 = 

467 
take_Suc_thms @ decisive_abs_rep_thms 

468 
@ @{thms decisive_ID decisive_ssum_map decisive_sprod_map}; 

469 
val tac = EVERY [ 

470 
rtac @{thm nat.induct} 1, 

471 
simp_tac (HOL_ss addsimps rules0) 1, 

472 
asm_simp_tac (HOL_ss addsimps rules1) 1]; 

473 
in Goal.prove_global thy [] [] goal (K tac) end; 

474 
fun conjuncts 1 thm = [thm] 

475 
 conjuncts n thm = let 

476 
val thmL = thm RS @{thm conjunct1}; 

477 
val thmR = thm RS @{thm conjunct2}; 

478 
in thmL :: conjuncts (n1) thmR end; 

479 
val decisive_thms = conjuncts (length spec) decisive_lemma; 

480 

481 
fun prove_finite_thm (absT, finite_const) = 

482 
let 

483 
val goal = mk_trp (finite_const $ Free ("x", absT)); 

484 
val tac = 

485 
EVERY [ 

486 
rewrite_goals_tac finite_defs, 

487 
rtac @{thm lub_ID_finite} 1, 

488 
resolve_tac chain_take_thms 1, 

489 
resolve_tac lub_take_thms 1, 

490 
resolve_tac decisive_thms 1]; 

491 
in 

492 
Goal.prove_global thy [] [] goal (K tac) 

493 
end; 

494 
val finite_thms = 

495 
map prove_finite_thm (absTs ~~ finite_consts); 

496 

497 
fun prove_take_induct ((ch_take, lub_take), decisive) = 

498 
Drule.export_without_context 

499 
(@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]); 

500 
val take_induct_thms = 

501 
map prove_take_induct 

502 
(chain_take_thms ~~ lub_take_thms ~~ decisive_thms); 

503 

504 
val thy = thy 

505 
> fold (snd oo add_qualified_thm "finite") 

35773  506 
(dbinds ~~ finite_thms) 
35655  507 
> fold (snd oo add_qualified_thm "take_induct") 
35773  508 
(dbinds ~~ take_induct_thms); 
35655  509 
in 
510 
((finite_thms, take_induct_thms), thy) 

511 
end; 

512 

35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

513 
fun add_lub_take_theorems 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

514 
(spec : (binding * iso_info) list) 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

515 
(take_info : take_info) 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

516 
(lub_take_thms : thm list) 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

517 
(thy : theory) = 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

518 
let 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

519 

7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

520 
(* retrieve components of spec *) 
35773  521 
val dbinds = map fst spec; 
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

522 
val iso_infos = map snd spec; 
35655  523 
val absTs = map #absT iso_infos; 
524 
val repTs = map #repT iso_infos; 

525 
val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info; 

35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

526 
val {chain_take_thms, deflation_take_thms, ...} = take_info; 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

527 

7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

528 
(* prove take lemmas *) 
35773  529 
fun prove_take_lemma ((chain_take, lub_take), dbind) thy = 
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

530 
let 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

531 
val take_lemma = 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

532 
Drule.export_without_context 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

533 
(@{thm lub_ID_take_lemma} OF [chain_take, lub_take]); 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

534 
in 
35773  535 
add_qualified_thm "take_lemma" (dbind, take_lemma) thy 
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

536 
end; 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

537 
val (take_lemma_thms, thy) = 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

538 
fold_map prove_take_lemma 
35773  539 
(chain_take_thms ~~ lub_take_thms ~~ dbinds) thy; 
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

540 

7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

541 
(* prove reach lemmas *) 
35773  542 
fun prove_reach_lemma ((chain_take, lub_take), dbind) thy = 
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

543 
let 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

544 
val thm = 
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset

545 
Drule.zero_var_indexes 
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

546 
(@{thm lub_ID_reach} OF [chain_take, lub_take]); 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

547 
in 
35773  548 
add_qualified_thm "reach" (dbind, thm) thy 
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

549 
end; 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

550 
val (reach_thms, thy) = 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

551 
fold_map prove_reach_lemma 
35773  552 
(chain_take_thms ~~ lub_take_thms ~~ dbinds) thy; 
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

553 

35655  554 
(* test for finiteness of domain definitions *) 
555 
local 

556 
val types = [@{type_name ssum}, @{type_name sprod}]; 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36241
diff
changeset

557 
fun finite d T = if member (op =) absTs T then d else finite' d T 
35655  558 
and finite' d (Type (c, Ts)) = 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36241
diff
changeset

559 
let val d' = d andalso member (op =) types c; 
35655  560 
in forall (finite d') Ts end 
561 
 finite' d _ = true; 

562 
in 

563 
val is_finite = forall (finite true) repTs; 

564 
end; 

35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

565 

35655  566 
val ((finite_thms, take_induct_thms), thy) = 
567 
if is_finite 

568 
then 

569 
let 

570 
val ((finites, take_inducts), thy) = 

571 
prove_finite_take_induct spec take_info lub_take_thms thy; 

572 
in 

573 
((SOME finites, take_inducts), thy) 

574 
end 

575 
else 

576 
let 

577 
fun prove_take_induct (chain_take, lub_take) = 

36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset

578 
Drule.zero_var_indexes 
35655  579 
(@{thm lub_ID_take_induct} OF [chain_take, lub_take]); 
580 
val take_inducts = 

581 
map prove_take_induct (chain_take_thms ~~ lub_take_thms); 

582 
val thy = fold (snd oo add_qualified_thm "take_induct") 

35773  583 
(dbinds ~~ take_inducts) thy; 
35655  584 
in 
585 
((NONE, take_inducts), thy) 

586 
end; 

587 

35656  588 
val result = 
589 
{ 

35659  590 
take_consts = #take_consts take_info, 
591 
take_defs = #take_defs take_info, 

592 
chain_take_thms = #chain_take_thms take_info, 

593 
take_0_thms = #take_0_thms take_info, 

594 
take_Suc_thms = #take_Suc_thms take_info, 

595 
deflation_take_thms = #deflation_take_thms take_info, 

596 
finite_consts = #finite_consts take_info, 

597 
finite_defs = #finite_defs take_info, 

598 
lub_take_thms = lub_take_thms, 

599 
reach_thms = reach_thms, 

600 
take_lemma_thms = take_lemma_thms, 

601 
is_finite = is_finite, 

602 
take_induct_thms = take_induct_thms 

35656  603 
}; 
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

604 
in 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

605 
(result, thy) 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

606 
end; 
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset

607 

35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset

608 
end; 