--- 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"}