merged
authorkuncar
Thu, 24 May 2012 15:03:06 +0200
changeset 47984 a1a5bf806d8b
parent 47983 a5e699834f2d (diff)
parent 47981 df35a8dd6368 (current diff)
child 47985 22846a7cf66e
merged
--- a/src/HOL/Library/Quotient_List.thy	Thu May 24 15:01:29 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Thu May 24 15:03:06 2012 +0200
@@ -37,7 +37,7 @@
     by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
 qed
 
-lemma list_reflp[reflp_preserve]:
+lemma list_reflp[reflexivity_rule]:
   assumes "reflp R"
   shows "reflp (list_all2 R)"
 proof (rule reflpI)
@@ -47,6 +47,17 @@
     by (induct xs) (simp_all add: *)
 qed
 
+lemma list_left_total[reflexivity_rule]:
+  assumes "left_total R"
+  shows "left_total (list_all2 R)"
+proof (rule left_totalI)
+  from assms have *: "\<And>xs. \<exists>ys. R xs ys" by (rule left_totalE)
+  fix xs
+  show "\<exists> ys. list_all2 R xs ys"
+    by (induct xs) (simp_all add: * list_all2_Cons1)
+qed
+
+
 lemma list_symp:
   assumes "symp R"
   shows "symp (list_all2 R)"
--- a/src/HOL/Library/Quotient_Option.thy	Thu May 24 15:01:29 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Thu May 24 15:03:06 2012 +0200
@@ -46,10 +46,16 @@
 lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
   by (metis option.exhaust) (* TODO: move to Option.thy *)
 
-lemma option_reflp[reflp_preserve]:
+lemma option_reflp[reflexivity_rule]:
   "reflp R \<Longrightarrow> reflp (option_rel R)"
   unfolding reflp_def split_option_all by simp
 
+lemma option_left_total[reflexivity_rule]:
+  "left_total R \<Longrightarrow> left_total (option_rel R)"
+  apply (intro left_totalI)
+  unfolding split_option_ex
+  by (case_tac x) (auto elim: left_totalE)
+
 lemma option_symp:
   "symp R \<Longrightarrow> symp (option_rel R)"
   unfolding symp_def split_option_all option_rel.simps by fast
--- a/src/HOL/Library/Quotient_Product.thy	Thu May 24 15:01:29 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy	Thu May 24 15:03:06 2012 +0200
@@ -27,12 +27,18 @@
   shows "prod_rel (op =) (op =) = (op =)"
   by (simp add: fun_eq_iff)
 
-lemma prod_reflp [reflp_preserve]:
+lemma prod_reflp [reflexivity_rule]:
   assumes "reflp R1"
   assumes "reflp R2"
   shows "reflp (prod_rel R1 R2)"
 using assms by (auto intro!: reflpI elim: reflpE)
 
+lemma prod_left_total [reflexivity_rule]:
+  assumes "left_total R1"
+  assumes "left_total R2"
+  shows "left_total (prod_rel R1 R2)"
+using assms by (auto intro!: left_totalI elim!: left_totalE)
+
 lemma prod_equivp [quot_equiv]:
   assumes "equivp R1"
   assumes "equivp R2"
--- a/src/HOL/Library/Quotient_Set.thy	Thu May 24 15:01:29 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Thu May 24 15:03:06 2012 +0200
@@ -34,9 +34,22 @@
 lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
   unfolding set_rel_def fun_eq_iff by auto
 
-lemma reflp_set_rel[reflp_preserve]: "reflp R \<Longrightarrow> reflp (set_rel R)"
+lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
   unfolding reflp_def set_rel_def by fast
 
+lemma left_total_set_rel[reflexivity_rule]:
+  assumes lt_R: "left_total R"
+  shows "left_total (set_rel R)"
+proof -
+  {
+    fix A
+    let ?B = "{y. \<exists>x \<in> A. R x y}"
+    have "(\<forall>x\<in>A. \<exists>y\<in>?B. R x y) \<and> (\<forall>y\<in>?B. \<exists>x\<in>A. R x y)" using lt_R by(elim left_totalE) blast
+  }
+  then have "\<And>A. \<exists>B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y)" by blast
+  then show ?thesis by (auto simp: set_rel_def intro: left_totalI)
+qed
+
 lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
   unfolding symp_def set_rel_def by fast
 
