author  kuncar 
Tue, 29 May 2012 19:13:02 +0200  
changeset 48024  7599b28b707f 
parent 47982  7aa35601ff65 
child 49625  06cf80661e7a 
permissions  rwrr 
47308  1 
(* Title: HOL/Tools/Lifting/lifting_def.ML 
2 
Author: Ondrej Kuncar 

3 

4 
Definitions for constants on quotient types. 

5 
*) 

6 

7 
signature LIFTING_DEF = 

8 
sig 

9 
val add_lift_def: 

10 
(binding * mixfix) > typ > term > thm > local_theory > local_theory 

11 

12 
val lift_def_cmd: 

13 
(binding * string option * mixfix) * string > local_theory > Proof.state 

14 

15 
val can_generate_code_cert: thm > bool 

16 
end; 

17 

18 
structure Lifting_Def: LIFTING_DEF = 

19 
struct 

20 

47698  21 
open Lifting_Util 
47308  22 

23 
infix 0 MRSL 

24 

47698  25 
(* Generation of the code certificate from the rsp theorem *) 
47308  26 

27 
fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V) 

28 
 get_body_types (U, V) = (U, V) 

29 

30 
fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W) 

31 
 get_binder_types _ = [] 

32 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

33 
fun get_binder_types_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

34 
(T, V) :: get_binder_types_by_rel S (U, W) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

35 
 get_binder_types_by_rel _ _ = [] 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

36 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

37 
fun get_body_type_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

38 
get_body_type_by_rel S (U, V) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

39 
 get_body_type_by_rel _ (U, V) = (U, V) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

40 

47308  41 
fun force_rty_type ctxt rty rhs = 
42 
let 

43 
val thy = Proof_Context.theory_of ctxt 

44 
val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs 

45 
val rty_schematic = fastype_of rhs_schematic 

46 
val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty 

47 
in 

48 
Envir.subst_term_types match rhs_schematic 

49 
end 

50 

51 
fun unabs_def ctxt def = 

52 
let 

53 
val (_, rhs) = Thm.dest_equals (cprop_of def) 

54 
fun dest_abs (Abs (var_name, T, _)) = (var_name, T) 

55 
 dest_abs tm = raise TERM("get_abs_var",[tm]) 

56 
val (var_name, T) = dest_abs (term_of rhs) 

57 
val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt 

58 
val thy = Proof_Context.theory_of ctxt' 

59 
val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T))) 

60 
in 

61 
Thm.combination def refl_thm > 

62 
singleton (Proof_Context.export ctxt' ctxt) 

63 
end 

64 

65 
fun unabs_all_def ctxt def = 

66 
let 

67 
val (_, rhs) = Thm.dest_equals (cprop_of def) 

68 
val xs = strip_abs_vars (term_of rhs) 

69 
in 

70 
fold (K (unabs_def ctxt)) xs def 

71 
end 

72 

73 
val map_fun_unfolded = 

74 
@{thm map_fun_def[abs_def]} > 

75 
unabs_def @{context} > 

76 
unabs_def @{context} > 

77 
Local_Defs.unfold @{context} [@{thm comp_def}] 

78 

79 
fun unfold_fun_maps ctm = 

80 
let 

81 
fun unfold_conv ctm = 

82 
case (Thm.term_of ctm) of 

83 
Const (@{const_name "map_fun"}, _) $ _ $ _ => 

84 
(Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm 

85 
 _ => Conv.all_conv ctm 

86 
in 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

87 
(Conv.fun_conv unfold_conv) ctm 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

88 
end 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

89 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

90 
fun unfold_fun_maps_beta ctm = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

91 
let val try_beta_conv = Conv.try_conv (Thm.beta_conversion false) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

92 
in 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

93 
(unfold_fun_maps then_conv try_beta_conv) ctm 
47308  94 
end 
95 

96 
fun prove_rel ctxt rsp_thm (rty, qty) = 

97 
let 

98 
val ty_args = get_binder_types (rty, qty) 

99 
fun disch_arg args_ty thm = 

100 
let 

47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

101 
val quot_thm = Lifting_Term.prove_quot_thm ctxt args_ty 
47308  102 
in 
103 
[quot_thm, thm] MRSL @{thm apply_rsp''} 

104 
end 

105 
in 

106 
fold disch_arg ty_args rsp_thm 

107 
end 

108 

109 
exception CODE_CERT_GEN of string 

110 

111 
fun simplify_code_eq ctxt def_thm = 

48024  112 
Local_Defs.unfold ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm 
47308  113 

47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

114 
(* 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

115 
quot_thm  quotient theorem (Quotient R Abs Rep T). 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

116 
returns: whether the Lifting package is capable to generate code for the abstract type 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

117 
represented by quot_thm 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

118 
*) 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

119 

47308  120 
fun can_generate_code_cert quot_thm = 
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47937
diff
changeset

121 
case quot_thm_rel quot_thm of 
47308  122 
Const (@{const_name HOL.eq}, _) => true 
123 
 Const (@{const_name invariant}, _) $ _ => true 

124 
 _ => false 

125 

126 
fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) = 

127 
let 

128 
val thy = Proof_Context.theory_of ctxt 

47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

129 
val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty)) 
47308  130 
val fun_rel = prove_rel ctxt rsp_thm (rty, qty) 
131 
val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs} 

