author  wenzelm 
Mon, 26 Aug 2013 16:13:20 +0200  
changeset 53207  9745b7d4cc79 
parent 53205  8d41170242cb 
child 53651  ee90c67502c9 
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 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

9 
val generate_parametric_transfer_rule: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

10 
Proof.context > thm > thm > thm 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

11 

47308  12 
val add_lift_def: 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

13 
(binding * mixfix) > typ > term > thm > thm option > local_theory > local_theory 
47308  14 

15 
val lift_def_cmd: 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

16 
(binding * string option * mixfix) * string * (Facts.ref * Args.src list) option > local_theory > Proof.state 
47308  17 

18 
val can_generate_code_cert: thm > bool 

19 
end; 

20 

21 
structure Lifting_Def: LIFTING_DEF = 

22 
struct 

23 

47698  24 
open Lifting_Util 
47308  25 

26 
infix 0 MRSL 

27 

51994  28 
(* Reflexivity prover *) 
29 

30 
fun refl_tac ctxt = 

31 
let 

32 
fun intro_reflp_tac (ct, i) = 

33 
let 

34 
val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm reflpD} 

35 
val concl_pat = Drule.strip_imp_concl (cprop_of rule) 

36 
val insts = Thm.first_order_match (concl_pat, ct) 

37 
in 

38 
rtac (Drule.instantiate_normalize insts rule) i 

39 
end 

40 
handle Pattern.MATCH => no_tac 

41 

42 
val rules = @{thm is_equality_eq} :: 

43 
((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt)) 

44 
in 

45 
EVERY' [CSUBGOAL intro_reflp_tac, 

46 
REPEAT_ALL_NEW (resolve_tac rules)] 

47 
end 

48 

49 
fun try_prove_reflexivity ctxt prop = 

50 
SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1)) 

51 
handle ERROR _ => NONE 

52 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

53 
(* Generation of a transfer rule *) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

54 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

55 
fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule = 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

56 
let 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

57 
fun preprocess ctxt thm = 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

58 
let 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

59 
val tm = (strip_args 2 o HOLogic.dest_Trueprop o concl_of) thm; 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

60 
val param_rel = (snd o dest_comb o fst o dest_comb) tm; 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

61 
val thy = Proof_Context.theory_of ctxt; 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

62 
val free_vars = Term.add_vars param_rel []; 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

63 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

64 
fun make_subst (var as (_, typ)) subst = 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

65 
let 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

