1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Thu Apr 10 17:48:18 2014 +0200
     1.3 @@ -0,0 +1,118 @@
     1.4 +(*  Title:      HOL/Tools/Transfer/transfer_bnf.ML
     1.5 +    Author:     Ondrej Kuncar, TU Muenchen
     1.6 +
     1.7 +Setup for Lifting for types that are BNF.
     1.8 +*)
     1.9 +
    1.10 +signature LIFTING_BNF =
    1.11 +sig
    1.12 +end
    1.13 +
    1.14 +structure Lifting_BNF : LIFTING_BNF =
    1.15 +struct
    1.16 +
    1.17 +open BNF_Util
    1.18 +open BNF_Def
    1.19 +open Transfer_BNF
    1.20 +
    1.21 +(* Quotient map theorem *)
    1.22 +
    1.23 +fun Quotient_tac bnf ctxt i =
    1.24 +  let
    1.25 +    val rel_Grp = rel_Grp_of_bnf bnf
    1.26 +    fun get_lhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
    1.27 +    val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
    1.28 +    val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
    1.29 +    val inst = map2 (curry(pairself (certify ctxt))) vars UNIVs
    1.30 +    val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst) 
    1.31 +      |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
    1.32 +      |> (fn thm => thm RS sym)
    1.33 +    val rel_mono = rel_mono_of_bnf bnf
    1.34 +    val rel_conversep_sym = rel_conversep_of_bnf bnf RS sym
    1.35 +  in
    1.36 +    EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Quotient_alt_def5}]), 
    1.37 +      REPEAT_DETERM o (etac conjE), rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_Grp_UNIV_sym]),
    1.38 +      rtac rel_mono THEN_ALL_NEW atac, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.39 +        [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW atac,
    1.40 +      SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]),
    1.41 +      hyp_subst_tac ctxt, rtac refl] i
    1.42 +  end
    1.43 +
    1.44 +fun mk_Quotient args =
    1.45 +  let
    1.46 +    val argTs = map fastype_of args
    1.47 +  in
    1.48 +    list_comb (Const (@{const_name Quotient}, argTs ---> HOLogic.boolT), args)
    1.49 +  end
    1.50 +
    1.51 +fun prove_Quotient_map bnf ctxt =
    1.52 +  let
    1.53 +    val live = live_of_bnf bnf
    1.54 +    val old_ctxt = ctxt
    1.55 +    val (((As, Bs), Ds), ctxt) = ctxt
    1.56 +      |> mk_TFrees live
    1.57 +      ||>> mk_TFrees live
    1.58 +      ||>> mk_TFrees (dead_of_bnf bnf)
    1.59 +    val argTss = map2 (fn a => fn b => [mk_pred2T a a, a --> b, b --> a,mk_pred2T a b]) As Bs
    1.60 +    val ((argss, argss'), ctxt) = fold_map2 mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt
    1.61 +      |>> `transpose
    1.62 +   
    1.63 +    val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss
    1.64 +    val R_rel = list_comb (mk_rel_of_bnf Ds As As bnf, nth argss' 0)
    1.65 +    val Abs_map = list_comb (mk_map_of_bnf Ds As Bs bnf, nth argss' 1)
    1.66 +    val Rep_map = list_comb (mk_map_of_bnf Ds Bs As bnf, nth argss' 2)
    1.67 +    val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3)
    1.68 +    val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop
    1.69 +    val goal = Logic.list_implies (assms, concl)
    1.70 +    val thm = Goal.prove ctxt [] [] goal 
    1.71 +      (fn {context = ctxt, prems = _} => Quotient_tac bnf ctxt 1)
    1.72 +  in
    1.73 +    Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
    1.74 +  end
    1.75 +
    1.76 +
    1.77 +fun Quotient_map bnf ctxt =
    1.78 +  let
    1.79 +    val Quotient = prove_Quotient_map bnf ctxt
    1.80 +    fun qualify defname suffix = Binding.qualified true suffix defname
    1.81 +    val Quotient_thm_name = qualify (base_name_of_bnf bnf) "Quotient"
    1.82 +    val notes = [((Quotient_thm_name, []), [([Quotient], @{attributes [quot_map]})])]
    1.83 +  in
    1.84 +    notes
    1.85 +  end
    1.86 +
    1.87 +(* relator_eq_onp  *)
    1.88 +
    1.89 +fun relator_eq_onp bnf ctxt =
    1.90 +  let
    1.91 +    val pred_data = lookup_defined_pred_data ctxt (type_name_of_bnf bnf)
    1.92 +  in
    1.93 +    [((Binding.empty, []), [([Transfer.rel_eq_onp pred_data], @{attributes [relator_eq_onp]})])]    
    1.94 +  end
    1.95 +
    1.96 +(* relator_mono  *)
    1.97 +
    1.98 +fun relator_mono bnf =
    1.99 +  [((Binding.empty, []), [([rel_mono_of_bnf bnf], @{attributes [relator_mono]})])]    
   1.100 +  
   1.101 +(* relator_distr  *)
   1.102 +
   1.103 +fun relator_distr bnf =
   1.104 +  [((Binding.empty, []), [([rel_OO_of_bnf bnf RS sym], @{attributes [relator_distr]})])]
   1.105 +
   1.106 +(* interpretation *)
   1.107 +
   1.108 +fun lifting_bnf_interpretation bnf lthy =
   1.109 +  if dead_of_bnf bnf > 0 then lthy
   1.110 +  else
   1.111 +    let
   1.112 +      val notes = relator_eq_onp bnf lthy @ Quotient_map bnf lthy @ relator_mono bnf
   1.113 +        @ relator_distr bnf
   1.114 +    in
   1.115 +      snd (Local_Theory.notes notes lthy)
   1.116 +    end
   1.117 +
   1.118 +val _ = Context.>> (Context.map_theory (bnf_interpretation
   1.119 +  (bnf_only_type_ctr (fn bnf => map_local_theory (lifting_bnf_interpretation bnf)))))
   1.120 +
   1.121 +end