author  wenzelm 
Wed, 17 Mar 1999 13:49:14 +0100  
changeset 6383  45bb139e6ceb 
parent 6357  12448b8f92fb 
child 6690  acbcf8085166 
permissions  rwrr 
4866  1 
(* Title: HOL/Tools/typedef_package.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

6357  5 
Gordon/HOLstyle type definitions. 
4866  6 
*) 
7 

8 
signature TYPEDEF_PACKAGE = 

9 
sig 

5697  10 
val quiet_mode: bool ref 
5104  11 
val add_typedecls: (bstring * string list * mixfix) list > theory > theory 
4866  12 
val add_typedef: string > bstring * string list * mixfix > 
13 
string > string list > thm list > tactic option > theory > theory 

14 
val add_typedef_i: string > bstring * string list * mixfix > 

15 
term > string list > thm list > tactic option > theory > theory 

5180
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

16 
val add_typedef_i_no_def: string > bstring * string list * mixfix > 
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

17 
term > string list > thm list > tactic option > theory > theory 
6383  18 
val typedef_proof: string > bstring * string list * mixfix > string > theory > ProofHistory.T 
19 
val typedef_proof_i: string > bstring * string list * mixfix > term > theory > ProofHistory.T 

4866  20 
end; 
21 

22 
structure TypedefPackage: TYPEDEF_PACKAGE = 

23 
struct 

24 

25 

5104  26 
(** type declarations **) 
27 

28 
fun add_typedecls decls thy = 

29 
let 

30 
val full = Sign.full_name (Theory.sign_of thy); 

31 

32 
fun arity_of (raw_name, args, mx) = 

33 
(full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS); 

34 
in 

35 
thy 

36 
> PureThy.add_typedecls decls 

37 
> Theory.add_arities_i (map arity_of decls) 

38 
end; 

39 

40 

41 

42 
(** type definitions **) 

43 

5697  44 
(* messages *) 
45 

46 
val quiet_mode = ref false; 

47 
fun message s = if ! quiet_mode then () else writeln s; 

48 

49 

6383  50 
(* nonemptiness of set *) (*exception ERROR*) 
4866  51 

6383  52 
fun check_nonempty cset thm = 
4866  53 
let 
6383  54 
val {t, sign, maxidx, ...} = Thm.rep_cterm cset; 
55 
val {prop, ...} = Thm.rep_thm (Thm.transfer_sg sign (Drule.standard thm)); 

56 
val matches = Pattern.matches (Sign.tsig_of sign); 

57 
in 

58 
(case try (HOLogic.dest_mem o HOLogic.dest_Trueprop) prop of 

59 
None => raise ERROR 

60 
 Some (_, A) => if matches (Logic.incr_indexes ([], maxidx) A, t) then () else raise ERROR) 

61 
end handle ERROR => error ("Bad nonemptiness theorem " ^ Display.string_of_thm thm ^ 

62 
"\nfor set " ^ quote (Display.string_of_cterm cset)); 

63 

64 
fun goal_nonempty cset = 

65 
let 

66 
val {T = setT, t = A, maxidx, sign} = Thm.rep_cterm cset; 

4866  67 
val T = HOLogic.dest_setT setT; 
6383  68 
in Thm.cterm_of sign (HOLogic.mk_Trueprop (HOLogic.mk_mem (Var (("x", maxidx + 1), T), A))) end; 
69 

70 
fun prove_nonempty thy cset (witn_names, witn_thms, witn_tac) = 

71 
let 

72 
val is_def = Logic.is_equals o #prop o Thm.rep_thm; 

73 
val thms = PureThy.get_thmss thy witn_names @ witn_thms; 

4866  74 
val tac = 
75 
TRY (rewrite_goals_tac (filter is_def thms)) THEN 

76 
TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN 

6383  77 
if_none witn_tac (TRY (ALLGOALS (CLASET' blast_tac))); 
4866  78 
in 
6383  79 
message ("Proving nonemptiness of set " ^ quote (string_of_cterm cset) ^ " ..."); 
80 
prove_goalw_cterm [] (goal_nonempty cset) (K [tac]) 

81 
end handle ERROR => error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset)); 

4866  82 

83 

6383  84 
(* prepare_typedef *) 
85 

86 
fun read_term sg used s = 

87 
#1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termTVar)); 

4866  88 

6383  89 
fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg; 
90 

91 
fun err_in_typedef name = 

92 
error ("The error(s) above occurred in typedef " ^ quote name); 

93 

94 
fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set thy = 

4866  95 
let 
4970  96 
val _ = Theory.requires thy "Set" "typedefs"; 
6383  97 
val sign = Theory.sign_of thy; 
4866  98 
val full_name = Sign.full_name sign; 
99 

100 
(*rhs*) 

6383  101 
val cset = prep_term sign vs raw_set; 
102 
val {T = setT, t = set, ...} = Thm.rep_cterm cset; 

4866  103 
val rhs_tfrees = term_tfrees set; 
104 
val oldT = HOLogic.dest_setT setT handle TYPE _ => 

105 
error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT)); 

106 

107 
(*lhs*) 

6383  108 
val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs; 
4866  109 
val tname = Syntax.type_name t mx; 
110 
val newT = Type (full_name tname, map TFree lhs_tfrees); 

111 

112 
val Rep_name = "Rep_" ^ name; 

113 
val Abs_name = "Abs_" ^ name; 

114 
val setC = Const (full_name name, setT); 

