author  kuncar 
Fri, 08 Mar 2013 13:14:23 +0100  
changeset 51374  84d01fd733cf 
parent 51314  eac4bb5adbf9 
child 51927  bcd6898ac613 
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 

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

28 
(* 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

29 

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

30 
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

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

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

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

34 
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

35 
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

36 
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

37 
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

38 

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

39 
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

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

41 
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

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

43 
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

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

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

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

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

48 

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

49 
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

50 
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

51 
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

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

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

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

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

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

57 

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

58 
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

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

60 
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

61 
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

62 
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

63 
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

64 
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

65 
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

66 
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

67 
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

68 
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

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

70 
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

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

72 

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

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

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

75 
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

76 
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

77 
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

78 
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

79 
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

80 
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

81 
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

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

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

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

85 

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

86 
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

87 
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

88 
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

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

90 
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

91 
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

92 
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

93 
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

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

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

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

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

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

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

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

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

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

103 

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

104 
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

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

106 
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

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

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

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

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

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

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

113 

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

114 
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

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

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

117 
([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

118 
> Morphism.thm (Local_Theory.target_morphism lthy) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

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

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

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

122 
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

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

124 

47698  125 
(* Generation of the code certificate from the rsp theorem *) 
47308  126 

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

128 
 get_body_types (U, V) = (U, V) 

129 

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

131 
 get_binder_types _ = [] 

132 

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

133 
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

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

135 
 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

136 

70375fa2679d
generate abs_eq, use it as a 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 
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

138 
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

139 
 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

140 

47308  141 
fun force_rty_type ctxt rty rhs = 
142 
let 

143 
val thy = Proof_Context.theory_of ctxt 

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

145 
val rty_schematic = fastype_of rhs_schematic 

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

147 
in 

148 
Envir.subst_term_types match rhs_schematic 

149 
end 

150 

151 
fun unabs_def ctxt def = 

152 
let 

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

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

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

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

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

158 
val thy = Proof_Context.theory_of ctxt' 

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

160 
in 

161 
Thm.combination def refl_thm > 

162 
singleton (Proof_Context.export ctxt' ctxt) 

163 
end 

164 

165 
fun unabs_all_def ctxt def = 

166 
let 

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

168 
val xs = strip_abs_vars (term_of rhs) 

169 
in 

170 
fold (K (unabs_def ctxt)) xs def 

171 
end 

172 

173 
val map_fun_unfolded = 

174 
@{thm map_fun_def[abs_def]} > 

175 
unabs_def @{context} > 

176 
unabs_def @{context} > 

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

178 

179 
fun unfold_fun_maps ctm = 

180 
let 

181 
fun unfold_conv ctm = 

182 
case (Thm.term_of ctm) of 

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

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

185 
 _ => Conv.all_conv ctm 

186 
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

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

188 
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

189 

70375fa2679d
generate abs_eq, use it as a 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 
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

191 
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

192 
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

193 
(unfold_fun_maps then_conv try_beta_conv) ctm 
47308  194 
end 
195 

196 
fun prove_rel ctxt rsp_thm (rty, qty) = 

197 
let 

198 
val ty_args = get_binder_types (rty, qty) 

199 
fun disch_arg args_ty thm = 

200 
let 

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

201 
val quot_thm = Lifting_Term.prove_quot_thm ctxt args_ty 
47308  202 
in 
203 
[quot_thm, thm] MRSL @{thm apply_rsp''} 

204 
end 

205 
in 

206 
fold disch_arg ty_args rsp_thm 

207 
end 

208 

209 
exception CODE_CERT_GEN of string 

210 

211 
fun simplify_code_eq ctxt def_thm = 

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

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

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

215 
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

216 
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

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

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

219 

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

221 
case quot_thm_rel quot_thm of 
47308  222 
Const (@{const_name HOL.eq}, _) => true 
223 
 Const (@{const_name invariant}, _) $ _ => true 

224 
 _ => false 

225 

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

227 
let 

228 
val thy = Proof_Context.theory_of ctxt 

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

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

232 
val abs_rep_eq = 

233 
case (HOLogic.dest_Trueprop o prop_of) fun_rel of 

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

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

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

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

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

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

243 
in 

244 
simplify_code_eq ctxt code_cert 

245 
end 

246 

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

247 
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

248 
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

249 
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

250 
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

251 
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

252 
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

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

254 
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

255 

70375fa2679d
generate abs_eq, use it as a 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 
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

257 
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

258 
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

259 
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

260 
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

261 
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

262 
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

263 
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

264 
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

265 
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

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

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

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_abs_eq ctxt def_thm rsp_thm quot_thm = 
47308  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 
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

273 
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

274 
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

275 
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

276 
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

277 
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

278 
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

279 
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

280 
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

281 
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

282 

70375fa2679d
generate abs_eq, use it as a 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 
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

284 
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

285 
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

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

288 
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

289 
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

290 
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

291 

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

292 
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

293 
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

294 
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

295 

70375fa2679d
generate abs_eq, use it as a 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 
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

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

298 
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

299 
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

300 
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

301 
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

302 
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

303 

70375fa2679d
generate abs_eq, use it as a 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 
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

305 
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

306 
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

307 
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

308 
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

309 
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

310 
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

311 
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

312 
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

313 
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

314 
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

315 
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

316 
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

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

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

319 
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

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

322 
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

323 
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

324 
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

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

327 
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

328 
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

329 

70375fa2679d
generate abs_eq, use it as a 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 
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

331 
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

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

333 
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

334 
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

335 

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

336 
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

337 
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

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

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

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

343 
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

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

346 
 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

347 

70375fa2679d
generate abs_eq, use it as a 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 
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

349 
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

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

351 
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

352 
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

353 
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

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

356 
false 
47308  357 
end 
358 

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

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

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

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

364 
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

365 
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

366 
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

367 
false 
47308  368 
end 
369 

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

370 
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

371 
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

372 
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

373 
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

374 
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

375 
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

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

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

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

379 
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

380 
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

381 
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

382 
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

383 
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

384 
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

385 
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

386 
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

387 
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

388 
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

389 
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

390 
end 
47308  391 

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

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

393 
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

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

395 

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

396 
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

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

398 
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

399 
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

400 
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

401 
*) 
47308  402 

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

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

406 
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

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

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

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

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

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

414 

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

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

417 

49885
b0d6d2e7a522
don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule
kuncar
parents:
49626
diff
changeset

418 
fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) lthy' 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

419 
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

420 

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

421 
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

422 
val opt_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty) 
47351  423 

47545  424 
fun qualify defname suffix = Binding.qualified true suffix defname 
47308  425 

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

428 
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

429 
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

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

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

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

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

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

438 
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

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

440 
> define_code abs_eq_thm opt_rep_eq_thm (rty_forced, qty) 
47308  441 
end 
442 

443 
fun mk_readable_rsp_thm_eq tm lthy = 

444 
let 

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

446 

447 
fun simp_arrows_conv ctm = 

448 
let 

449 
val unfold_conv = Conv.rewrs_conv 

49626  450 
[@{thm fun_rel_eq_invariant[THEN eq_reflection]}, 
451 
@{thm fun_rel_eq[THEN eq_reflection]}, 

452 
@{thm fun_rel_eq_rel[THEN eq_reflection]}, 

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

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

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

47308  459 
in 
460 
case (Thm.term_of ctm) of 

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

49626  462 
(binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm 
463 
 _ => (invariant_commute_conv then_conv relator_eq_conv) ctm 

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

465 

47308  466 
val unfold_ret_val_invs = Conv.bottom_conv 
467 
(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

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

471 
val beta_conv = Thm.beta_conversion true 

472 
val eq_thm = 

473 
(simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm 

474 
in 

475 
Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2) 

476 
end 

477 

47607  478 
fun rename_to_tnames ctxt term = 
479 
let 

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

481 
 all_typs _ = [] 

47308  482 

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

485 
 rename t _ = t 

486 

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

488 
val new_names = Datatype_Prop.make_tnames (all_typs fixed_def_t) 

489 
in 

490 
rename term new_names 

491 
end 

47308  492 

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

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

494 

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

495 
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

496 
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

497 

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

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

499 

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

500 
fun lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy = 
47308  501 
let 
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

502 
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

503 
val rhs = (Syntax.check_term lthy' o Syntax.parse_term lthy') rhs_raw 
47308  504 

505 
fun try_to_prove_refl thm = 

506 
let 

507 
val lhs_eq = 

508 
thm 

509 
> prop_of 

510 
> Logic.dest_implies 

511 
> fst 

512 
> strip_all_body 

513 
> try HOLogic.dest_Trueprop 

514 
in 

515 
case lhs_eq of 

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

517 
 _ => NONE 

518 
end 

519 

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

520 
val rsp_rel = Lifting_Term.equiv_relation lthy' (fastype_of rhs, qty) 
47308  521 
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

522 
val forced_rhs = force_rty_type lthy' rty_forced rhs; 
47308  523 
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

524 
val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy' 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

525 
val opt_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq 
47308  526 
val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq) 
47607  527 
val readable_rsp_tm_tnames = rename_to_tnames lthy' readable_rsp_tm 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset

528 
val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy')) opt_par_xthm 
47607  529 

47308  530 
fun after_qed thm_list lthy = 
531 
let 

532 
val internal_rsp_thm = 

533 
case thm_list of 

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

534 
[] => the opt_proven_rsp_thm 
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47503
diff
changeset

535 
 [[thm]] => Goal.prove lthy [] [] internal_rsp_tm 
47308  536 
(fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1) 
537 
in 

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

538 
add_lift_def (binding, mx) qty rhs internal_rsp_thm opt_par_thm lthy 
47308  539 
end 
540 

541 
in 

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

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

543 
SOME _ => Proof.theorem NONE after_qed [] lthy' 
47607  544 
 NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm_tnames,[])]] lthy' 
47308  545 
end 
546 

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

547 
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

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

549 
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

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

551 
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

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

553 
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

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

555 
"", 
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 
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47373
diff
changeset

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

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

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

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

561 

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

562 
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

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

564 
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

565 
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

566 
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

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

568 
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

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

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

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

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

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

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

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

576 
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

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

578 
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

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

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

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

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

583 

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

584 
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

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

586 
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

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

588 
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

589 

47308  590 
(* parser and command *) 
591 
val liftdef_parser = 

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

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

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

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

597 
(liftdef_parser >> lift_def_cmd_with_err_handling) 
47308  598 

599 

600 
end; (* structure *) 