66 
val [rty, rty'] = binder_types typ 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

67 
in 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

68 
if (Term.is_TVar rty andalso is_Type rty') then 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

69 
(Var var, HOLogic.eq_const rty')::subst 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

70 
else 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

71 
subst 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

72 
end; 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

73 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

74 
val subst = fold make_subst free_vars []; 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

75 
val csubst = map (pairself (cterm_of thy)) subst; 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

76 
val inst_thm = Drule.cterm_instantiate csubst thm; 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

77 
in 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

78 
Conv.fconv_rule 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

79 
((Conv.concl_conv (nprems_of inst_thm) o HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

80 
(Raw_Simplifier.rewrite false (Transfer.get_sym_relator_eq ctxt))) inst_thm 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

81 
end 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

82 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

83 
fun inst_relcomppI thy ant1 ant2 = 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

84 
let 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

85 
val t1 = (HOLogic.dest_Trueprop o concl_of) ant1 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

86 
val t2 = (HOLogic.dest_Trueprop o prop_of) ant2 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

87 
val fun1 = cterm_of thy (strip_args 2 t1) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

88 
val args1 = map (cterm_of thy) (get_args 2 t1) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

89 
val fun2 = cterm_of thy (strip_args 2 t2) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

90 
val args2 = map (cterm_of thy) (get_args 1 t2) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

91 
val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI} 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

92 
val vars = (rev (Term.add_vars (prop_of relcomppI) [])) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

93 
val subst = map (apfst ((cterm_of thy) o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2)) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

94 
in 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

95 
Drule.cterm_instantiate subst relcomppI 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

96 
end 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

97 

51994  98 
fun zip_transfer_rules ctxt thm = let 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

99 
val thy = Proof_Context.theory_of ctxt 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

100 
fun mk_POS ty = Const (@{const_name POS}, ty > ty > HOLogic.boolT) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

101 
val rel = (Thm.dest_fun2 o Thm.dest_arg o cprop_of) thm 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

102 
val typ = (typ_of o ctyp_of_term) rel 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

103 
val POS_const = cterm_of thy (mk_POS typ) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

104 
val var = cterm_of thy (Var (("X", #maxidx (rep_cterm (rel)) + 1), typ)) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

105 
val goal = Thm.apply (cterm_of thy HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

106 
in 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

107 
[Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply} 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

108 
end 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

109 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

110 
val thm = (inst_relcomppI (Proof_Context.theory_of ctxt) parametric_transfer_rule transfer_rule) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

111 
OF [parametric_transfer_rule, transfer_rule] 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

112 
val preprocessed_thm = preprocess ctxt thm 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

113 
val orig_ctxt = ctxt 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

114 
val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

115 
val assms = cprems_of fixed_thm 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

116 
val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

117 
val ctxt = Context.proof_map(fold (add_transfer_rule o Thm.assume) assms) ctxt 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

118 
val zipped_thm = 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

119 
fixed_thm 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

120 
> undisch_all 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

121 
> zip_transfer_rules ctxt 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

122 
> implies_intr_list assms 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

123 
> singleton (Variable.export ctxt orig_ctxt) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

124 
in 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

125 
zipped_thm 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

126 
end 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

127 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

128 
fun print_generate_transfer_info msg = 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

129 
let 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

130 
val error_msg = cat_lines 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

131 
["Generation of a parametric transfer rule failed.", 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

132 
(Pretty.string_of (Pretty.block 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

133 
[Pretty.str "Reason:", Pretty.brk 2, msg]))] 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

134 
in 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

135 
error error_msg 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

136 
end 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

137 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

138 
fun generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm = 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

139 
let 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

140 
val transfer_rule = 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

141 
([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

142 
> Lifting_Term.parametrize_transfer_rule lthy 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

143 
in 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

144 
(option_fold transfer_rule (generate_parametric_transfer_rule lthy transfer_rule) opt_par_thm 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

145 
handle Lifting_Term.MERGE_TRANSFER_REL msg => (print_generate_transfer_info msg; transfer_rule)) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

146 
end 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

147 

47698  148 
(* Generation of the code certificate from the rsp theorem *) 
47308  149 

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

151 
 get_body_types (U, V) = (U, V) 

152 

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

154 
 get_binder_types _ = [] 

155 

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

156 
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

157 
(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

158 
 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

159 

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 
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

161 
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

162 
 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

163 

47308  164 
fun force_rty_type ctxt rty rhs = 
165 
let 

166 
val thy = Proof_Context.theory_of ctxt 

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

168 
val rty_schematic = fastype_of rhs_schematic 

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

170 
in 

171 
Envir.subst_term_types match rhs_schematic 

172 
end 

173 

174 
fun unabs_def ctxt def = 

175 
let 

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

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

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

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

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

181 
val thy = Proof_Context.theory_of ctxt' 

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

183 
in 

184 
Thm.combination def refl_thm > 

185 
singleton (Proof_Context.export ctxt' ctxt) 

186 
end 

187 

188 
fun unabs_all_def ctxt def = 

189 
let 

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

191 
val xs = strip_abs_vars (term_of rhs) 

192 
in 

193 
fold (K (unabs_def ctxt)) xs def 

194 
end 

195 

196 
val map_fun_unfolded = 

197 
@{thm map_fun_def[abs_def]} > 

198 
unabs_def @{context} > 

199 
unabs_def @{context} > 

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

201 

202 
fun unfold_fun_maps ctm = 

203 
let 

204 
fun unfold_conv ctm = 

205 
case (Thm.term_of ctm) of 

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

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

208 
 _ => Conv.all_conv ctm 

209 
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

210 
(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

211 
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

212 

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 
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

214 
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

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 
(unfold_fun_maps then_conv try_beta_conv) ctm 
47308  217 
end 
218 

219 
fun prove_rel ctxt rsp_thm (rty, qty) = 

220 
let 

221 
val ty_args = get_binder_types (rty, qty) 

222 
fun disch_arg args_ty thm = 

223 
let 

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

224 
val quot_thm = Lifting_Term.prove_quot_thm ctxt args_ty 
47308  225 
in 
226 
[quot_thm, thm] MRSL @{thm apply_rsp''} 

227 
end 

228 
in 

229 
fold disch_arg ty_args rsp_thm 

230 
end 

231 

232 
exception CODE_CERT_GEN of string 

233 

234 
fun simplify_code_eq ctxt def_thm = 

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

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

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

238 
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

239 
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

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

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

242 

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

244 
case quot_thm_rel quot_thm of 
47308  245 
Const (@{const_name HOL.eq}, _) => true 
246 
 Const (@{const_name invariant}, _) $ _ => true 

247 
 _ => false 

248 

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

250 
let 

251 
val thy = Proof_Context.theory_of ctxt 

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

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

255 
val abs_rep_eq = 

256 
case (HOLogic.dest_Trueprop o prop_of) fun_rel of 

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

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

259 
 _ => 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

260 
val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm 
47308  261 
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

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

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

266 
in 

267 
simplify_code_eq ctxt code_cert 

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 generate_trivial_rep_eq ctxt def_thm = 
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset

271 
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

272 
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

273 
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

274 
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

275 
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

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

277 
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

278 

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 
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

280 
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

281 
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

282 
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

283 
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

284 
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

285 
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

286 
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

287 
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

288 
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

289 
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

290 
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

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

292 

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

293 
fun generate_abs_eq ctxt def_thm rsp_thm quot_thm = 
47308  294 
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

295 
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

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

297 
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

298 
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

299 
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

300 
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

301 
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

302 

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

303 
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

304 
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

305 
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

306 
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

307 
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

308 
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

309 
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

310 
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

311 
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

312 
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

313 
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

314 
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

315 
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

316 
> 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

317 
> (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

318 
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

319 

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 
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

321 
val indexed_prems = map_index (apfst (fn x => x + 1)) prems 
51994  322 
val indexed_assms = map (apsnd (try_prove_reflexivity ctxt)) indexed_prems 
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

323 
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

324 
val abs_eq = fold_rev (fn (i, assms) => fn thm => assms RSN (i, thm)) proved_assms abs_eq_with_assms 
47308  325 
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

326 
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

327 
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

328 

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 
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

330 
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

331 
(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

332 
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

333 
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

334 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

335 
fun define_code_using_rep_eq opt_rep_eq_thm lthy = 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

336 
case opt_rep_eq_thm of 
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

337 
SOME rep_eq_thm => 
47308  338 
let 
339 
val add_abs_eqn_attribute = 

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

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

342 
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

343 
(snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [rep_eq_thm]) lthy 
47308  344 
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

345 
 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

346 

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

347 
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

348 
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

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

350 
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

351 
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

352 
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

353 
Code.is_constr thy ((fst o dest_Const) abs_fun) 
47308  354 
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

355 
false 
47308  356 
end 
357 

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

358 
fun has_abstr ctxt quot_thm = 
47308  359 
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

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

361 
val abs_fun = quot_thm_abs quot_thm 
47308  362 
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

363 
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

364 
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

365 
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

366 
false 
47308  367 
end 
368 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

369 
fun define_code abs_eq_thm opt_rep_eq_thm (rty, qty) 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

370 
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

371 
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

372 
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

373 
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

374 
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

375 
(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

376 
else 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

377 
(snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the opt_rep_eq_thm]) 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

378 
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

379 
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

380 
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

381 
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

382 
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

383 
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

384 
else if has_abstr lthy body_quot_thm then 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

385 
define_code_using_rep_eq opt_rep_eq_thm 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

386 
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

387 
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

388 
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

389 
end 
47308  390 

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

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

392 
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

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

394 

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

395 
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

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

397 
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

398 
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

399 
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

400 
*) 
47308  401 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

402 
fun add_lift_def var qty rhs rsp_thm opt_par_thm lthy = 
47308  403 
let 
404 
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

405 
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

406 
val absrep_trm = quot_thm_abs quot_thm 
47308  407 
val rty_forced = (domain_type o fastype_of) absrep_trm 
408 
val forced_rhs = force_rty_type lthy rty_forced rhs 

53207
9745b7d4cc79
prefer Binding.name_of over Binding.print  the latter leads to funny quotes and markup within the constructed term;
wenzelm
parents:
53205
diff
changeset

409 
val lhs = Free (Binding.name_of (#1 var), qty) 
47308  410 
val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs) 
411 
val (_, prop') = Local_Defs.cert_def lthy prop 

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

413 

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

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

416 

53205  417 
val transfer_rule = generate_transfer_rule lthy' quot_thm rsp_thm def_thm opt_par_thm 
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
49885
diff
changeset

418 

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

419 
val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

420 
val opt_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty) 
47351  421 

47545  422 
fun qualify defname suffix = Binding.qualified true suffix defname 
47308  423 

47545  424 
val lhs_name = (#1 var) 
47308  425 
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

426 
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

427 
val rep_eq_thm_name = qualify lhs_name "rep_eq" 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

428 
val transfer_rule_name = qualify lhs_name "transfer" 
47373  429 
val transfer_attr = Attrib.internal (K Transfer.transfer_add) 
47308  430 
in 
431 
lthy' 

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

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

433 
> (snd oo Local_Theory.note) ((transfer_rule_name, [transfer_attr]), [transfer_rule]) 
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

434 
> (snd oo Local_Theory.note) ((abs_eq_thm_name, []), [abs_eq_thm]) 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

435 
> (case opt_rep_eq_thm of 
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

436 
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

437 
 NONE => I) 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

438 
> define_code abs_eq_thm opt_rep_eq_thm (rty_forced, qty) 
47308  439 
end 
440 

441 
fun mk_readable_rsp_thm_eq tm lthy = 

442 
let 

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

444 

445 
fun simp_arrows_conv ctm = 

446 
let 

447 
val unfold_conv = Conv.rewrs_conv 

49626  448 
[@{thm fun_rel_eq_invariant[THEN eq_reflection]}, 
449 
@{thm fun_rel_eq[THEN eq_reflection]}, 

450 
@{thm fun_rel_eq_rel[THEN eq_reflection]}, 

47308  451 
@{thm fun_rel_def[THEN eq_reflection]}] 
452 
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

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

454 
(K (Conv.try_conv (Conv.rewrs_conv (Lifting_Info.get_invariant_commute_rules lthy)))) lthy 
49626  455 
val relator_eq_conv = Conv.bottom_conv 
456 
(K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy 

47308  457 
in 
458 
case (Thm.term_of ctm) of 

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

49626  460 
(binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm 
461 
 _ => (invariant_commute_conv then_conv relator_eq_conv) ctm 

47308  462 
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

463 

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

51314
eac4bb5adbf9
just one HOLogic.Trueprop_conv, with regular exception CTERM;
wenzelm
parents:
49975
diff
changeset

466 
val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv) 
47308  467 
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} 
468 
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy 

469 
val beta_conv = Thm.beta_conversion true 

470 
val eq_thm = 

471 
(simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm 

472 
in 

473 
Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2) 

474 
end 

475 

47607  476 
fun rename_to_tnames ctxt term = 
477 
let 

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

479 
 all_typs _ = [] 

47308  480 

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

483 
 rename t _ = t 

484 

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

486 
val new_names = Datatype_Prop.make_tnames (all_typs fixed_def_t) 

487 
in 

488 
rename term new_names 

489 
end 

47308  490 

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

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

492 

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

493 
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

494 
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

495 

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

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

497 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

498 
fun lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy = 
47308  499 
let 
51994  500 
val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy 
501 
val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw 

502 
val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty) 

47308  503 
val rty_forced = (domain_type o fastype_of) rsp_rel; 
51994  504 
val forced_rhs = force_rty_type lthy rty_forced rhs; 
47308  505 
val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs) 
51994  506 
val opt_proven_rsp_thm = try_prove_reflexivity lthy internal_rsp_tm 
507 
val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm 

508 

509 
fun after_qed internal_rsp_thm lthy = 

510 
add_lift_def (binding, mx) qty rhs internal_rsp_thm opt_par_thm lthy 

47308  511 

512 
in 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

513 
case opt_proven_rsp_thm of 
51994  514 
SOME thm => Proof.theorem NONE (K (after_qed thm)) [] lthy 
515 
 NONE => 

516 
let 

517 
val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy 

518 
val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq) 

519 
val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm 

520 

521 
fun after_qed' thm_list lthy = 

522 
let 

523 
val internal_rsp_thm = Goal.prove lthy [] [] internal_rsp_tm 

524 
(fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac (hd thm_list) 1) 

525 
in 

526 
after_qed internal_rsp_thm lthy 

527 
end 

528 
in 

529 
Proof.theorem NONE after_qed' [[(readable_rsp_tm_tnames,[])]] lthy 

530 
end 

47308  531 
end 
532 

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

533 
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

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

535 
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

536 
["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

537 
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

538 
[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

539 
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

540 
[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

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

542 
(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

543 
[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

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

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

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

547 

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

548 
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

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

550 
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

551 
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

552 
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

553 
["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

554 
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

555 
[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

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

557 
[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

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

559 
(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

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

561 
Pretty.brk 2, 
51957  562 
Pretty.str "The type of the term cannot be instantiated to", 
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

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

564 
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

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

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

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

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

569 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

570 
fun lift_def_cmd_with_err_handling (raw_var, rhs_raw, opt_par_xthm) lthy = 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

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

572 
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

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

574 
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

575 

47308  576 
(* parser and command *) 
577 
val liftdef_parser = 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

578 
(((Parse.binding  (@{keyword "::"}  (Parse.typ >> SOME)  Parse.opt_mixfix')) >> Parse.triple2) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

579 
 @{keyword "is"}  Parse.term  Scan.option (@{keyword "parametric"}  Parse.!!! Parse_Spec.xthm)) >> Parse.triple1 
47308  580 
val _ = 
581 
Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"} 

582 
"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

583 
(liftdef_parser >> lift_def_cmd_with_err_handling) 
47308  584 

585 

586 
end; (* structure *) 