--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Thu Apr 10 17:48:18 2014 +0200
@@ -0,0 +1,118 @@
+(* Title: HOL/Tools/Transfer/transfer_bnf.ML
+ Author: Ondrej Kuncar, TU Muenchen
+
+Setup for Lifting for types that are BNF.
+*)
+
+signature LIFTING_BNF =
+sig
+end
+
+structure Lifting_BNF : LIFTING_BNF =
+struct
+
+open BNF_Util
+open BNF_Def
+open Transfer_BNF
+
+(* Quotient map theorem *)
+
+fun Quotient_tac bnf ctxt i =
+ let
+ val rel_Grp = rel_Grp_of_bnf bnf
+ fun get_lhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
+ val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
+ val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
+ val inst = map2 (curry(pairself (certify ctxt))) vars UNIVs
+ val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst)
+ |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
+ |> (fn thm => thm RS sym)
+ val rel_mono = rel_mono_of_bnf bnf
+ val rel_conversep_sym = rel_conversep_of_bnf bnf RS sym
+ in
+ EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Quotient_alt_def5}]),
+ REPEAT_DETERM o (etac conjE), rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_Grp_UNIV_sym]),
+ rtac rel_mono THEN_ALL_NEW atac, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt
+ [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW atac,
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]),
+ hyp_subst_tac ctxt, rtac refl] i
+ end
+
+fun mk_Quotient args =
+ let
+ val argTs = map fastype_of args
+ in
+ list_comb (Const (@{const_name Quotient}, argTs ---> HOLogic.boolT), args)
+ end
+
+fun prove_Quotient_map bnf ctxt =
+ let
+ val live = live_of_bnf bnf
+ val old_ctxt = ctxt
+ val (((As, Bs), Ds), ctxt) = ctxt
+ |> mk_TFrees live
+ ||>> mk_TFrees live
+ ||>> mk_TFrees (dead_of_bnf bnf)
+ val argTss = map2 (fn a => fn b => [mk_pred2T a a, a --> b, b --> a,mk_pred2T a b]) As Bs
+ val ((argss, argss'), ctxt) = fold_map2 mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt
+ |>> `transpose
+
+ val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss
+ val R_rel = list_comb (mk_rel_of_bnf Ds As As bnf, nth argss' 0)
+ val Abs_map = list_comb (mk_map_of_bnf Ds As Bs bnf, nth argss' 1)
+ val Rep_map = list_comb (mk_map_of_bnf Ds Bs As bnf, nth argss' 2)
+ val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3)
+ val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop
+ val goal = Logic.list_implies (assms, concl)
+ val thm = Goal.prove ctxt [] [] goal
+ (fn {context = ctxt, prems = _} => Quotient_tac bnf ctxt 1)
+ in
+ Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
+ end
+
+
+fun Quotient_map bnf ctxt =
+ let
+ val Quotient = prove_Quotient_map bnf ctxt
+ fun qualify defname suffix = Binding.qualified true suffix defname
+ val Quotient_thm_name = qualify (base_name_of_bnf bnf) "Quotient"
+ val notes = [((Quotient_thm_name, []), [([Quotient], @{attributes [quot_map]})])]
+ in
+ notes
+ end
+
+(* relator_eq_onp *)
+
+fun relator_eq_onp bnf ctxt =
+ let
+ val pred_data = lookup_defined_pred_data ctxt (type_name_of_bnf bnf)
+ in
+ [((Binding.empty, []), [([Transfer.rel_eq_onp pred_data], @{attributes [relator_eq_onp]})])]
+ end
+
+(* relator_mono *)
+
+fun relator_mono bnf =
+ [((Binding.empty, []), [([rel_mono_of_bnf bnf], @{attributes [relator_mono]})])]
+
+(* relator_distr *)
+
+fun relator_distr bnf =
+ [((Binding.empty, []), [([rel_OO_of_bnf bnf RS sym], @{attributes [relator_distr]})])]
+
+(* interpretation *)
+
+fun lifting_bnf_interpretation bnf lthy =
+ if dead_of_bnf bnf > 0 then lthy
+ else
+ let
+ val notes = relator_eq_onp bnf lthy @ Quotient_map bnf lthy @ relator_mono bnf
+ @ relator_distr bnf
+ in
+ snd (Local_Theory.notes notes lthy)
+ end
+
+val _ = Context.>> (Context.map_theory (bnf_interpretation
+ (bnf_only_type_ctr (fn bnf => map_local_theory (lifting_bnf_interpretation bnf)))))
+
+end