author  wenzelm 
Mon, 24 May 1999 21:57:13 +0200  
changeset 6723  f342449d73ca 
parent 6690  acbcf8085166 
child 6729  b6e167580a32 
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 
6690  18 
val typedef_proof: string > bstring * string list * mixfix > string 
19 
> bool > theory > ProofHistory.T 

20 
val typedef_proof_i: string > bstring * string list * mixfix > term 

21 
> bool > theory > ProofHistory.T 

4866  22 
end; 
23 

24 
structure TypedefPackage: TYPEDEF_PACKAGE = 

25 
struct 

26 

27 

5104  28 
(** type declarations **) 
29 

30 
fun add_typedecls decls thy = 

31 
let 

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

33 

34 
fun arity_of (raw_name, args, mx) = 

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

36 
in 

37 
thy 

38 
> PureThy.add_typedecls decls 

39 
> Theory.add_arities_i (map arity_of decls) 

40 
end; 

41 

42 

43 

44 
(** type definitions **) 

45 

5697  46 
(* messages *) 
47 

48 
val quiet_mode = ref false; 

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

50 

51 

6383  52 
(* nonemptiness of set *) (*exception ERROR*) 
4866  53 

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

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

59 
in 

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

61 
None => raise ERROR 

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

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

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

65 

66 
fun goal_nonempty cset = 

67 
let 

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

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

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

73 
let 

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

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

4866  76 
val tac = 
77 
TRY (rewrite_goals_tac (filter is_def thms)) THEN 

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

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

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

4866  84 

85 

6383  86 
(* prepare_typedef *) 
87 

88 
fun read_term sg used s = 

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

4866  90 

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

93 
fun err_in_typedef name = 

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

95 

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

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

102 
(*rhs*) 

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

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

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

108 

109 
(*lhs*) 

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

113 

114 
val Rep_name = "Rep_" ^ name; 

115 
val Abs_name = "Abs_" ^ name; 

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

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

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

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

120 
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

121 
val set' = if no_def then set else setC; 
4866  122 

123 
(*axioms*) 

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

124 
val rep_type = HOLogic.mk_Trueprop (HOLogic.mk_mem (RepC $ x_new, set')); 
4866  125 
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

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

6383  129 
(*theory extender*) 
130 
fun do_typedef theory = 

131 
theory 

132 
> Theory.assert_super thy 

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

134 
> Theory.add_consts_i 

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

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

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

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

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

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

141 
[(Rep_name, rep_type), 

142 
(Rep_name ^ "_inverse", rep_type_inv), 

143 
(Abs_name ^ "_inverse", abs_type_inv)] 

144 
handle ERROR => err_in_typedef name; 

145 

4866  146 

147 
(* errors *) 

148 

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

150 

151 
val illegal_vars = 

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

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

154 

155 
val dup_lhs_tfrees = 

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

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

158 

159 
val extra_rhs_tfrees = 

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

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

162 

163 
val illegal_frees = 

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

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

166 

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

168 
in 

6383  169 
if null errs then () else error (cat_lines errs); 
170 
(cset, do_typedef) 

171 
end handle ERROR => err_in_typedef name; 

4866  172 

173 

6383  174 
(* add_typedef interfaces *) 
4866  175 

6383  176 
fun gen_add_typedef prep_term no_def name typ set names thms tac thy = 
177 
let 

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

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

180 
in check_nonempty cset result; thy > do_typedef end; 

4866  181 

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

182 
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

183 
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

184 
val add_typedef_i_no_def = gen_add_typedef cert_term true; 
4866  185 

186 

6383  187 
(* typedef_proof interface *) 
188 

189 
fun typedef_attribute cset do_typedef (thy, thm) = 

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

6357  191 

6690  192 
fun gen_typedef_proof prep_term name typ set int thy = 
6383  193 
let 
194 
val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy; 

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

196 
in 

197 
thy 

6690  198 
> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, []) int 
6383  199 
end; 
200 

201 
val typedef_proof = gen_typedef_proof read_term; 

202 
val typedef_proof_i = gen_typedef_proof cert_term; 

6357  203 

204 

6383  205 

206 
(** outer syntax **) 

207 

6723  208 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6383  209 

6357  210 
val typedeclP = 
6723  211 
OuterSyntax.command "typedecl" "HOL type declaration" K.thy_decl 
212 
(P.type_args  P.name  P.opt_mixfix >> (fn ((vs, t), mx) => 

6357  213 
Toplevel.theory (add_typedecls [(t, vs, mx)]))); 
214 

6723  215 

6383  216 
val typedef_proof_decl = 
6723  217 
Scan.option (P.$$$ "("  P.name  P.$$$ ")")  
218 
(P.type_args  P.name)  P.opt_infix  (P.$$$ "="  P.term); 

6357  219 

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

6357  222 

223 
val typedefP = 

6723  224 
OuterSyntax.command "typedef" "HOL type definition (requires nonemptiness proof)" K.thy_goal 
6383  225 
(typedef_proof_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef_proof))); 
6357  226 

6723  227 

6357  228 
val _ = OuterSyntax.add_parsers [typedeclP, typedefP]; 
229 

4866  230 
end; 
6383  231 

232 

233 
end; 