115 
val RepC = Const (full_name Rep_name, newT > oldT); 

116 
val AbsC = Const (full_name Abs_name, oldT > newT); 

117 
val x_new = Free ("x", newT); 

118 
val y_old = Free ("y", oldT); 

5180
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

119 
val set' = if no_def then set else setC; 
4866  120 

121 
(*axioms*) 

5180
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

122 
val rep_type = HOLogic.mk_Trueprop (HOLogic.mk_mem (RepC $ x_new, set')); 
4866  123 
val rep_type_inv = HOLogic.mk_Trueprop (HOLogic.mk_eq (AbsC $ (RepC $ x_new), x_new)); 
5180
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

124 
val abs_type_inv = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (y_old, set')), 
4866  125 
HOLogic.mk_Trueprop (HOLogic.mk_eq (RepC $ (AbsC $ y_old), y_old))); 
126 

6383  127 
(*theory extender*) 
128 
fun do_typedef theory = 

129 
theory 

130 
> Theory.assert_super thy 

131 
> add_typedecls [(t, vs, mx)] 

132 
> Theory.add_consts_i 

133 
((if no_def then [] else [(name, setT, NoSyn)]) @ 

134 
[(Rep_name, newT > oldT, NoSyn), 

135 
(Abs_name, oldT > newT, NoSyn)]) 

136 
> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes) 

137 
[Logic.mk_defpair (setC, set)]) 

138 
> (PureThy.add_axioms_i o map Thm.no_attributes) 

139 
[(Rep_name, rep_type), 

140 
(Rep_name ^ "_inverse", rep_type_inv), 

141 
(Abs_name ^ "_inverse", abs_type_inv)] 

142 
handle ERROR => err_in_typedef name; 

143 

4866  144 

145 
(* errors *) 

146 

147 
fun show_names pairs = commas_quote (map fst pairs); 

148 

149 
val illegal_vars = 

150 
if null (term_vars set) andalso null (term_tvars set) then [] 

151 
else ["Illegal schematic variable(s) on rhs"]; 

152 

153 
val dup_lhs_tfrees = 

154 
(case duplicates lhs_tfrees of [] => [] 

155 
 dups => ["Duplicate type variables on lhs: " ^ show_names dups]); 

156 

157 
val extra_rhs_tfrees = 

158 
(case gen_rems (op =) (rhs_tfrees, lhs_tfrees) of [] => [] 

159 
 extras => ["Extra type variables on rhs: " ^ show_names extras]); 

160 

161 
val illegal_frees = 

162 
(case term_frees set of [] => [] 

163 
 xs => ["Illegal variables on rhs: " ^ show_names (map dest_Free xs)]); 

164 

165 
val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees; 

166 
in 

6383  167 
if null errs then () else error (cat_lines errs); 
168 
(cset, do_typedef) 

169 
end handle ERROR => err_in_typedef name; 

4866  170 

171 

6383  172 
(* add_typedef interfaces *) 
4866  173 

6383  174 
fun gen_add_typedef prep_term no_def name typ set names thms tac thy = 
175 
let 

176 
val (cset, do_typedef) = prepare_typedef prep_term no_def name typ set thy; 

177 
val result = prove_nonempty thy cset (names, thms, tac); 

178 
in check_nonempty cset result; thy > do_typedef end; 

4866  179 

5180
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

180 
val add_typedef = gen_add_typedef read_term false; 
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

181 
val add_typedef_i = gen_add_typedef cert_term false; 
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

182 
val add_typedef_i_no_def = gen_add_typedef cert_term true; 
4866  183 

184 

6383  185 
(* typedef_proof interface *) 
186 

187 
fun typedef_attribute cset do_typedef (thy, thm) = 

188 
(check_nonempty cset thm; (thy > do_typedef, thm)); 

6357  189 

6383  190 
fun gen_typedef_proof prep_term name typ set thy = 
191 
let 

192 
val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy; 

193 
val goal = Thm.term_of (goal_nonempty cset); 

194 
in 

195 
thy 

196 
> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, []) 

197 
end; 

198 

199 
val typedef_proof = gen_typedef_proof read_term; 

200 
val typedef_proof_i = gen_typedef_proof cert_term; 

6357  201 

202 

6383  203 

204 
(** outer syntax **) 

205 

206 
local open OuterParse in 

207 

6357  208 
val typedeclP = 
6383  209 
OuterSyntax.command "typedecl" "HOL type declaration" 
210 
(type_args  name  opt_mixfix >> (fn ((vs, t), mx) => 

6357  211 
Toplevel.theory (add_typedecls [(t, vs, mx)]))); 
212 

6383  213 
val typedef_proof_decl = 
214 
Scan.option ($$$ "("  name  $$$ ")")  

215 
(type_args  name)  opt_infix  ($$$ "="  term); 

6357  216 

6383  217 
fun mk_typedef_proof (((opt_name, (vs, t)), mx), A) = 
218 
typedef_proof (if_none opt_name (Syntax.type_name t mx)) (t, vs, mx) A; 

6357  219 

220 
val typedefP = 

6383  221 
OuterSyntax.command "typedef" "HOL type definition (requires nonemptiness proof)" 
222 
(typedef_proof_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef_proof))); 

6357  223 

224 
val _ = OuterSyntax.add_parsers [typedeclP, typedefP]; 

225 

4866  226 
end; 
6383  227 

228 

229 
end; 