# HG changeset patch
# User kuncar
# Date 1333554672 -7200
# Node ID 87c0eaf04bad02a12c4fdcd84de9448fcbef4606
# Parent  d1ecc9cec5312fd6ed508d4d98ecc1fa1beeeb24
support non-open typedefs; define cr_rel in terms of a rep function for typedefs

diff -r d1ecc9cec531 -r 87c0eaf04bad src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Apr 04 16:29:17 2012 +0100
+++ b/src/HOL/Lifting.thy	Wed Apr 04 17:51:12 2012 +0200
@@ -236,16 +236,17 @@
   shows "invariant P x x \<equiv> P x"
 using assms by (auto simp add: invariant_def)
 
-lemma copy_type_to_Quotient:
+lemma UNIV_typedef_to_Quotient:
   assumes "type_definition Rep Abs UNIV"
-  and T_def: "T \<equiv> (\<lambda>x y. Abs x = y)"
+  and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   shows "Quotient (op =) Abs Rep T"
 proof -
   interpret type_definition Rep Abs UNIV by fact
-  from Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI)
+  from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
+    by (fastforce intro!: QuotientI fun_eq_iff)
 qed
 
-lemma copy_type_to_equivp:
+lemma UNIV_typedef_to_equivp:
   fixes Abs :: "'a \<Rightarrow> 'b"
   and Rep :: "'b \<Rightarrow> 'a"
   assumes "type_definition Rep Abs (UNIV::'a set)"
@@ -253,6 +254,28 @@
 by (rule identity_equivp)
 
 lemma typedef_to_Quotient:
+  assumes "type_definition Rep Abs S"
+  and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
+  shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T"
+proof -
+  interpret type_definition Rep Abs S by fact
+  from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
+    by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
+qed
+
+lemma typedef_to_part_equivp:
+  assumes "type_definition Rep Abs S"
+  shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))"
+proof (intro part_equivpI)
+  interpret type_definition Rep Abs S by fact
+  show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
+next
+  show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
+next
+  show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
+qed
+
+lemma open_typedef_to_Quotient:
   assumes "type_definition Rep Abs {x. P x}"
   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   shows "Quotient (invariant P) Abs Rep T"
@@ -262,16 +285,7 @@
     by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
 qed
 
-lemma invariant_type_to_Quotient:
-  assumes "type_definition Rep Abs {x. P x}"
-  and T_def: "T \<equiv> (\<lambda>x y. (invariant P) x x \<and> Abs x = y)"
-  shows "Quotient (invariant P) Abs Rep T"
-proof -
-  interpret type_definition Rep Abs "{x. P x}" by fact
-  from Rep Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI simp: invariant_def)
-qed
-
-lemma invariant_type_to_part_equivp:
+lemma open_typedef_to_part_equivp:
   assumes "type_definition Rep Abs {x. P x}"
   shows "part_equivp (invariant P)"
 proof (intro part_equivpI)
diff -r d1ecc9cec531 -r 87c0eaf04bad src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Wed Apr 04 16:29:17 2012 +0100
+++ b/src/HOL/Quotient.thy	Wed Apr 04 17:51:12 2012 +0200
@@ -772,24 +772,6 @@
 using assms
 by (rule OOO_quotient3) auto
 
-subsection {* Invariant *}
-
-lemma copy_type_to_Quotient3:
-  assumes "type_definition Rep Abs UNIV"
-  shows "Quotient3 (op =) Abs Rep"
-proof -
-  interpret type_definition Rep Abs UNIV by fact
-  from Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I)
-qed
-
-lemma invariant_type_to_Quotient3:
-  assumes "type_definition Rep Abs {x. P x}"
-  shows "Quotient3 (Lifting.invariant P) Abs Rep"
-proof -
-  interpret type_definition Rep Abs "{x. P x}" by fact
-  from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I simp: invariant_def)
-qed
-
 subsection {* ML setup *}
 
 text {* Auxiliary data for the quotient package *}
diff -r d1ecc9cec531 -r 87c0eaf04bad src/HOL/Quotient_Examples/Lift_DList.thy
--- a/src/HOL/Quotient_Examples/Lift_DList.thy	Wed Apr 04 16:29:17 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Wed Apr 04 17:51:12 2012 +0200
@@ -54,28 +54,13 @@
 proof -
   {
     fix x y
-    have "list_all2 cr_dlist x y \<Longrightarrow> 
-      List.map Abs_dlist x = y \<and> list_all2 (Lifting.invariant distinct) x x"
+    have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y"
       unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto
   }
   note cr = this
-
   fix x :: "'a list list" and y :: "'a list list"