132 
val abs_rep_eq = 

133 
case (HOLogic.dest_Trueprop o prop_of) fun_rel of 

134 
Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm 

135 
 Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq} 

136 
 _ => raise CODE_CERT_GEN "relation is neither equality nor invariant" 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

137 
val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm 
47308  138 
val unabs_def = unabs_all_def ctxt unfolded_def 
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47937
diff
changeset

139 
val rep = (cterm_of thy o quot_thm_rep) quot_thm 
47308  140 
val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq} 
141 
val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong} 

142 
val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans} 

143 
in 

144 
simplify_code_eq ctxt code_cert 

145 
end 

146 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

147 
fun generate_trivial_rep_eq ctxt def_thm = 
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset

148 
let 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

149 
val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

150 
val code_eq = unabs_all_def ctxt unfolded_def 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

151 
val simp_code_eq = simplify_code_eq ctxt code_eq 
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset

152 
in 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

153 
simp_code_eq 
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset

154 
end 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

155 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

156 
fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

157 
if body_type rty = body_type qty then 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

158 
SOME (generate_trivial_rep_eq ctxt def_thm) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

159 
else 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

160 
let 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

161 
val (rty_body, qty_body) = get_body_types (rty, qty) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

162 
val quot_thm = Lifting_Term.prove_quot_thm ctxt (rty_body, qty_body) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

163 
in 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

164 
if can_generate_code_cert quot_thm then 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

165 
SOME (generate_code_cert ctxt def_thm rsp_thm (rty, qty)) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

166 
else 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

167 
NONE 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

168 
end 
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset

169 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

170 
fun generate_abs_eq ctxt def_thm rsp_thm quot_thm = 
47308  171 
let 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

172 
fun refl_tac ctxt = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

173 
let 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

174 
fun intro_reflp_tac (t, i) = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

175 
let 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

176 
val concl_pat = Drule.strip_imp_concl (cprop_of @{thm reflpD}) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

177 
val insts = Thm.first_order_match (concl_pat, t) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

178 
in 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

179 
rtac (Drule.instantiate_normalize insts @{thm reflpD}) i 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

180 
end 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

181 
handle Pattern.MATCH => no_tac 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

182 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

183 
val fun_rel_meta_eq = mk_meta_eq @{thm fun_rel_eq} 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

184 
val conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv fun_rel_meta_eq))) ctxt 
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47951
diff
changeset

185 
val rules = Lifting_Info.get_reflexivity_rules ctxt 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

186 
in 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

187 
EVERY' [CSUBGOAL intro_reflp_tac, 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

188 
CONVERSION conv, 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

189 
REPEAT_ALL_NEW (resolve_tac rules)] 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

190 
end 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

191 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

192 
fun try_prove_prem ctxt prop = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

193 
SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1)) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

194 
handle ERROR _ => NONE 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

195 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

196 
val abs_eq_with_assms = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

197 
let 
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47937
diff
changeset

198 
val (rty, qty) = quot_thm_rty_qty quot_thm 
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47937
diff
changeset

199 
val rel = quot_thm_rel quot_thm 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

200 
val ty_args = get_binder_types_by_rel rel (rty, qty) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

201 
val body_type = get_body_type_by_rel rel (rty, qty) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

202 
val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

203 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

204 
val rep_abs_folded_unmapped_thm = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

205 
let 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

206 
val rep_id = [quot_thm, def_thm] MRSL @{thm Quotient_Rep_eq} 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

