left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Apr 10 17:48:14 2014 +0200
@@ -1597,7 +1597,6 @@
@{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
@{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
@{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
- @{attribute_def (HOL) "reflexivity_rule"} & : & @{text attribute} \\
@{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\
@{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\
@{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\
@@ -1742,13 +1741,6 @@
respectfulness theorem. For examples see @{file
"~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
- \item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
- that a relator respects left-totality and left_uniqueness. For examples
- see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
- in the same directory.
- The property is used in a reflexivity prover, which is used for discharging respectfulness
- theorems for type copies and also for discharging assumptions of abstraction function equations.
-
\item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator.
E.g., @{text "A \<le> B \<Longrightarrow> list_all2 A \<le> list_all2 B"}. For examples
see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
--- a/src/HOL/Library/FSet.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Library/FSet.thy Thu Apr 10 17:48:14 2014 +0200
@@ -834,7 +834,7 @@
apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
by (auto simp add: rel_set_def)
-lemma left_total_rel_fset[reflexivity_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
+lemma left_total_rel_fset[transfer_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
unfolding left_total_def
apply transfer
apply (subst(asm) choice_iff)
@@ -843,7 +843,7 @@
by (auto simp add: rel_set_def)
lemmas right_unique_rel_fset[transfer_rule] = right_unique_rel_set[Transfer.transferred]
-lemmas left_unique_rel_fset[reflexivity_rule] = left_unique_rel_set[Transfer.transferred]
+lemmas left_unique_rel_fset[transfer_rule] = left_unique_rel_set[Transfer.transferred]
thm right_unique_rel_fset left_unique_rel_fset
--- a/src/HOL/Lifting.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Lifting.thy Thu Apr 10 17:48:14 2014 +0200
@@ -24,82 +24,6 @@
"(id ---> id) = id"
by (simp add: fun_eq_iff)
-subsection {* Other predicates on relations *}
-
-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 bi_total_iff: "bi_total A = (right_total A \<and> left_total A)"
-unfolding left_total_def right_total_def bi_total_def by blast
-
-lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
-by(simp add: left_total_def right_total_def bi_total_def)
-
-definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
- where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
-
-lemma left_unique_transfer [transfer_rule]:
- assumes "right_total A"
- assumes "right_total B"
- assumes "bi_unique A"
- shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
-using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
-by metis
-
-lemma bi_unique_iff: "bi_unique A = (right_unique A \<and> left_unique A)"
-unfolding left_unique_def right_unique_def bi_unique_def by blast
-
-lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
-by(auto simp add: left_unique_def right_unique_def bi_unique_def)
-
-lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
-unfolding left_unique_def by blast
-
-lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
-unfolding left_unique_def by blast
-
-lemma left_total_fun:
- "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
- unfolding left_total_def rel_fun_def
- apply (rule allI, rename_tac f)
- apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
- apply clarify
- apply (subgoal_tac "(THE x. A x y) = x", simp)
- apply (rule someI_ex)
- apply (simp)
- apply (rule the_equality)
- apply assumption
- apply (simp add: left_unique_def)
- done
-
-lemma left_unique_fun:
- "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
- unfolding left_total_def left_unique_def rel_fun_def
- by (clarify, rule ext, fast)
-
-lemma left_total_eq: "left_total op=" unfolding left_total_def by blast
-
-lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast
-
-lemma [simp]:
- shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
- and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
-by(auto simp add: left_unique_def right_unique_def)
-
-lemma [simp]:
- shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
- and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
-by(simp_all add: left_total_def right_total_def)
-
subsection {* Quotient Predicate *}
definition
@@ -391,6 +315,9 @@
assumes 1: "Quotient R Abs Rep T" and 2: "reflp R"
begin
+lemma Quotient_left_total: "left_total T"
+ using 1 2 unfolding Quotient_alt_def left_total_def reflp_def by auto
+
lemma Quotient_bi_total: "bi_total T"
using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
@@ -464,12 +391,6 @@
shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
using assms unfolding left_unique_def by blast
-lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
-unfolding left_total_def OO_def by fast
-
-lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
-unfolding left_unique_def OO_def by blast
-
lemma invariant_le_eq:
"invariant P \<le> op=" unfolding invariant_def by blast
@@ -487,18 +408,6 @@
definition NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
"NEG A B \<equiv> B \<le> A"
-(*
- The following two rules are here because we don't have any proper
- left-unique ant left-total relations. Left-unique and left-total
- assumptions show up in distributivity rules for the function type.
-*)
-
-lemma bi_unique_left_unique[transfer_rule]: "bi_unique R \<Longrightarrow> left_unique R"
-unfolding bi_unique_def left_unique_def by blast
-
-lemma bi_total_left_total[transfer_rule]: "bi_total R \<Longrightarrow> left_total R"
-unfolding bi_total_def left_total_def by blast
-
lemma pos_OO_eq:
shows "POS (A OO op=) A"
unfolding POS_def OO_def by blast
@@ -635,10 +544,10 @@
using assms by blast
lemma pcr_Domainp_total:
- assumes "bi_total B"
+ assumes "left_total B"
assumes "Domainp A = P"
shows "Domainp (A OO B) = P"
-using assms unfolding bi_total_def
+using assms unfolding left_total_def
by fast
lemma Quotient_to_Domainp:
@@ -660,12 +569,6 @@
ML_file "Tools/Lifting/lifting_info.ML"
setup Lifting_Info.setup
-lemmas [reflexivity_rule] =
- order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq
- Quotient_composition_ge_eq
- left_total_eq left_unique_eq left_total_composition left_unique_composition
- left_total_fun left_unique_fun
-
(* setup for the function type *)
declare fun_quotient[quot_map]
declare fun_mono[relator_mono]
@@ -676,7 +579,7 @@
ML_file "Tools/Lifting/lifting_def.ML"
ML_file "Tools/Lifting/lifting_setup.ML"
-
+
hide_const (open) invariant POS NEG
end
--- a/src/HOL/Lifting_Option.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Lifting_Option.thy Thu Apr 10 17:48:14 2014 +0200
@@ -39,11 +39,11 @@
using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
by (auto iff: fun_eq_iff split: option.split)
-lemma left_total_rel_option[reflexivity_rule]:
+lemma left_total_rel_option[transfer_rule]:
"left_total R \<Longrightarrow> left_total (rel_option R)"
unfolding left_total_def split_option_all split_option_ex by simp
-lemma left_unique_rel_option [reflexivity_rule]:
+lemma left_unique_rel_option [transfer_rule]:
"left_unique R \<Longrightarrow> left_unique (rel_option R)"
unfolding left_unique_def split_option_all by simp
--- a/src/HOL/Lifting_Product.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Lifting_Product.thy Thu Apr 10 17:48:14 2014 +0200
@@ -30,13 +30,13 @@
shows "Domainp (rel_prod T1 T2) = (pred_prod P1 P2)"
using assms unfolding rel_prod_def pred_prod_def by blast
-lemma left_total_rel_prod [reflexivity_rule]:
+lemma left_total_rel_prod [transfer_rule]:
assumes "left_total R1"
assumes "left_total R2"
shows "left_total (rel_prod R1 R2)"
using assms unfolding left_total_def rel_prod_def by auto
-lemma left_unique_rel_prod [reflexivity_rule]:
+lemma left_unique_rel_prod [transfer_rule]:
assumes "left_unique R1" and "left_unique R2"
shows "left_unique (rel_prod R1 R2)"
using assms unfolding left_unique_def rel_prod_def by auto
--- a/src/HOL/Lifting_Set.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Lifting_Set.thy Thu Apr 10 17:48:14 2014 +0200
@@ -54,14 +54,14 @@
apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
done
-lemma left_total_rel_set[reflexivity_rule]:
+lemma left_total_rel_set[transfer_rule]:
"left_total A \<Longrightarrow> left_total (rel_set A)"
unfolding left_total_def rel_set_def
apply safe
apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
done
-lemma left_unique_rel_set[reflexivity_rule]:
+lemma left_unique_rel_set[transfer_rule]:
"left_unique A \<Longrightarrow> left_unique (rel_set A)"
unfolding left_unique_def rel_set_def
by fast
--- a/src/HOL/Lifting_Sum.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Lifting_Sum.thy Thu Apr 10 17:48:14 2014 +0200
@@ -26,11 +26,11 @@
using assms
by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
-lemma left_total_rel_sum[reflexivity_rule]:
+lemma left_total_rel_sum[transfer_rule]:
"left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (rel_sum R1 R2)"
using assms unfolding left_total_def split_sum_all split_sum_ex by simp
-lemma left_unique_rel_sum [reflexivity_rule]:
+lemma left_unique_rel_sum [transfer_rule]:
"left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (rel_sum R1 R2)"
using assms unfolding left_unique_def split_sum_all by simp
--- a/src/HOL/List.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/List.thy Thu Apr 10 17:48:14 2014 +0200
@@ -6619,14 +6619,14 @@
by (auto iff: fun_eq_iff)
qed
-lemma left_total_list_all2[reflexivity_rule]:
+lemma left_total_list_all2[transfer_rule]:
"left_total R \<Longrightarrow> left_total (list_all2 R)"
unfolding left_total_def
apply safe
apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
done
-lemma left_unique_list_all2 [reflexivity_rule]:
+lemma left_unique_list_all2 [transfer_rule]:
"left_unique R \<Longrightarrow> left_unique (list_all2 R)"
unfolding left_unique_def
apply (subst (2) all_comm, subst (1) all_comm)
--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 10 17:48:14 2014 +0200
@@ -29,12 +29,18 @@
fun mono_eq_prover ctxt prop =
let
- val rules = Lifting_Info.get_reflexivity_rules ctxt
+ val refl_rules = Lifting_Info.get_reflexivity_rules ctxt
+ val transfer_rules = Transfer.get_transfer_raw ctxt
+
+ fun main_tac (t, i) =
+ case HOLogic.dest_Trueprop t of
+ Const (@{const_name "less_eq"}, _) $ _ $ _ => REPEAT_ALL_NEW (resolve_tac refl_rules) i
+ | _ => REPEAT_ALL_NEW (resolve_tac transfer_rules) i
in
- SOME (Goal.prove ctxt [] [] prop (K (REPEAT_ALL_NEW (resolve_tac rules) 1)))
+ SOME (Goal.prove ctxt [] [] prop (K (SUBGOAL main_tac 1)))
handle ERROR _ => NONE
end
-
+
fun try_prove_reflexivity ctxt prop =
let
val thy = Proof_Context.theory_of ctxt
@@ -511,7 +517,7 @@
@{thm rel_fun_eq_rel[THEN eq_reflection]},
@{thm rel_fun_def[THEN eq_reflection]}]
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
- val invariant_assms_tac_rules = @{thm left_unique_composition} ::
+ val invariant_assms_tac_rules = @{thm left_unique_OO} ::
invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
val invariant_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac invariant_assms_tac_rules)
THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
--- a/src/HOL/Tools/Lifting/lifting_info.ML Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Thu Apr 10 17:48:14 2014 +0200
@@ -279,18 +279,6 @@
fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
-val relfexivity_rule_setup =
- let
- val name = @{binding reflexivity_rule}
- fun del_thm thm = Data.map (map_reflexivity_rules (Item_Net.remove thm))
- val del = Thm.declaration_attribute del_thm
- val text = "rules that are used to prove that a relation is reflexive"
- val content = Item_Net.content o get_reflexivity_rules'
- in
- Attrib.setup name (Attrib.add_del add_reflexivity_rule_attribute del) text
- #> Global_Theory.add_thms_dynamic (name, content)
- end
-
(* info about relator distributivity theorems *)
fun map_relator_distr_data' f1 f2 f3 f4
@@ -518,13 +506,18 @@
quot_map_attribute_setup
#> quot_del_attribute_setup
#> Invariant_Commute.setup
- #> relfexivity_rule_setup
#> relator_distr_attribute_setup
(* setup fixed invariant rules *)
val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context})
- [@{thm composed_equiv_rel_invariant}, @{thm composed_equiv_rel_eq_invariant}])
+ @{thms composed_equiv_rel_invariant composed_equiv_rel_eq_invariant})
+
+(* setup fixed reflexivity rules *)
+
+val _ = Context.>> (fold add_reflexivity_rule
+ @{thms order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq
+ bi_unique_OO bi_total_OO right_unique_OO right_total_OO left_unique_OO left_total_OO})
(* outer syntax commands *)
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Apr 10 17:48:14 2014 +0200
@@ -253,8 +253,6 @@
SOME reflp_thm => lthy
|> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
[reflp_thm RS @{thm reflp_ge_eq}])
- |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
- [[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
@@ -298,7 +296,8 @@
end
local
- val OO_rules = [@{thm bi_total_OO}, @{thm bi_unique_OO}, @{thm right_total_OO}, @{thm right_unique_OO}]
+ val OO_rules = @{thms left_total_OO left_unique_OO right_total_OO right_unique_OO bi_total_OO
+ bi_unique_OO}
in
fun parametrize_class_constraint ctxt pcr_def constraint =
let
@@ -325,7 +324,8 @@
val check_assms =
let
- val right_names = ["bi_total", "bi_unique", "right_total", "right_unique"]
+ val right_names = ["right_total", "right_unique", "left_total", "left_unique", "bi_total",
+ "bi_unique"]
fun is_right_name name = member op= right_names (Long_Name.base_name name)
@@ -451,10 +451,10 @@
thms
end
- fun parametrize_total_domain bi_total pcrel_def ctxt =
+ fun parametrize_total_domain left_total pcrel_def ctxt =
let
val thm =
- (bi_total RS @{thm pcr_Domainp_total})
+ (left_total RS @{thm pcr_Domainp_total})
|> fold_Domainp_pcrel pcrel_def
|> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt)
in
@@ -521,7 +521,8 @@
let
val thms =
[("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
- ("bi_total", @{thm Quotient_bi_total} )]
+ ("left_total", @{thm Quotient_left_total} ),
+ ("bi_total", @{thm Quotient_bi_total})]
in
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
[[quot_thm, reflp_thm] MRSL thm])) thms lthy
@@ -559,14 +560,17 @@
case opt_reflp_thm of
SOME reflp_thm =>
let
+ val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total})
val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
- val domain_thms = parametrize_total_domain bi_total pcrel_def lthy
+ val domain_thms = parametrize_total_domain left_total pcrel_def lthy
val id_abs_transfer = generate_parametric_id lthy rty
(Lifting_Term.parametrize_transfer_rule lthy
([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
+ val left_total = parametrize_class_constraint lthy pcrel_def left_total
val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
val thms =
[("id_abs_transfer",id_abs_transfer),
+ ("left_total", left_total ),
("bi_total", bi_total )]
in
lthy
@@ -652,7 +656,8 @@
let
val thms =
[("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
- ("bi_total", @{thm Quotient_bi_total} )]
+ ("left_total", @{thm Quotient_left_total} ),
+ ("bi_total", @{thm Quotient_bi_total} )]
in
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
[[quot_thm, reflp_thm] MRSL thm])) thms lthy
@@ -662,9 +667,10 @@
|> (snd oo Local_Theory.note) ((qualify "domain", [transfer_domain_attr]), [dom_thm])
val thms =
[("rep_transfer", @{thm typedef_rep_transfer}),
- ("bi_unique", @{thm typedef_bi_unique} ),
+ ("left_unique", @{thm typedef_left_unique} ),
("right_unique", @{thm typedef_right_unique}),
- ("right_total", @{thm typedef_right_total} )]
+ ("right_total", @{thm typedef_right_total} ),
+ ("bi_unique", @{thm typedef_bi_unique} )]
in
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
[[typedef_thm, T_def] MRSL thm])) thms lthy
@@ -679,14 +685,17 @@
case opt_reflp_thm of
SOME reflp_thm =>
let
+ val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total})
val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
- val domain_thms = parametrize_total_domain bi_total pcrel_def lthy
+ val domain_thms = parametrize_total_domain left_total pcrel_def lthy
+ val left_total = parametrize_class_constraint lthy pcrel_def left_total
val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
val id_abs_transfer = generate_parametric_id lthy rty
(Lifting_Term.parametrize_transfer_rule lthy
([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
val thms =
- [("bi_total", bi_total ),
+ [("left_total", left_total ),
+ ("bi_total", bi_total ),
("id_abs_transfer",id_abs_transfer)]
in
lthy
@@ -708,8 +717,9 @@
(Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL @{thm typedef_rep_transfer})))
::
(map_snd (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm))
- [("bi_unique", @{thm typedef_bi_unique} ),
- ("right_unique", @{thm typedef_right_unique}),
+ [("left_unique", @{thm typedef_left_unique} ),
+ ("right_unique", @{thm typedef_right_unique}),
+ ("bi_unique", @{thm typedef_bi_unique} ),
("right_total", @{thm typedef_right_total} )])
in
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
@@ -724,8 +734,6 @@
lthy
|> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []),
[quot_thm])
- |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_left_unique}])
|> setup_lifting_infr gen_code quot_thm opt_reflp_thm
|> setup_transfer_rules
end
--- a/src/HOL/Topological_Spaces.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy Thu Apr 10 17:48:14 2014 +0200
@@ -2486,7 +2486,7 @@
apply(auto simp add: rel_fun_def)
done
-lemma left_total_rel_filter [reflexivity_rule]:
+lemma left_total_rel_filter [transfer_rule]:
assumes [transfer_rule]: "bi_total A" "bi_unique A"
shows "left_total (rel_filter A)"
proof(rule left_totalI)
@@ -2511,7 +2511,7 @@
unfolding bi_total_conv_left_right using assms
by(simp add: left_total_rel_filter right_total_rel_filter)
-lemma left_unique_rel_filter [reflexivity_rule]:
+lemma left_unique_rel_filter [transfer_rule]:
assumes "left_unique A"
shows "left_unique (rel_filter A)"
proof(rule left_uniqueI)
--- a/src/HOL/Transfer.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Transfer.thy Thu Apr 10 17:48:14 2014 +0200
@@ -135,6 +135,12 @@
subsection {* Predicates on relations, i.e. ``class constraints'' *}
+definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
+
+definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)"
@@ -149,6 +155,21 @@
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
+unfolding left_unique_def by blast
+
+lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
+unfolding left_unique_def by blast
+
+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 bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
by(simp add: bi_unique_def)
@@ -192,12 +213,41 @@
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
unfolding bi_unique_def rel_fun_def by auto
+lemma [simp]:
+ shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
+ and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
+by(auto simp add: left_unique_def right_unique_def)
+
+lemma [simp]:
+ shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
+ and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
+by(simp_all add: left_total_def right_total_def)
+
lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
by(auto simp add: bi_unique_def)
lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
by(auto simp add: bi_total_def)
+lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)"
+unfolding left_total_def right_total_def bi_total_def by blast
+
+lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
+by(simp add: left_total_def right_total_def bi_total_def)
+
+lemma bi_unique_iff: "bi_unique A \<longleftrightarrow> right_unique A \<and> left_unique A"
+unfolding left_unique_def right_unique_def bi_unique_def by blast
+
+lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
+by(auto simp add: left_unique_def right_unique_def bi_unique_def)
+
+lemma bi_totalI: "left_total R \<Longrightarrow> right_total R \<Longrightarrow> bi_total R"
+unfolding bi_total_iff ..
+
+lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R"
+unfolding bi_unique_iff ..
+
+
text {* Properties are preserved by relation composition. *}
lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"
@@ -217,21 +267,52 @@
"\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)"
unfolding right_unique_def OO_def by fast
+lemma left_total_OO: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
+unfolding left_total_def OO_def by fast
+
+lemma left_unique_OO: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
+unfolding left_unique_def OO_def by blast
+
subsection {* Properties of relators *}
-lemma right_total_eq [transfer_rule]: "right_total (op =)"
+lemma left_total_eq[transfer_rule]: "left_total op="
+ unfolding left_total_def by blast
+
+lemma left_unique_eq[transfer_rule]: "left_unique op="
+ unfolding left_unique_def by blast
+
+lemma right_total_eq [transfer_rule]: "right_total op="
unfolding right_total_def by simp
-lemma right_unique_eq [transfer_rule]: "right_unique (op =)"
+lemma right_unique_eq [transfer_rule]: "right_unique op="
unfolding right_unique_def by simp
-lemma bi_total_eq [transfer_rule]: "bi_total (op =)"
+lemma bi_total_eq[transfer_rule]: "bi_total (op =)"
unfolding bi_total_def by simp
-lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)"
+lemma bi_unique_eq[transfer_rule]: "bi_unique (op =)"
unfolding bi_unique_def by simp
+lemma left_total_fun[transfer_rule]:
+ "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
+ unfolding left_total_def rel_fun_def
+ apply (rule allI, rename_tac f)
+ apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
+ apply clarify
+ apply (subgoal_tac "(THE x. A x y) = x", simp)
+ apply (rule someI_ex)
+ apply (simp)
+ apply (rule the_equality)
+ apply assumption
+ apply (simp add: left_unique_def)
+ done
+
+lemma left_unique_fun[transfer_rule]:
+ "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
+ unfolding left_total_def left_unique_def rel_fun_def
+ by (clarify, rule ext, fast)
+
lemma right_total_fun [transfer_rule]:
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
unfolding right_total_def rel_fun_def
@@ -251,35 +332,15 @@
unfolding right_total_def right_unique_def rel_fun_def
by (clarify, rule ext, fast)
-lemma bi_total_fun [transfer_rule]:
+lemma bi_total_fun[transfer_rule]:
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
- unfolding bi_total_def rel_fun_def
- apply safe
- apply (rename_tac f)
- apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
- apply clarify
- apply (subgoal_tac "(THE x. A x y) = x", simp)
- apply (rule someI_ex)
- apply (simp)
- apply (rule the_equality)
- apply assumption
- apply (simp add: bi_unique_def)
- apply (rename_tac g)
- apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
- apply clarify
- apply (subgoal_tac "(THE y. A x y) = y", simp)
- apply (rule someI_ex)
- apply (simp)
- apply (rule the_equality)
- apply assumption
- apply (simp add: bi_unique_def)
- done
+ unfolding bi_unique_iff bi_total_iff
+ by (blast intro: right_total_fun left_total_fun)
-lemma bi_unique_fun [transfer_rule]:
+lemma bi_unique_fun[transfer_rule]:
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
- unfolding bi_total_def bi_unique_def rel_fun_def fun_eq_iff
- by fast+
-
+ unfolding bi_unique_iff bi_total_iff
+ by (blast intro: right_unique_fun left_unique_fun)
subsection {* Transfer rules *}
@@ -318,6 +379,16 @@
"right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
unfolding right_unique_alt_def .
+text {* Transfer rules using equality. *}
+
+lemma left_unique_transfer [transfer_rule]:
+ assumes "right_total A"
+ assumes "right_total B"
+ assumes "bi_unique A"
+ shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
+using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
+by metis
+
lemma eq_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(A ===> A ===> op =) (op =) (op =)"