author  wenzelm 
Mon, 15 Feb 2010 17:17:51 +0100  
changeset 35129  ed24ba6f69aa 
parent 35021  c839a4c670c6 
child 35203  ef65a2218c31 
permissions  rwrr 
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

1 
(* Title: HOLCF/Tools/repdef.ML 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

2 
Author: Brian Huffman 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

3 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

4 
Defining representable domains using algebraic deflations. 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

5 
*) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

6 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

7 
signature REPDEF = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

8 
sig 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

9 
type rep_info = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

10 
{ emb_def: thm, prj_def: thm, approx_def: thm, REP: thm } 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

11 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

12 
val add_repdef: bool > binding option > binding * string list * mixfix > 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

13 
term > (binding * binding) option > theory > 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

14 
(Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

15 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

16 
val repdef_cmd: (bool * binding) * (binding * string list * mixfix) * string 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

17 
* (binding * binding) option > theory > theory 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

18 
end; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

19 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

20 
structure Repdef :> REPDEF = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

21 
struct 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

22 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

23 
(** type definitions **) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

24 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

25 
type rep_info = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

26 
{ emb_def: thm, prj_def: thm, approx_def: thm, REP: thm }; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

27 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

28 
(* building terms *) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

29 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

30 
fun adm_const T = Const (@{const_name adm}, (T > HOLogic.boolT) > HOLogic.boolT); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

31 
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

32 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

33 
fun below_const T = Const (@{const_name below}, T > T > HOLogic.boolT); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

34 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

35 
val natT = @{typ nat}; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

36 
val udomT = @{typ udom}; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

37 
fun alg_deflT T = Type (@{type_name alg_defl}, [T]); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

38 
fun cfunT (T, U) = Type (@{type_name ">"}, [T, U]); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

39 
fun emb_const T = Const (@{const_name emb}, cfunT (T, udomT)); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

40 
fun prj_const T = Const (@{const_name prj}, cfunT (udomT, T)); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

41 
fun approx_const T = Const (@{const_name approx}, natT > cfunT (T, T)); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

42 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

43 
fun LAM_const (T, U) = Const (@{const_name Abs_CFun}, (T > U) > cfunT (T, U)); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

44 
fun APP_const (T, U) = Const (@{const_name Rep_CFun}, cfunT (T, U) > (T > U)); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

45 
fun cast_const T = Const (@{const_name cast}, cfunT (alg_deflT T, cfunT (T, T))); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

46 
fun mk_cast (t, x) = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

47 
APP_const (udomT, udomT) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

48 
$ (APP_const (alg_deflT udomT, cfunT (udomT, udomT)) $ cast_const udomT $ t) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

49 
$ x; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

50 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

51 
(* manipulating theorems *) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

52 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

53 
(* proving class instances *) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

54 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

55 
fun declare_type_name a = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

56 
Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

57 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

58 
fun gen_add_repdef 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

59 
(prep_term: Proof.context > 'a > term) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

60 
(def: bool) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

61 
(name: binding) 
35129  62 
(typ as (tname, vs, mx) : binding * string list * mixfix) 
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

63 
(raw_defl: 'a) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

64 
(opt_morphs: (binding * binding) option) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

65 
(thy: theory) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

66 
: (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

67 
let 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

68 
val _ = Theory.requires thy "Representable" "repdefs"; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

69 
val ctxt = ProofContext.init thy; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

70 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

71 
(*rhs*) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

72 
val defl = prep_term (ctxt > fold declare_type_name vs) raw_defl; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

73 
val deflT = Term.fastype_of defl; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

74 
val _ = if deflT = @{typ "udom alg_defl"} then () 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

75 
else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ ctxt deflT)); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

76 
val rhs_tfrees = Term.add_tfrees defl []; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

77 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

78 
(*lhs*) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

79 
val defS = Sign.defaultS thy; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

80 
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

81 
val lhs_sorts = map snd lhs_tfrees; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

82 
val full_tname = Sign.full_name thy tname; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

83 
val newT = Type (full_tname, map TFree lhs_tfrees); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

84 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

85 
(*morphisms*) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

86 
val morphs = opt_morphs 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

87 
> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

88 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

89 
(*set*) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

90 
val in_defl = @{term "in_deflation :: udom => udom alg_defl => bool"}; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

91 
val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

92 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

93 
(*pcpodef*) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

94 
val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_deflation} 1; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

95 
val tac2 = rtac @{thm adm_mem_Collect_in_deflation} 1; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

96 
val ((info, cpo_info, pcpo_info), thy2) = thy 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

97 
> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

98 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

99 
(*definitions*) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

100 
val Rep_const = Const (#Rep_name info, newT > udomT); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

101 
val Abs_const = Const (#Abs_name info, udomT > newT); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

102 
val emb_eqn = Logic.mk_equals (emb_const newT, LAM_const (newT, udomT) $ Rep_const); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

103 
val prj_eqn = Logic.mk_equals (prj_const newT, LAM_const (udomT, newT) $ 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

104 
Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0))); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

105 
val repdef_approx_const = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

106 
Const (@{const_name repdef_approx}, (newT > udomT) > (udomT > newT) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

107 
> alg_deflT udomT > natT > cfunT (newT, newT)); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

108 
val approx_eqn = Logic.mk_equals (approx_const newT, 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

109 
repdef_approx_const $ Rep_const $ Abs_const $ defl); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

110 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

111 
(*instantiate class rep*) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

112 
val name_def = Binding.suffix_name "_def" name; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

113 
val ([emb_ldef, prj_ldef, approx_ldef], lthy3) = thy2 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

114 
> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep}) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

