1.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 18 23:13:11 2012 +0200
1.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 18 23:57:44 2012 +0200
1.3 @@ -8,11 +8,11 @@
1.4 sig
1.5 exception SETUP_LIFTING_INFR of string
1.6
1.7 - val setup_lifting_infr: thm -> local_theory -> local_theory
1.8 + val setup_lifting_infr: bool -> thm -> local_theory -> local_theory
1.9
1.10 - val setup_by_quotient: thm -> thm option -> local_theory -> local_theory
1.11 + val setup_by_quotient: bool -> thm -> thm option -> local_theory -> local_theory
1.12
1.13 - val setup_by_typedef_thm: thm -> local_theory -> local_theory
1.14 + val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
1.15 end;
1.16
1.17 structure Lifting_Setup: LIFTING_SETUP =
1.18 @@ -38,8 +38,8 @@
1.19 (def_thm, lthy'')
1.20 end
1.21
1.22 -fun define_abs_type quot_thm lthy =
1.23 - if Lifting_Def.can_generate_code_cert quot_thm then
1.24 +fun define_abs_type no_code quot_thm lthy =
1.25 + if not no_code andalso Lifting_Def.can_generate_code_cert quot_thm then
1.26 let
1.27 val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
1.28 val add_abstype_attribute =
1.29 @@ -78,7 +78,7 @@
1.30 @ (map Pretty.string_of errs)))
1.31 end
1.32
1.33 -fun setup_lifting_infr quot_thm lthy =
1.34 +fun setup_lifting_infr no_code quot_thm lthy =
1.35 let
1.36 val _ = quot_thm_sanity_check lthy quot_thm
1.37 val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
1.38 @@ -89,10 +89,10 @@
1.39 lthy
1.40 |> Local_Theory.declaration {syntax = false, pervasive = true}
1.41 (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
1.42 - |> define_abs_type quot_thm
1.43 + |> define_abs_type no_code quot_thm
1.44 end
1.45
1.46 -fun setup_by_quotient quot_thm maybe_reflp_thm lthy =
1.47 +fun setup_by_quotient no_code quot_thm maybe_reflp_thm lthy =
1.48 let
1.49 val transfer_attr = Attrib.internal (K Transfer.transfer_add)
1.50 val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
1.51 @@ -119,10 +119,10 @@
1.52 [quot_thm RS @{thm Quotient_right_total}])
1.53 |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]),
1.54 [quot_thm RS @{thm Quotient_rel_eq_transfer}])
1.55 - |> setup_lifting_infr quot_thm
1.56 + |> setup_lifting_infr no_code quot_thm
1.57 end
1.58
1.59 -fun setup_by_typedef_thm typedef_thm lthy =
1.60 +fun setup_by_typedef_thm no_code typedef_thm lthy =
1.61 let
1.62 val transfer_attr = Attrib.internal (K Transfer.transfer_add)
1.63 val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
1.64 @@ -169,22 +169,53 @@
1.65 [[quot_thm] MRSL @{thm Quotient_right_unique}])
1.66 |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]),
1.67 [[quot_thm] MRSL @{thm Quotient_right_total}])
1.68 - |> setup_lifting_infr quot_thm
1.69 + |> setup_lifting_infr no_code quot_thm
1.70 end
1.71
1.72 -fun setup_lifting_cmd xthm lthy =
1.73 +fun setup_lifting_cmd no_code xthm opt_reflp_xthm lthy =
1.74 let
1.75 val input_thm = singleton (Attrib.eval_thms lthy) xthm
1.76 val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
1.77 + handle TERM _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
1.78 +
1.79 + fun sanity_check_reflp_thm reflp_thm =
1.80 + let
1.81 + val reflp_tm = (HOLogic.dest_Trueprop o prop_of) reflp_thm
1.82 + handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
1.83 + in
1.84 + case reflp_tm of
1.85 + Const (@{const_name reflp}, _) $ _ => ()
1.86 + | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
1.87 + end
1.88 +
1.89 + fun setup_quotient () =
1.90 + case opt_reflp_xthm of
1.91 + SOME reflp_xthm =>
1.92 + let
1.93 + val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm
1.94 + val _ = sanity_check_reflp_thm reflp_thm
1.95 + in
1.96 + setup_by_quotient no_code input_thm (SOME reflp_thm) lthy
1.97 + end
1.98 + | NONE => setup_by_quotient no_code input_thm NONE lthy
1.99 +
1.100 + fun setup_typedef () =
1.101 + case opt_reflp_xthm of
1.102 + SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
1.103 + | NONE => setup_by_typedef_thm no_code input_thm lthy
1.104 in
1.105 case input_term of
1.106 - (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_lifting_infr input_thm lthy
1.107 - | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_by_typedef_thm input_thm lthy
1.108 + (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
1.109 + | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_typedef ()
1.110 | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
1.111 end
1.112
1.113 +val opt_no_code =
1.114 + Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K true) --| @{keyword ")"})) false
1.115 +
1.116 val _ =
1.117 Outer_Syntax.local_theory @{command_spec "setup_lifting"}
1.118 "Setup lifting infrastructure"
1.119 - (Parse_Spec.xthm >> (fn xthm => setup_lifting_cmd xthm))
1.120 + (opt_no_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >>
1.121 + (fn ((no_code, xthm), opt_reflp_xthm) => setup_lifting_cmd no_code xthm opt_reflp_xthm))
1.122 end;