--- a/src/HOL/Library/Quotient_Sum.thy	Thu May 24 15:01:29 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Thu May 24 15:03:06 2012 +0200
@@ -46,10 +46,16 @@
 lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
   by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
 
-lemma sum_reflp[reflp_preserve]:
+lemma sum_reflp[reflexivity_rule]:
   "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
   unfolding reflp_def split_sum_all sum_rel.simps by fast
 
+lemma sum_left_total[reflexivity_rule]:
+  "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
+  apply (intro left_totalI)
+  unfolding split_sum_ex 
+  by (case_tac x) (auto elim: left_totalE)
+
 lemma sum_symp:
   "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
   unfolding symp_def split_sum_all sum_rel.simps by fast
--- a/src/HOL/Lifting.thy	Thu May 24 15:01:29 2012 +0200
+++ b/src/HOL/Lifting.thy	Thu May 24 15:03:06 2012 +0200
@@ -121,9 +121,6 @@
 lemma identity_quotient: "Quotient (op =) id id (op =)"
 unfolding Quotient_def by simp 
 
-lemma reflp_equality: "reflp (op =)"
-by (auto intro: reflpI)
-
 text {* TODO: Use one of these alternatives as the real definition. *}
 
 lemma Quotient_alt_def:
@@ -380,6 +377,45 @@
   shows "T c c'"
   using assms by (auto dest: Quotient_cr_rel)
 
+text {* Proving reflexivity *}
+
+definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
+
+lemma left_totalI:
+  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
+unfolding left_total_def by blast
+
+lemma left_totalE:
+  assumes "left_total R"
+  obtains "(\<And>x. \<exists>y. R x y)"
+using assms unfolding left_total_def by blast
+
+lemma Quotient_to_left_total:
+  assumes q: "Quotient R Abs Rep T"
+  and r_R: "reflp R"
+  shows "left_total T"
+using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
+
+lemma reflp_Quotient_composition:
+  assumes lt_R1: "left_total R1"
+  and r_R2: "reflp R2"
+  shows "reflp (R1 OO R2 OO R1\<inverse>\<inverse>)"
+using assms
+proof -
+  {
+    fix x
+    from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast
+    moreover then have "R1\<inverse>\<inverse> y x" by simp
+    moreover have "R2 y y" using r_R2 by (auto elim: reflpE)
+    ultimately have "(R1 OO R2 OO R1\<inverse>\<inverse>) x x" by auto
+  }
+  then show ?thesis by (auto intro: reflpI)
+qed
+
+lemma reflp_equality: "reflp (op =)"
+by (auto intro: reflpI)
+
 subsection {* ML setup *}
 
 use "Tools/Lifting/lifting_util.ML"
@@ -388,7 +424,7 @@
 setup Lifting_Info.setup
 
 declare fun_quotient[quot_map]
-declare reflp_equality[reflp_preserve]
+lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
 
 use "Tools/Lifting/lifting_term.ML"
 
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu May 24 15:01:29 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu May 24 15:03:06 2012 +0200
@@ -182,7 +182,7 @@
         
         val fun_rel_meta_eq = mk_meta_eq @{thm fun_rel_eq}
         val conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv fun_rel_meta_eq))) ctxt
-        val rules = Lifting_Info.get_reflp_preserve_rules ctxt
+        val rules = Lifting_Info.get_reflexivity_rules ctxt
       in
         EVERY' [CSUBGOAL intro_reflp_tac, 
                 CONVERSION conv,
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu May 24 15:01:29 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu May 24 15:03:06 2012 +0200
@@ -21,9 +21,9 @@
 
   val get_invariant_commute_rules: Proof.context -> thm list
   