207 
val ctm = Thm.dest_equals_lhs (cprop_of rep_id) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

208 
val unfolded_maps_eq = unfold_fun_maps ctm 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

209 
val t1 = [quot_thm, def_thm, rsp_thm] MRSL @{thm Quotient_rep_abs_fold_unmap} 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

210 
val prems_pat = (hd o Drule.cprems_of) t1 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

211 
val insts = Thm.first_order_match (prems_pat, cprop_of unfolded_maps_eq) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

212 
in 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

213 
unfolded_maps_eq RS (Drule.instantiate_normalize insts t1) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

214 
end 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

215 
in 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

216 
rep_abs_folded_unmapped_thm 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

217 
> fold (fn _ => fn thm => thm RS @{thm fun_relD2}) ty_args 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

218 
> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm])) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

219 
end 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

220 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

221 
val prems = prems_of abs_eq_with_assms 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

222 
val indexed_prems = map_index (apfst (fn x => x + 1)) prems 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

223 
val indexed_assms = map (apsnd (try_prove_prem ctxt)) indexed_prems 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

224 
val proved_assms = map (apsnd the) (filter (is_some o snd) indexed_assms) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

225 
val abs_eq = fold_rev (fn (i, assms) => fn thm => assms RSN (i, thm)) proved_assms abs_eq_with_assms 
47308  226 
in 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

227 
simplify_code_eq ctxt abs_eq 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

228 
end 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

229 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

230 
fun define_code_using_abs_eq abs_eq_thm lthy = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

231 
if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

232 
(snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

233 
else 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

234 
lthy 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

235 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

236 
fun define_code_using_rep_eq maybe_rep_eq_thm lthy = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

237 
case maybe_rep_eq_thm of 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

238 
SOME rep_eq_thm => 
47308  239 
let 
240 
val add_abs_eqn_attribute = 

241 
Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I) 

242 
val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute); 

243 
in 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

244 
(snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [rep_eq_thm]) lthy 
47308  245 
end 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

246 
 NONE => lthy 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

247 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

248 
fun has_constr ctxt quot_thm = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

249 
let 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

250 
val thy = Proof_Context.theory_of ctxt 
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47937
diff
changeset

251 
val abs_fun = quot_thm_abs quot_thm 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

252 
in 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

253 
if is_Const abs_fun then 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

254 
Code.is_constr thy ((fst o dest_Const) abs_fun) 
47308  255 
else 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

256 
false 
47308  257 
end 
258 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

259 
fun has_abstr ctxt quot_thm = 
47308  260 
let 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

261 
val thy = Proof_Context.theory_of ctxt 
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47937
diff
changeset

262 
val abs_fun = quot_thm_abs quot_thm 
47308  263 
in 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

264 
if is_Const abs_fun then 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

265 
Code.is_abstr thy ((fst o dest_Const) abs_fun) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

266 
else 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

267 
false 
47308  268 
end 
269 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

270 
fun define_code abs_eq_thm maybe_rep_eq_thm (rty, qty) lthy = 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

271 
let 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

272 
val (rty_body, qty_body) = get_body_types (rty, qty) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

273 
in 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

274 
if rty_body = qty_body then 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

275 
if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

276 
(snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

277 
else 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

278 
(snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the maybe_rep_eq_thm]) lthy 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

279 
else 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

280 
let 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

281 
val body_quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

282 
in 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

283 
if has_constr lthy body_quot_thm then 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

284 
define_code_using_abs_eq abs_eq_thm lthy 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

285 
else if has_abstr lthy body_quot_thm then 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

286 
define_code_using_rep_eq maybe_rep_eq_thm lthy 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

287 
else 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

288 
lthy 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

289 
end 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

290 
end 
47308  291 

47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

292 
(* 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

293 
Defines an operation on an abstract type in terms of a corresponding operation 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

294 
on a representation type. 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

295 

0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

296 
var  a binding and a mixfix of the new constant being defined 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

297 
qty  an abstract type of the new constant 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

298 
rhs  a term representing the new constant on the raw level 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

299 
rsp_thm  a respectfulness theorem in the internal tagged form (like '(R ===> R ===> R) f f'), 
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

300 
i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs" 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

301 
*) 
47308  302 

303 
fun add_lift_def var qty rhs rsp_thm lthy = 

304 
let 

305 
val rty = fastype_of rhs 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

306 
val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty) 
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47937
diff
changeset