115 
> fold_map Specification.definition 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

116 
[ (NONE, ((Binding.prefix_name "emb_" name_def, []), emb_eqn)) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

117 
, (NONE, ((Binding.prefix_name "prj_" name_def, []), prj_eqn)) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

118 
, (NONE, ((Binding.prefix_name "approx_" name_def, []), approx_eqn)) ] 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

119 
>> map (snd o snd); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

120 
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy3); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

121 
val [emb_def, prj_def, approx_def] = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

122 
ProofContext.export lthy3 ctxt_thy [emb_ldef, prj_ldef, approx_ldef]; 
33826  123 
val type_definition_thm = 
124 
MetaSimplifier.rewrite_rule 

125 
(the_list (#set_def info)) 

126 
(#type_definition info); 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

127 
val typedef_thms = 
33826  128 
[type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def]; 
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

129 
val thy4 = lthy3 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

130 
> Class.prove_instantiation_instance 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

131 
(K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1)) 
33681  132 
> Local_Theory.exit_global; 
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

133 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

134 
(*other theorems*) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

135 
val typedef_thms' = map (Thm.transfer thy4) 
33826  136 
[type_definition_thm, #below_def cpo_info, emb_def, prj_def]; 
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

137 
val ([REP_thm], thy5) = thy4 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

138 
> Sign.add_path (Binding.name_of name) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

139 
> PureThy.add_thms 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

140 
[((Binding.prefix_name "REP_" name, 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33826
diff
changeset

141 
Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])] 
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

142 
> Sign.parent_path; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

143 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

144 
val rep_info = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

145 
{ emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm }; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

146 
in 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

147 
((info, cpo_info, pcpo_info, rep_info), thy5) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

148 
end 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

149 
handle ERROR msg => 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

150 
cat_error msg ("The error(s) above occurred in repdef " ^ quote (Binding.str_of name)); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

151 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

152 
fun add_repdef def opt_name typ defl opt_morphs thy = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

153 
let 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

154 
val name = the_default (#1 typ) opt_name; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

155 
in 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

156 
gen_add_repdef Syntax.check_term def name typ defl opt_morphs thy 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

157 
end; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

158 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

159 
fun repdef_cmd ((def, name), typ, A, morphs) = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

160 
snd o gen_add_repdef Syntax.read_term def name typ A morphs; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

161 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

162 
(** outer syntax **) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

163 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

164 
local structure P = OuterParse and K = OuterKeyword in 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

165 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

166 
val repdef_decl = 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

167 
Scan.optional (P.$$$ "("  
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

168 
((P.$$$ "open" >> K false)  Scan.option P.binding  P.binding >> (fn s => (true, SOME s))) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

169 
 P.$$$ ")") (true, NONE)  
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

170 
(P.type_args  P.binding)  P.opt_infix  (P.$$$ "="  P.term)  
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

171 
Scan.option (P.$$$ "morphisms"  P.!!! (P.binding  P.binding)); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

172 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

173 
fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = 
35129  174 
repdef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs); 
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

175 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

176 
val _ = 
33812  177 
OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl 
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

178 
(repdef_decl >> 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

179 
(Toplevel.print oo (Toplevel.theory o mk_repdef))); 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

180 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

181 
end; 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

182 

331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset

183 
end; 