support non-open typedefs; define cr_rel in terms of a rep function for typedefs
authorkuncar
Wed Apr 04 17:51:12 2012 +0200 (2012-04-04)
changeset 4736187c0eaf04bad
parent 47360 d1ecc9cec531
child 47362 b1f099bdfbba
child 47363 c7fc95e722ff
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
src/HOL/Lifting.thy
src/HOL/Quotient.thy
src/HOL/Quotient_Examples/Lift_DList.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_setup.ML
     1.1 --- a/src/HOL/Lifting.thy	Wed Apr 04 16:29:17 2012 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 04 17:51:12 2012 +0200
     1.3 @@ -236,16 +236,17 @@
     1.4    shows "invariant P x x \<equiv> P x"
     1.5  using assms by (auto simp add: invariant_def)
     1.6  
     1.7 -lemma copy_type_to_Quotient:
     1.8 +lemma UNIV_typedef_to_Quotient:
     1.9    assumes "type_definition Rep Abs UNIV"
    1.10 -  and T_def: "T \<equiv> (\<lambda>x y. Abs x = y)"
    1.11 +  and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.12    shows "Quotient (op =) Abs Rep T"
    1.13  proof -
    1.14    interpret type_definition Rep Abs UNIV by fact
    1.15 -  from Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI)
    1.16 +  from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
    1.17 +    by (fastforce intro!: QuotientI fun_eq_iff)
    1.18  qed
    1.19  
    1.20 -lemma copy_type_to_equivp:
    1.21 +lemma UNIV_typedef_to_equivp:
    1.22    fixes Abs :: "'a \<Rightarrow> 'b"
    1.23    and Rep :: "'b \<Rightarrow> 'a"
    1.24    assumes "type_definition Rep Abs (UNIV::'a set)"
    1.25 @@ -253,6 +254,28 @@
    1.26  by (rule identity_equivp)
    1.27  
    1.28  lemma typedef_to_Quotient:
    1.29 +  assumes "type_definition Rep Abs S"
    1.30 +  and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.31 +  shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T"
    1.32 +proof -
    1.33 +  interpret type_definition Rep Abs S by fact
    1.34 +  from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
    1.35 +    by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
    1.36 +qed
    1.37 +
    1.38 +lemma typedef_to_part_equivp:
    1.39 +  assumes "type_definition Rep Abs S"
    1.40 +  shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))"
    1.41 +proof (intro part_equivpI)
    1.42 +  interpret type_definition Rep Abs S by fact
    1.43 +  show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
    1.44 +next
    1.45 +  show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
    1.46 +next
    1.47 +  show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
    1.48 +qed
    1.49 +
    1.50 +lemma open_typedef_to_Quotient:
    1.51    assumes "type_definition Rep Abs {x. P x}"
    1.52    and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.53    shows "Quotient (invariant P) Abs Rep T"
    1.54 @@ -262,16 +285,7 @@
    1.55      by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
    1.56  qed
    1.57  
    1.58 -lemma invariant_type_to_Quotient:
    1.59 -  assumes "type_definition Rep Abs {x. P x}"
    1.60 -  and T_def: "T \<equiv> (\<lambda>x y. (invariant P) x x \<and> Abs x = y)"
    1.61 -  shows "Quotient (invariant P) Abs Rep T"
    1.62 -proof -
    1.63 -  interpret type_definition Rep Abs "{x. P x}" by fact
    1.64 -  from Rep Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI simp: invariant_def)
    1.65 -qed
    1.66 -
    1.67 -lemma invariant_type_to_part_equivp:
    1.68 +lemma open_typedef_to_part_equivp:
    1.69    assumes "type_definition Rep Abs {x. P x}"
    1.70    shows "part_equivp (invariant P)"
    1.71  proof (intro part_equivpI)
     2.1 --- a/src/HOL/Quotient.thy	Wed Apr 04 16:29:17 2012 +0100
     2.2 +++ b/src/HOL/Quotient.thy	Wed Apr 04 17:51:12 2012 +0200
     2.3 @@ -772,24 +772,6 @@
     2.4  using assms
     2.5  by (rule OOO_quotient3) auto
     2.6  
     2.7 -subsection {* Invariant *}
     2.8 -
     2.9 -lemma copy_type_to_Quotient3:
    2.10 -  assumes "type_definition Rep Abs UNIV"
    2.11 -  shows "Quotient3 (op =) Abs Rep"
    2.12 -proof -
    2.13 -  interpret type_definition Rep Abs UNIV by fact
    2.14 -  from Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I)
    2.15 -qed
    2.16 -
    2.17 -lemma invariant_type_to_Quotient3:
    2.18 -  assumes "type_definition Rep Abs {x. P x}"
    2.19 -  shows "Quotient3 (Lifting.invariant P) Abs Rep"
    2.20 -proof -
    2.21 -  interpret type_definition Rep Abs "{x. P x}" by fact
    2.22 -  from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I simp: invariant_def)
    2.23 -qed
    2.24 -
    2.25  subsection {* ML setup *}
    2.26  
    2.27  text {* Auxiliary data for the quotient package *}
     3.1 --- a/src/HOL/Quotient_Examples/Lift_DList.thy	Wed Apr 04 16:29:17 2012 +0100
     3.2 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Wed Apr 04 17:51:12 2012 +0200
     3.3 @@ -54,28 +54,13 @@
     3.4  proof -
     3.5    {
     3.6      fix x y
     3.7 -    have "list_all2 cr_dlist x y \<Longrightarrow> 
     3.8 -      List.map Abs_dlist x = y \<and> list_all2 (Lifting.invariant distinct) x x"
     3.9 +    have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y"
    3.10        unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto
    3.11    }
    3.12    note cr = this
    3.13 -
    3.14    fix x :: "'a list list" and y :: "'a list list"
    3.15 -  assume a: "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
    3.16 -  from a have l_x: "list_all2 (Lifting.invariant distinct) x x" by (auto simp add: cr)
    3.17 -  from a have l_y: "list_all2 (Lifting.invariant distinct) y y" by (auto simp add: cr)
    3.18 -  from a have m: "(Lifting.invariant distinct) (List.map Abs_dlist x) (List.map Abs_dlist y)" 
    3.19 -    by (auto simp add: cr)
    3.20 -
    3.21 -  have "x = y" 
    3.22 -  proof -
    3.23 -    have m':"List.map Abs_dlist x = List.map Abs_dlist y" using m unfolding Lifting.invariant_def by simp
    3.24 -    have dist: "\<And>l. list_all2 (Lifting.invariant distinct) l l \<Longrightarrow> !x. x \<in> (set l) \<longrightarrow> distinct x"
    3.25 -      unfolding list_all2_def Lifting.invariant_def by (auto simp add: zip_same)
    3.26 -    from dist[OF l_x] dist[OF l_y] have "inj_on Abs_dlist (set x \<union> set y)" by (intro inj_onI) 
    3.27 -      (metis CollectI UnE Abs_dlist_inverse)
    3.28 -    with m' show ?thesis by (rule map_inj_on)
    3.29 -  qed
    3.30 +  assume "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
    3.31 +  then have "x = y" by (auto dest: cr simp add: Lifting.invariant_def)
    3.32    then show "?thesis x y" unfolding Lifting.invariant_def by auto
    3.33  qed
    3.34  
     4.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 16:29:17 2012 +0100
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 17:51:12 2012 +0200
     4.3 @@ -177,7 +177,7 @@
     4.4      val ((_, (_ , def_thm)), lthy') = 
     4.5        Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
     4.6  
     4.7 -    val transfer_thm = def_thm RS (rsp_thm RS (quotient_thm RS @{thm Quotient_to_transfer}))
     4.8 +    val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
     4.9  
    4.10      fun qualify defname suffix = Binding.name suffix
    4.11        |> Binding.qualify true defname
     5.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 04 16:29:17 2012 +0100
     5.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 04 17:51:12 2012 +0200
     5.3 @@ -22,26 +22,11 @@
     5.4  
     5.5  exception SETUP_LIFTING_INFR of string
     5.6  
     5.7 -fun define_cr_rel equiv_thm abs_fun lthy =
     5.8 +fun define_cr_rel rep_fun lthy =
     5.9    let
    5.10 -    fun force_type_of_rel rel forced_ty =
    5.11 -      let
    5.12 -        val thy = Proof_Context.theory_of lthy
    5.13 -        val rel_ty = (domain_type o fastype_of) rel
    5.14 -        val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty
    5.15 -      in
    5.16 -        Envir.subst_term_types ty_inst rel
    5.17 -      end
    5.18 -
    5.19 -    val (rty, qty) = (dest_funT o fastype_of) abs_fun
    5.20 -    val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
    5.21 -    val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
    5.22 -      Const (@{const_name equivp}, _) $ _ => abs_fun_graph
    5.23 -      | Const (@{const_name part_equivp}, _) $ rel => 
    5.24 -        HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
    5.25 -      | _ => raise SETUP_LIFTING_INFR "unsupported equivalence theorem"
    5.26 -      )
    5.27 -    val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
    5.28 +    val (qty, rty) = (dest_funT o fastype_of) rep_fun
    5.29 +    val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
    5.30 +    val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph));
    5.31      val qty_name = (fst o dest_Type) qty
    5.32      val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)  
    5.33      val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
    5.34 @@ -82,9 +67,9 @@
    5.35    let
    5.36      fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy =
    5.37        let
    5.38 -        val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
    5.39 +        val (_ $ rep_fun $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
    5.40          val equiv_thm = typedef_thm RS to_equiv_thm
    5.41 -        val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
    5.42 +        val (T_def, lthy') = define_cr_rel rep_fun lthy
    5.43          val quot_thm =  [typedef_thm, T_def] MRSL to_quot_thm
    5.44        in
    5.45          (quot_thm, equiv_thm, lthy')
    5.46 @@ -93,12 +78,13 @@
    5.47      val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
    5.48      val (quot_thm, equiv_thm, lthy') = (case typedef_set of
    5.49        Const ("Orderings.top_class.top", _) => 
    5.50 -        derive_quot_and_equiv_thm @{thm copy_type_to_Quotient} @{thm copy_type_to_equivp} 
    5.51 +        derive_quot_and_equiv_thm @{thm UNIV_typedef_to_Quotient} @{thm UNIV_typedef_to_equivp} 
    5.52            typedef_thm lthy
    5.53        | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
    5.54 -        derive_quot_and_equiv_thm @{thm invariant_type_to_Quotient} @{thm invariant_type_to_part_equivp} 
    5.55 +        derive_quot_and_equiv_thm @{thm open_typedef_to_Quotient} @{thm open_typedef_to_part_equivp} 
    5.56            typedef_thm lthy
    5.57 -      | _ => raise SETUP_LIFTING_INFR "unsupported typedef theorem")
    5.58 +      | _ => derive_quot_and_equiv_thm @{thm typedef_to_Quotient} @{thm typedef_to_part_equivp} 
    5.59 +          typedef_thm lthy)
    5.60    in
    5.61      setup_lifting_infr quot_thm equiv_thm lthy'
    5.62    end
    5.63 @@ -109,5 +95,4 @@
    5.64    Outer_Syntax.local_theory @{command_spec "setup_lifting"}
    5.65      "Setup lifting infrastructure" 
    5.66        (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))
    5.67 -
    5.68  end;