307 
val absrep_trm = quot_thm_abs quot_thm 
47308  308 
val rty_forced = (domain_type o fastype_of) absrep_trm 
309 
val forced_rhs = force_rty_type lthy rty_forced rhs 

310 
val lhs = Free (Binding.print (#1 var), qty) 

311 
val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs) 

312 
val (_, prop') = Local_Defs.cert_def lthy prop 

313 
val (_, newrhs) = Local_Defs.abs_def prop' 

314 

315 
val ((_, (_ , def_thm)), lthy') = 

316 
Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy 

317 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

318 
val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}) 
47503  319 
> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy') 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

320 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

321 
val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

322 
val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty) 
47351  323 

47545  324 
fun qualify defname suffix = Binding.qualified true suffix defname 
47308  325 

47545  326 
val lhs_name = (#1 var) 
47308  327 
val rsp_thm_name = qualify lhs_name "rsp" 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

328 
val abs_eq_thm_name = qualify lhs_name "abs_eq" 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

329 
val rep_eq_thm_name = qualify lhs_name "rep_eq" 
47351  330 
val transfer_thm_name = qualify lhs_name "transfer" 
47373  331 
val transfer_attr = Attrib.internal (K Transfer.transfer_add) 
47308  332 
in 
333 
lthy' 

334 
> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm]) 

47373  335 
> (snd oo Local_Theory.note) ((transfer_thm_name, [transfer_attr]), [transfer_thm]) 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

336 
> (snd oo Local_Theory.note) ((abs_eq_thm_name, []), [abs_eq_thm]) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

337 
> (case maybe_rep_eq_thm of 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

338 
SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm]) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

339 
 NONE => I) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

340 
> define_code abs_eq_thm maybe_rep_eq_thm (rty_forced, qty) 
47308  341 
end 
342 

343 
fun mk_readable_rsp_thm_eq tm lthy = 

344 
let 

345 
val ctm = cterm_of (Proof_Context.theory_of lthy) tm 

346 

347 
fun norm_fun_eq ctm = 

348 
let 

349 
fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy 

350 
fun erase_quants ctm' = 

351 
case (Thm.term_of ctm') of 

352 
Const ("HOL.eq", _) $ _ $ _ => Conv.all_conv ctm' 

353 
 _ => (Conv.binder_conv (K erase_quants) lthy then_conv 

354 
Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm' 

355 
in 

356 
(abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm 

357 
end 

358 

359 
fun simp_arrows_conv ctm = 

360 
let 

361 
val unfold_conv = Conv.rewrs_conv 

362 
[@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]}, 

363 
@{thm fun_rel_def[THEN eq_reflection]}] 

364 
val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq 

365 
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 

47634
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47607
diff
changeset

366 
val invariant_commute_conv = Conv.bottom_conv 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47607
diff
changeset

367 
(K (Conv.try_conv (Conv.rewrs_conv (Lifting_Info.get_invariant_commute_rules lthy)))) lthy 
47308  368 
in 
369 
case (Thm.term_of ctm) of 

370 
Const (@{const_name "fun_rel"}, _) $ _ $ _ => 

371 
(binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm 

47634
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47607
diff
changeset

372 
 _ => invariant_commute_conv ctm 
47308  373 
end 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47852
diff
changeset

374 

47308  375 
val unfold_ret_val_invs = Conv.bottom_conv 
376 
(K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy 

47699  377 
val simp_conv = Trueprop_conv (Conv.fun2_conv simp_arrows_conv) 
47308  378 
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} 
379 
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy 

380 
val beta_conv = Thm.beta_conversion true 

381 
val eq_thm = 

382 
(simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm 

383 
in 

384 
Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2) 

385 
end 

386 

47607  387 
fun rename_to_tnames ctxt term = 
388 
let 

389 
fun all_typs (Const ("all", _) $ Abs (_, T, t)) = T :: all_typs t 

390 
 all_typs _ = [] 

47308  391 

47607  392 
fun rename (Const ("all", T1) $ Abs (_, T2, t)) (new_name :: names) = 
393 
(Const ("all", T1) $ Abs (new_name, T2, rename t names)) 

394 
 rename t _ = t 

395 

396 
val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt 

397 
val new_names = Datatype_Prop.make_tnames (all_typs fixed_def_t) 

398 
in 

399 
rename term new_names 

400 
end 

47308  401 

47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

402 
(* 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

403 

0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

404 
lifting_definition command. It opens a proof of a corresponding respectfulness 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

405 
theorem in a userfriendly, readable form. Then add_lift_def is called internally. 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

406 

0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

407 
*) 
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47699
diff
changeset

408 

47308  409 
fun lift_def_cmd (raw_var, rhs_raw) lthy = 
410 
let 

47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

411 
val ((binding, SOME qty, mx), lthy') = yield_singleton Proof_Context.read_vars raw_var lthy 
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

412 
val rhs = (Syntax.check_term lthy' o Syntax.parse_term lthy') rhs_raw 
47308  413 

414 
fun try_to_prove_refl thm = 

415 
let 

416 
val lhs_eq = 

417 
thm 

418 
> prop_of 

419 
> Logic.dest_implies 

420 
> fst 

421 
> strip_all_body 

422 
> try HOLogic.dest_Trueprop 

423 
in 

424 
case lhs_eq of 

425 
SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm) 

426 
 _ => NONE 

427 
end 

428 

47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

429 
val rsp_rel = Lifting_Term.equiv_relation lthy' (fastype_of rhs, qty) 
47308  430 
val rty_forced = (domain_type o fastype_of) rsp_rel; 
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

431 
val forced_rhs = force_rty_type lthy' rty_forced rhs; 
47308  432 
val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs) 
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

433 
val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy' 
47308  434 
val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq 
435 
val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq) 

