1.1 --- a/src/HOL/Lifting.thy	Tue Apr 17 16:14:07 2012 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Tue Apr 17 19:16:13 2012 +0200
     1.3 @@ -218,6 +218,10 @@
     1.4      done
     1.5  qed
     1.6  
     1.7 +lemma equivp_reflp2:
     1.8 +  "equivp R \<Longrightarrow> reflp R"
     1.9 +  by (erule equivpE)
    1.10 +
    1.11  subsection {* Invariant *}
    1.12  
    1.13  definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 

     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Apr 17 16:14:07 2012 +0100
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Apr 17 19:16:13 2012 +0200
     2.3 @@ -8,7 +8,9 @@
     2.4  sig
     2.5    exception SETUP_LIFTING_INFR of string
     2.6  
     2.7 -  val setup_lifting_infr: thm -> thm -> local_theory -> local_theory
     2.8 +  val setup_lifting_infr: thm -> local_theory -> local_theory
     2.9 +
    2.10 +  val setup_by_quotient: thm -> thm option -> local_theory -> local_theory
    2.11  
    2.12    val setup_by_typedef_thm: thm -> local_theory -> local_theory
    2.13  end;
    2.14 @@ -76,7 +78,7 @@
    2.15                                                  @ (map Pretty.string_of errs)))
    2.16    end
    2.17  
    2.18 -fun setup_lifting_infr quot_thm equiv_thm lthy =
    2.19 +fun setup_lifting_infr quot_thm lthy =
    2.20    let
    2.21      val _ = quot_thm_sanity_check lthy quot_thm
    2.22      val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
    2.23 @@ -90,36 +92,73 @@
    2.24        |> define_abs_type quot_thm
    2.25    end
    2.26  
    2.27 +fun setup_by_quotient quot_thm maybe_reflp_thm lthy =
    2.28 +  let
    2.29 +    val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    2.30 +    val lthy' = case maybe_reflp_thm of
    2.31 +      SOME reflp_thm => lthy
    2.32 +        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.33 +          [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
    2.34 +        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.35 +          [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
    2.36 +      | NONE => lthy
    2.37 +  in
    2.38 +    lthy'
    2.39 +      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.40 +        [quot_thm RS @{thm Quotient_right_unique}])
    2.41 +      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.42 +        [quot_thm RS @{thm Quotient_right_total}])
    2.43 +      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.44 +        [quot_thm RS @{thm Quotient_rel_eq_transfer}])
    2.45 +      |> setup_lifting_infr quot_thm
    2.46 +  end
    2.47 +
    2.48  fun setup_by_typedef_thm typedef_thm lthy =
    2.49    let
    2.50 -    fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy =
    2.51 -      let
    2.52 -        val (_ $ rep_fun $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
    2.53 -        val equiv_thm = typedef_thm RS to_equiv_thm
    2.54 -        val (T_def, lthy') = define_cr_rel rep_fun lthy
    2.55 -        val quot_thm =  [typedef_thm, T_def] MRSL to_quot_thm
    2.56 -      in
    2.57 -        (quot_thm, equiv_thm, lthy')
    2.58 -      end
    2.59 +    val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    2.60 +    val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
    2.61 +    val (T_def, lthy') = define_cr_rel rep_fun lthy
    2.62 +    
    2.63 +    val quot_thm = (case typedef_set of
    2.64 +      Const ("Orderings.top_class.top", _) => 
    2.65 +        [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
    2.66 +      | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
    2.67 +        [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
    2.68 +      | _ => 
    2.69 +        [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient})
    2.70  
    2.71 -    val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
    2.72 -    val (quot_thm, equiv_thm, lthy') = (case typedef_set of
    2.73 -      Const ("Orderings.top_class.top", _) => 
    2.74 -        derive_quot_and_equiv_thm @{thm UNIV_typedef_to_Quotient} @{thm UNIV_typedef_to_equivp} 
    2.75 -          typedef_thm lthy
    2.76 -      | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
    2.77 -        derive_quot_and_equiv_thm @{thm open_typedef_to_Quotient} @{thm open_typedef_to_part_equivp} 
    2.78 -          typedef_thm lthy
    2.79 -      | _ => derive_quot_and_equiv_thm @{thm typedef_to_Quotient} @{thm typedef_to_part_equivp} 
    2.80 -          typedef_thm lthy)
    2.81 +    val lthy'' = (case typedef_set of
    2.82 +      Const ("Orderings.top_class.top", _) => (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.83 +        [[typedef_thm,T_def] MRSL @{thm copy_type_bi_total}]) lthy'
    2.84 +      | _ => lthy')
    2.85    in
    2.86 -    setup_lifting_infr quot_thm equiv_thm lthy'
    2.87 +    lthy''
    2.88 +      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.89 +        [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
    2.90 +      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.91 +        [T_def RS @{thm typedef_right_total}])
    2.92 +      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.93 +        [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}])
    2.94 +      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.95 +        [[typedef_thm, T_def] MRSL @{thm typedef_transfer_Ex}])
    2.96 +      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.97 +        [[typedef_thm, T_def] MRSL @{thm typedef_transfer_bforall}])
    2.98 +      |> setup_lifting_infr quot_thm
    2.99    end
   2.100  
   2.101 -fun setup_by_typedef_thm_aux xthm lthy = setup_by_typedef_thm (singleton (Attrib.eval_thms lthy) xthm) lthy
   2.102 +fun setup_lifting_cmd xthm lthy =
   2.103 +  let 
   2.104 +    val input_thm = singleton (Attrib.eval_thms lthy) xthm
   2.105 +    val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
   2.106 +  in
   2.107 +    case input_term of
   2.108 +      (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_lifting_infr input_thm lthy
   2.109 +      | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_by_typedef_thm input_thm lthy
   2.110 +      | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   2.111 +  end
   2.112  
   2.113  val _ = 
   2.114    Outer_Syntax.local_theory @{command_spec "setup_lifting"}
   2.115      "Setup lifting infrastructure" 
   2.116 -      (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))
   2.117 +      (Parse_Spec.xthm >> (fn xthm => setup_lifting_cmd xthm))
   2.118  end;

     3.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Tue Apr 17 16:14:07 2012 +0100
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Tue Apr 17 19:16:13 2012 +0200
     3.3 @@ -139,16 +139,18 @@
     3.4      val (rty, qty) = (dest_funT o fastype_of) abs_fun
     3.5      val qty_name = (fst o dest_Type) qty
     3.6      val quotient_thm_name = Binding.prefix_name "Quotient_" (Binding.qualified_name qty_name) 
     3.7 -    val quot_thm = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
     3.8 -      Const (@{const_name equivp}, _) $ _ => 
     3.9 -        [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}
    3.10 -      | Const (@{const_name part_equivp}, _) $ _ => 
    3.11 -        [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient}
    3.12 +    val (reflp_thm, quot_thm) = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
    3.13 +      Const (@{const_name equivp}, _) $ _ =>
    3.14 +        (SOME (equiv_thm RS @{thm equivp_reflp2}),
    3.15 +         [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp})
    3.16 +      | Const (@{const_name part_equivp}, _) $ _ =>
    3.17 +        (NONE,
    3.18 +        [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient})
    3.19        | _ => error "unsupported equivalence theorem"
    3.20        )
    3.21    in
    3.22      lthy'
    3.23 -      |> Lifting_Setup.setup_lifting_infr quot_thm equiv_thm
    3.24 +      |> Lifting_Setup.setup_by_quotient quot_thm reflp_thm
    3.25        |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
    3.26    end
    3.27  

     4.1 --- a/src/HOL/Word/Word.thy	Tue Apr 17 16:14:07 2012 +0100
     4.2 +++ b/src/HOL/Word/Word.thy	Tue Apr 17 19:16:13 2012 +0200
     4.3 @@ -244,26 +244,10 @@
     4.4    by (simp add: reflp_def)
     4.5  
     4.6  local_setup {*
     4.7 -  Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm reflp_word}
     4.8 +  Lifting_Setup.setup_by_quotient @{thm Quotient_word} (SOME @{thm reflp_word})
     4.9  *}
    4.10  
    4.11 -text {* TODO: The next several lemmas could be generated automatically. *}
    4.12 -
    4.13 -lemma bi_total_cr_word [transfer_rule]: "bi_total cr_word"
    4.14 -  using Quotient_word reflp_word by (rule Quotient_bi_total)
    4.15 -
    4.16 -lemma right_unique_cr_word [transfer_rule]: "right_unique cr_word"
    4.17 -  using Quotient_word by (rule Quotient_right_unique)
    4.18 -
    4.19 -lemma word_eq_transfer [transfer_rule]:
    4.20 -  "(fun_rel cr_word (fun_rel cr_word op =))
    4.21 -    (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
    4.22 -    (op = :: 'a::len0 word \<Rightarrow> 'a word \<Rightarrow> bool)"
    4.23 -  using Quotient_word by (rule Quotient_rel_eq_transfer)
    4.24 -
    4.25 -lemma word_of_int_transfer [transfer_rule]:
    4.26 -  "(fun_rel op = cr_word) (\<lambda>x. x) word_of_int"
    4.27 -  using Quotient_word reflp_word by (rule Quotient_id_abs_transfer)
    4.28 +text {* TODO: The next lemma could be generated automatically. *}
    4.29  
    4.30  lemma uint_transfer [transfer_rule]:
    4.31    "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a)))