src/HOL/Tools/Lifting/lifting_setup.ML
author kuncar
Wed Apr 18 17:04:03 2012 +0200 (2012-04-18)
changeset 47545 a2850a16e30f
parent 47535 0f94b02fda1c
child 47566 c201a1fe0a81
permissions -rw-r--r--
Lifting: generate more thms & note them & tuned
     1 (*  Title:      HOL/Tools/Lifting/lifting_setup.ML
     2     Author:     Ondrej Kuncar
     3 
     4 Setting up the lifting infrastructure.
     5 *)
     6 
     7 signature LIFTING_SETUP =
     8 sig
     9   exception SETUP_LIFTING_INFR of string
    10 
    11   val setup_lifting_infr: thm -> local_theory -> local_theory
    12 
    13   val setup_by_quotient: thm -> thm option -> local_theory -> local_theory
    14 
    15   val setup_by_typedef_thm: thm -> local_theory -> local_theory
    16 end;
    17 
    18 structure Lifting_Setup: LIFTING_SETUP =
    19 struct
    20 
    21 infix 0 MRSL
    22 
    23 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    24 
    25 exception SETUP_LIFTING_INFR of string
    26 
    27 fun define_cr_rel rep_fun lthy =
    28   let
    29     val (qty, rty) = (dest_funT o fastype_of) rep_fun
    30     val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
    31     val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph));
    32     val qty_name = (fst o dest_Type) qty
    33     val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)  
    34     val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
    35     val ((_, (_ , def_thm)), lthy'') =
    36       Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
    37   in
    38     (def_thm, lthy'')
    39   end
    40 
    41 fun define_abs_type quot_thm lthy =
    42   if Lifting_Def.can_generate_code_cert quot_thm then
    43     let
    44       val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
    45       val add_abstype_attribute = 
    46           Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
    47         val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
    48     in
    49       lthy
    50         |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
    51     end
    52   else
    53     lthy
    54 
    55 fun quot_thm_sanity_check ctxt quot_thm =
    56   let
    57     val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
    58     val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm_fixed
    59     val rty_tfreesT = Term.add_tfree_namesT rty []
    60     val qty_tfreesT = Term.add_tfree_namesT qty []
    61     val extra_rty_tfrees =
    62       case subtract (op =) qty_tfreesT rty_tfreesT of
    63         [] => []
    64       | extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
    65                                  Pretty.brk 1] @ 
    66                                  ((Pretty.commas o map (Pretty.str o quote)) extras) @
    67                                  [Pretty.str "."])]
    68     val not_type_constr = 
    69       case qty of
    70          Type _ => []
    71          | _ => [Pretty.block [Pretty.str "The quotient type ",
    72                                 Pretty.quote (Syntax.pretty_typ ctxt' qty),
    73                                 Pretty.brk 1,
    74                                 Pretty.str "is not a type constructor."]]
    75     val errs = extra_rty_tfrees @ not_type_constr
    76   in
    77     if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] 
    78                                                 @ (map Pretty.string_of errs)))
    79   end
    80 
    81 fun setup_lifting_infr quot_thm lthy =
    82   let
    83     val _ = quot_thm_sanity_check lthy quot_thm
    84     val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
    85     val qty_full_name = (fst o dest_Type) qtyp
    86     val quotients = { quot_thm = quot_thm }
    87     fun quot_info phi = Lifting_Info.transform_quotients phi quotients
    88   in
    89     lthy
    90       |> Local_Theory.declaration {syntax = false, pervasive = true}
    91         (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
    92       |> define_abs_type quot_thm
    93   end
    94 
    95 fun setup_by_quotient quot_thm maybe_reflp_thm lthy =
    96   let
    97     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    98     val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
    99     val qty_name = (Binding.name o fst o dest_Type) qty
   100     fun qualify suffix = Binding.qualified true suffix qty_name
   101     val lthy' = case maybe_reflp_thm of
   102       SOME reflp_thm => lthy
   103         |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), 
   104           [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
   105         |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
   106           [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
   107       | NONE => lthy
   108         |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
   109           [quot_thm RS @{thm Quotient_All_transfer}])
   110         |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), 
   111           [quot_thm RS @{thm Quotient_Ex_transfer}])
   112         |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
   113           [quot_thm RS @{thm Quotient_forall_transfer}])
   114   in
   115     lthy'
   116       |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), 
   117         [quot_thm RS @{thm Quotient_right_unique}])
   118       |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
   119         [quot_thm RS @{thm Quotient_right_total}])
   120       |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), 
   121         [quot_thm RS @{thm Quotient_rel_eq_transfer}])
   122       |> setup_lifting_infr quot_thm
   123   end
   124 
   125 fun setup_by_typedef_thm typedef_thm lthy =
   126   let
   127     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
   128     val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
   129     val (T_def, lthy') = define_cr_rel rep_fun lthy
   130 
   131     val quot_thm = case typedef_set of
   132       Const ("Orderings.top_class.top", _) => 
   133         [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
   134       | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
   135         [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
   136       | _ => 
   137         [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
   138 
   139     val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
   140     val qty_name = (Binding.name o fst o dest_Type) qty
   141     fun qualify suffix = Binding.qualified true suffix qty_name
   142 
   143     val lthy'' = case typedef_set of
   144       Const ("Orderings.top_class.top", _) => 
   145         let
   146           val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp}
   147           val reflp_thm = equivp_thm RS @{thm equivp_reflp2}
   148         in
   149           lthy'
   150             |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), 
   151               [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
   152             |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
   153               [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
   154         end
   155       | _ => lthy'
   156         |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
   157           [[typedef_thm, T_def] MRSL @{thm typedef_All_transfer}])
   158         |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), 
   159           [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}])
   160         |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
   161           [[typedef_thm, T_def] MRSL @{thm typedef_forall_transfer}])
   162   in
   163     lthy''
   164       |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), 
   165         [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
   166       |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]), 
   167         [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
   168       |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), 
   169         [[quot_thm] MRSL @{thm Quotient_right_unique}])
   170       |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
   171         [[quot_thm] MRSL @{thm Quotient_right_total}])
   172       |> setup_lifting_infr quot_thm
   173   end
   174 
   175 fun setup_lifting_cmd xthm lthy =
   176   let 
   177     val input_thm = singleton (Attrib.eval_thms lthy) xthm
   178     val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
   179   in
   180     case input_term of
   181       (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_lifting_infr input_thm lthy
   182       | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_by_typedef_thm input_thm lthy
   183       | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   184   end
   185 
   186 val _ = 
   187   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
   188     "Setup lifting infrastructure" 
   189       (Parse_Spec.xthm >> (fn xthm => setup_lifting_cmd xthm))
   190 end;