47607  436 
val readable_rsp_tm_tnames = rename_to_tnames lthy' readable_rsp_tm 
437 

47308  438 
fun after_qed thm_list lthy = 
439 
let 

440 
val internal_rsp_thm = 

441 
case thm_list of 

442 
[] => the maybe_proven_rsp_thm 

47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

443 
 [[thm]] => Goal.prove lthy [] [] internal_rsp_tm 
47308  444 
(fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1) 
445 
in 

446 
add_lift_def (binding, mx) qty rhs internal_rsp_thm lthy 

447 
end 

448 

449 
in 

450 
case maybe_proven_rsp_thm of 

47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

451 
SOME _ => Proof.theorem NONE after_qed [] lthy' 
47607  452 
 NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm_tnames,[])]] lthy' 
47308  453 
end 
454 

47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

455 
fun quot_thm_err ctxt (rty, qty) pretty_msg = 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

456 
let 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

457 
val error_msg = cat_lines 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

458 
["Lifting failed for the following types:", 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

459 
Pretty.string_of (Pretty.block 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

460 
[Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]), 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

461 
Pretty.string_of (Pretty.block 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

462 
[Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]), 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

463 
"", 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

464 
(Pretty.string_of (Pretty.block 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

465 
[Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))] 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

466 
in 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

467 
error error_msg 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

468 
end 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

469 

47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

470 
fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) = 
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

471 
let 
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

472 
val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt 
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

473 
val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw 
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

474 
val error_msg = cat_lines 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

475 
["Lifting failed for the following term:", 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

476 
Pretty.string_of (Pretty.block 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

477 
[Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]), 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

478 
Pretty.string_of (Pretty.block 
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

479 
[Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty_schematic]), 
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

480 
"", 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

481 
(Pretty.string_of (Pretty.block 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

482 
[Pretty.str "Reason:", 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

483 
Pretty.brk 2, 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

484 
Pretty.str "The type of the term cannot be instancied to", 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

485 
Pretty.brk 1, 
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

486 
Pretty.quote (Syntax.pretty_typ ctxt rty_forced), 
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

487 
Pretty.str "."]))] 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

488 
in 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

489 
error error_msg 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

490 
end 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

491 

075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

492 
fun lift_def_cmd_with_err_handling (raw_var, rhs_raw) lthy = 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

493 
(lift_def_cmd (raw_var, rhs_raw) lthy 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

494 
handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg) 
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

495 
handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) => 
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

496 
check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw) 
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

497 

47308  498 
(* parser and command *) 
499 
val liftdef_parser = 

500 
((Parse.binding  (@{keyword "::"}  (Parse.typ >> SOME)  Parse.opt_mixfix')) >> Parse.triple2) 

501 
 @{keyword "is"}  Parse.term 

502 

503 
val _ = 

504 
Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"} 

505 
"definition for constants over the quotient type" 

47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

506 
(liftdef_parser >> lift_def_cmd_with_err_handling) 
47308  507 

508 

509 
end; (* structure *) 