-  val get_reflp_preserve_rules: Proof.context -> thm list
-  val add_reflp_preserve_rule_attribute: attribute
-  val add_reflp_preserve_rule_attrib: Attrib.src
+  val get_reflexivity_rules: Proof.context -> thm list
+  val add_reflexivity_rule_attribute: attribute
+  val add_reflexivity_rule_attrib: Attrib.src
 
   val setup: theory -> theory
 end;
@@ -183,13 +183,13 @@
 
 structure Reflp_Preserve = Named_Thms
 (
-  val name = @{binding reflp_preserve}
+  val name = @{binding reflexivity_rule}
   val description = "theorems that a relator preserves a reflexivity property"
 )
 
-val get_reflp_preserve_rules = Reflp_Preserve.get
-val add_reflp_preserve_rule_attribute = Reflp_Preserve.add
-val add_reflp_preserve_rule_attrib = Attrib.internal (K add_reflp_preserve_rule_attribute)
+val get_reflexivity_rules = Reflp_Preserve.get
+val add_reflexivity_rule_attribute = Reflp_Preserve.add
+val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute)
 
 (* theory setup *)
 
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu May 24 15:01:29 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu May 24 15:03:06 2012 +0200
@@ -103,8 +103,10 @@
     fun quot_info phi = Lifting_Info.transform_quotients phi quotients
     val lthy' = case maybe_reflp_thm of
       SOME reflp_thm => lthy
-        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
+        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
               [reflp_thm])
+        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
+              [[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
         |> define_code_constr gen_code quot_thm
       | NONE => lthy
         |> define_abs_type gen_code quot_thm
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Thu May 24 15:01:29 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Thu May 24 15:03:06 2012 +0200
@@ -9,11 +9,11 @@
   val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
     ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
 
-  val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
-    ((binding * binding) option * bool)) list -> Proof.context -> Proof.state
+  val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * 
+    ((binding * binding) option * bool) -> Proof.context -> Proof.state
 
-  val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
-    (binding * binding) option) list -> Proof.context -> Proof.state
+  val quotient_type_cmd: (((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
+    (binding * binding) option -> Proof.context -> Proof.state
 end;
 
 structure Quotient_Type: QUOTIENT_TYPE =
@@ -290,11 +290,11 @@
  relations are equivalence relations
 *)
 
-fun quotient_type quot_list lthy =
+fun quotient_type quot lthy =
   let
     (* sanity check *)
-    val _ = List.app sanity_check quot_list
-    val _ = List.app (map_check lthy) quot_list
+    val _ = sanity_check quot
+    val _ = map_check lthy quot
 
     fun mk_goal (rty, rel, partial) =
       let
@@ -305,14 +305,14 @@
         HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
       end
 
-    val goals = map (mk_goal o #2) quot_list
+    val goal = (mk_goal o #2) quot
 
-    fun after_qed [thms] = fold (snd oo add_quotient_type) (quot_list ~~ thms)
+    fun after_qed [[thm]] = (snd oo add_quotient_type) (quot, thm)
   in
-    Proof.theorem NONE after_qed [map (rpair []) goals] lthy
+    Proof.theorem NONE after_qed [[(goal, [])]] lthy
   end
 
-fun quotient_type_cmd specs lthy =
+fun quotient_type_cmd spec lthy =
   let
     fun parse_spec ((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
       let
@@ -327,7 +327,7 @@
         (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2)
       end
 
-    val (spec', _) = fold_map parse_spec specs lthy
+    val (spec', _) = parse_spec spec lthy
   in
     quotient_type spec' lthy
   end
@@ -338,12 +338,11 @@
 val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
 
 val quotspec_parser =
-  Parse.and_list1
-    ((opt_gen_code -- Parse.type_args -- Parse.binding) --
+     (opt_gen_code -- Parse.type_args -- Parse.binding) --
       (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
       Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
         (@{keyword "/"} |-- (partial -- Parse.term))  --
-        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
+        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}