-  assume a: "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
-  from a have l_x: "list_all2 (Lifting.invariant distinct) x x" by (auto simp add: cr)
-  from a have l_y: "list_all2 (Lifting.invariant distinct) y y" by (auto simp add: cr)
-  from a have m: "(Lifting.invariant distinct) (List.map Abs_dlist x) (List.map Abs_dlist y)" 
-    by (auto simp add: cr)
-
-  have "x = y" 
-  proof -
-    have m':"List.map Abs_dlist x = List.map Abs_dlist y" using m unfolding Lifting.invariant_def by simp
-    have dist: "\<And>l. list_all2 (Lifting.invariant distinct) l l \<Longrightarrow> !x. x \<in> (set l) \<longrightarrow> distinct x"
-      unfolding list_all2_def Lifting.invariant_def by (auto simp add: zip_same)
-    from dist[OF l_x] dist[OF l_y] have "inj_on Abs_dlist (set x \<union> set y)" by (intro inj_onI) 
-      (metis CollectI UnE Abs_dlist_inverse)
-    with m' show ?thesis by (rule map_inj_on)
-  qed
+  assume "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
+  then have "x = y" by (auto dest: cr simp add: Lifting.invariant_def)
   then show "?thesis x y" unfolding Lifting.invariant_def by auto
 qed
 
diff -r d1ecc9cec531 -r 87c0eaf04bad src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 16:29:17 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 17:51:12 2012 +0200
@@ -177,7 +177,7 @@
     val ((_, (_ , def_thm)), lthy') = 
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
-    val transfer_thm = def_thm RS (rsp_thm RS (quotient_thm RS @{thm Quotient_to_transfer}))
+    val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
 
     fun qualify defname suffix = Binding.name suffix
       |> Binding.qualify true defname
diff -r d1ecc9cec531 -r 87c0eaf04bad src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 04 16:29:17 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 04 17:51:12 2012 +0200
@@ -22,26 +22,11 @@
 
 exception SETUP_LIFTING_INFR of string
 
-fun define_cr_rel equiv_thm abs_fun lthy =
+fun define_cr_rel rep_fun lthy =
   let
-    fun force_type_of_rel rel forced_ty =
-      let
-        val thy = Proof_Context.theory_of lthy
-        val rel_ty = (domain_type o fastype_of) rel
-        val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty
-      in
-        Envir.subst_term_types ty_inst rel
-      end
-
-    val (rty, qty) = (dest_funT o fastype_of) abs_fun
-    val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
-    val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
-      Const (@{const_name equivp}, _) $ _ => abs_fun_graph
-      | Const (@{const_name part_equivp}, _) $ rel => 
-        HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
-      | _ => raise SETUP_LIFTING_INFR "unsupported equivalence theorem"
-      )
-    val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
+    val (qty, rty) = (dest_funT o fastype_of) rep_fun
+    val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
+    val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph));
     val qty_name = (fst o dest_Type) qty
     val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)  
     val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
@@ -82,9 +67,9 @@
   let
     fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy =
       let
-        val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
+        val (_ $ rep_fun $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
         val equiv_thm = typedef_thm RS to_equiv_thm
-        val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
+        val (T_def, lthy') = define_cr_rel rep_fun lthy
         val quot_thm =  [typedef_thm, T_def] MRSL to_quot_thm
       in
         (quot_thm, equiv_thm, lthy')
@@ -93,12 +78,13 @@
     val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
     val (quot_thm, equiv_thm, lthy') = (case typedef_set of
       Const ("Orderings.top_class.top", _) => 
-        derive_quot_and_equiv_thm @{thm copy_type_to_Quotient} @{thm copy_type_to_equivp} 
+        derive_quot_and_equiv_thm @{thm UNIV_typedef_to_Quotient} @{thm UNIV_typedef_to_equivp} 
           typedef_thm lthy
       | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
-        derive_quot_and_equiv_thm @{thm invariant_type_to_Quotient} @{thm invariant_type_to_part_equivp} 
+        derive_quot_and_equiv_thm @{thm open_typedef_to_Quotient} @{thm open_typedef_to_part_equivp} 
           typedef_thm lthy
-      | _ => raise SETUP_LIFTING_INFR "unsupported typedef theorem")
+      | _ => derive_quot_and_equiv_thm @{thm typedef_to_Quotient} @{thm typedef_to_part_equivp} 
+          typedef_thm lthy)
   in
     setup_lifting_infr quot_thm equiv_thm lthy'
   end
@@ -109,5 +95,4 @@
   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
     "Setup lifting infrastructure" 
       (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))
-
 end;