Lifting: generate more thms & note them & tuned
authorkuncar
Wed Apr 18 17:04:03 2012 +0200 (2012-04-18)
changeset 47545a2850a16e30f
parent 47544 e455cdaac479
child 47546 2d49b0c9d8ec
Lifting: generate more thms & note them & tuned
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_setup.ML
     1.1 --- a/src/HOL/Lifting.thy	Wed Apr 18 15:48:32 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 18 17:04:03 2012 +0200
     1.3 @@ -353,39 +353,27 @@
     1.4    unfolding bi_unique_def T_def
     1.5    by (simp add: type_definition.Rep_inject [OF type])
     1.6  
     1.7 -lemma typedef_right_total: "right_total T"
     1.8 -  unfolding right_total_def T_def by simp
     1.9 -
    1.10  lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
    1.11    unfolding fun_rel_def T_def by simp
    1.12  
    1.13 -lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
    1.14 -  unfolding T_def fun_rel_def
    1.15 -  by (metis type_definition.Rep [OF type]
    1.16 -    type_definition.Abs_inverse [OF type])
    1.17 -
    1.18 -lemma typedef_transfer_Ex: "((T ===> op =) ===> op =) (Bex A) Ex"
    1.19 +lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All"
    1.20    unfolding T_def fun_rel_def
    1.21    by (metis type_definition.Rep [OF type]
    1.22      type_definition.Abs_inverse [OF type])
    1.23  
    1.24 -lemma typedef_transfer_bforall:
    1.25 +lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex"
    1.26 +  unfolding T_def fun_rel_def
    1.27 +  by (metis type_definition.Rep [OF type]
    1.28 +    type_definition.Abs_inverse [OF type])
    1.29 +
    1.30 +lemma typedef_forall_transfer:
    1.31    "((T ===> op =) ===> op =)
    1.32      (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
    1.33    unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
    1.34 -  by (rule typedef_transfer_All)
    1.35 +  by (rule typedef_All_transfer)
    1.36  
    1.37  end
    1.38  
    1.39 -text {* Generating transfer rules for a type copy. *}
    1.40 -
    1.41 -lemma copy_type_bi_total:
    1.42 -  assumes type: "type_definition Rep Abs UNIV"
    1.43 -  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.44 -  shows "bi_total T"
    1.45 -  unfolding bi_total_def T_def
    1.46 -  by (metis type_definition.Abs_inverse [OF type] UNIV_I)
    1.47 -
    1.48  text {* Generating the correspondence rule for a constant defined with
    1.49    @{text "lift_definition"}. *}
    1.50  
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 18 15:48:32 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 18 17:04:03 2012 +0200
     2.3 @@ -180,10 +180,9 @@
     2.4      val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
     2.5          |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
     2.6  
     2.7 -    fun qualify defname suffix = Binding.name suffix
     2.8 -      |> Binding.qualify true defname
     2.9 +    fun qualify defname suffix = Binding.qualified true suffix defname
    2.10  
    2.11 -    val lhs_name = Binding.name_of (#1 var)
    2.12 +    val lhs_name = (#1 var)
    2.13      val rsp_thm_name = qualify lhs_name "rsp"
    2.14      val code_eqn_thm_name = qualify lhs_name "rep_eq"
    2.15      val transfer_thm_name = qualify lhs_name "transfer"
     3.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 15:48:32 2012 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 17:04:03 2012 +0200
     3.3 @@ -59,19 +59,19 @@
     3.4      val rty_tfreesT = Term.add_tfree_namesT rty []
     3.5      val qty_tfreesT = Term.add_tfree_namesT qty []
     3.6      val extra_rty_tfrees =
     3.7 -      (case subtract (op =) qty_tfreesT rty_tfreesT of
     3.8 +      case subtract (op =) qty_tfreesT rty_tfreesT of
     3.9          [] => []
    3.10        | extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
    3.11                                   Pretty.brk 1] @ 
    3.12                                   ((Pretty.commas o map (Pretty.str o quote)) extras) @
    3.13 -                                 [Pretty.str "."])])
    3.14 +                                 [Pretty.str "."])]
    3.15      val not_type_constr = 
    3.16 -      (case qty of
    3.17 +      case qty of
    3.18           Type _ => []
    3.19           | _ => [Pretty.block [Pretty.str "The quotient type ",
    3.20                                  Pretty.quote (Syntax.pretty_typ ctxt' qty),
    3.21                                  Pretty.brk 1,
    3.22 -                                Pretty.str "is not a type constructor."]])
    3.23 +                                Pretty.str "is not a type constructor."]]
    3.24      val errs = extra_rty_tfrees @ not_type_constr
    3.25    in
    3.26      if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] 
    3.27 @@ -95,20 +95,29 @@
    3.28  fun setup_by_quotient quot_thm maybe_reflp_thm lthy =
    3.29    let
    3.30      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    3.31 +    val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
    3.32 +    val qty_name = (Binding.name o fst o dest_Type) qty
    3.33 +    fun qualify suffix = Binding.qualified true suffix qty_name
    3.34      val lthy' = case maybe_reflp_thm of
    3.35        SOME reflp_thm => lthy
    3.36 -        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    3.37 +        |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), 
    3.38            [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
    3.39 -        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    3.40 +        |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
    3.41            [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
    3.42        | NONE => lthy
    3.43 +        |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
    3.44 +          [quot_thm RS @{thm Quotient_All_transfer}])
    3.45 +        |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), 
    3.46 +          [quot_thm RS @{thm Quotient_Ex_transfer}])
    3.47 +        |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
    3.48 +          [quot_thm RS @{thm Quotient_forall_transfer}])
    3.49    in
    3.50      lthy'
    3.51 -      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    3.52 +      |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), 
    3.53          [quot_thm RS @{thm Quotient_right_unique}])
    3.54 -      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    3.55 +      |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
    3.56          [quot_thm RS @{thm Quotient_right_total}])
    3.57 -      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    3.58 +      |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), 
    3.59          [quot_thm RS @{thm Quotient_rel_eq_transfer}])
    3.60        |> setup_lifting_infr quot_thm
    3.61    end
    3.62 @@ -118,33 +127,48 @@
    3.63      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    3.64      val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
    3.65      val (T_def, lthy') = define_cr_rel rep_fun lthy
    3.66 -    
    3.67 -    val quot_thm = (case typedef_set of
    3.68 +
    3.69 +    val quot_thm = case typedef_set of
    3.70        Const ("Orderings.top_class.top", _) => 
    3.71          [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
    3.72        | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
    3.73          [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
    3.74        | _ => 
    3.75 -        [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient})
    3.76 +        [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
    3.77 +
    3.78 +    val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
    3.79 +    val qty_name = (Binding.name o fst o dest_Type) qty
    3.80 +    fun qualify suffix = Binding.qualified true suffix qty_name
    3.81  
    3.82 -    val lthy'' = (case typedef_set of
    3.83 -      Const ("Orderings.top_class.top", _) => (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    3.84 -        [[typedef_thm,T_def] MRSL @{thm copy_type_bi_total}]) lthy'
    3.85 -      | _ => lthy')
    3.86 +    val lthy'' = case typedef_set of
    3.87 +      Const ("Orderings.top_class.top", _) => 
    3.88 +        let
    3.89 +          val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp}
    3.90 +          val reflp_thm = equivp_thm RS @{thm equivp_reflp2}
    3.91 +        in
    3.92 +          lthy'
    3.93 +            |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), 
    3.94 +              [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
    3.95 +            |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
    3.96 +              [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
    3.97 +        end
    3.98 +      | _ => lthy'
    3.99 +        |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
   3.100 +          [[typedef_thm, T_def] MRSL @{thm typedef_All_transfer}])
   3.101 +        |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), 
   3.102 +          [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}])
   3.103 +        |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
   3.104 +          [[typedef_thm, T_def] MRSL @{thm typedef_forall_transfer}])
   3.105    in
   3.106      lthy''
   3.107 -      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
   3.108 +      |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), 
   3.109          [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
   3.110 -      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
   3.111 -        [[typedef_thm, T_def] MRSL @{thm typedef_right_total}])
   3.112 -      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
   3.113 +      |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]), 
   3.114          [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
   3.115 -      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
   3.116 -        [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}])
   3.117 -      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
   3.118 -        [[typedef_thm, T_def] MRSL @{thm typedef_transfer_Ex}])
   3.119 -      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
   3.120 -        [[typedef_thm, T_def] MRSL @{thm typedef_transfer_bforall}])
   3.121 +      |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), 
   3.122 +        [[quot_thm] MRSL @{thm Quotient_right_unique}])
   3.123 +      |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
   3.124 +        [[quot_thm] MRSL @{thm Quotient_right_total}])
   3.125        |> setup_lifting_infr quot_thm
   3.126    end
   3.127