# HG changeset patch # User kuncar # Date 1397144894 -7200 # Node ID beb3b685166588d5836ebd548142892ae0eb3a10 # Parent 7e8a369eb10d36e250fa744a626c343289869a3c left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore) diff -r 7e8a369eb10d -r beb3b6851665 src/Doc/Isar_Ref/HOL_Specific.thy --- 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 \"}\\ @{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 \ B \ list_all2 A \ list_all2 B"}. For examples see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Library/FSet.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 \ left_total (rel_fset A)" +lemma left_total_rel_fset[transfer_rule]: "left_total A \ 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 diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Lifting.thy --- 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 \ 'b \ bool) \ bool" - where "left_total R \ (\x. \y. R x y)" - -lemma left_totalI: - "(\x. \y. R x y) \ left_total R" -unfolding left_total_def by blast - -lemma left_totalE: - assumes "left_total R" - obtains "(\x. \y. R x y)" -using assms unfolding left_total_def by blast - -lemma bi_total_iff: "bi_total A = (right_total A \ left_total A)" -unfolding left_total_def right_total_def bi_total_def by blast - -lemma bi_total_conv_left_right: "bi_total R \ left_total R \ right_total R" -by(simp add: left_total_def right_total_def bi_total_def) - -definition left_unique :: "('a \ 'b \ bool) \ bool" - where "left_unique R \ (\x y z. R x z \ R y z \ 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 \ left_unique A)" -unfolding left_unique_def right_unique_def bi_unique_def by blast - -lemma bi_unique_conv_left_right: "bi_unique R \ left_unique R \ right_unique R" -by(auto simp add: left_unique_def right_unique_def bi_unique_def) - -lemma left_uniqueI: "(\x y z. \ A x z; A y z \ \ x = y) \ left_unique A" -unfolding left_unique_def by blast - -lemma left_uniqueD: "\ left_unique A; A x z; A y z \ \ x = y" -unfolding left_unique_def by blast - -lemma left_total_fun: - "\left_unique A; left_total B\ \ left_total (A ===> B)" - unfolding left_total_def rel_fun_def - apply (rule allI, rename_tac f) - apply (rule_tac x="\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: - "\left_total A; left_unique B\ \ 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\\ \ right_unique A" - and right_unique_conversep: "right_unique A\\ \ left_unique A" -by(auto simp add: left_unique_def right_unique_def) - -lemma [simp]: - shows left_total_conversep: "left_total A\\ \ right_total A" - and right_total_conversep: "right_total A\\ \ 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\\) \ op=" using assms unfolding left_unique_def by blast -lemma left_total_composition: "left_total R \ left_total S \ left_total (R OO S)" -unfolding left_total_def OO_def by fast - -lemma left_unique_composition: "left_unique R \ left_unique S \ left_unique (R OO S)" -unfolding left_unique_def OO_def by blast - lemma invariant_le_eq: "invariant P \ op=" unfolding invariant_def by blast @@ -487,18 +408,6 @@ definition NEG :: "('a \ 'b \ bool) \ ('a \ 'b \ bool) \ bool" where "NEG A B \ B \ 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 \ left_unique R" -unfolding bi_unique_def left_unique_def by blast - -lemma bi_total_left_total[transfer_rule]: "bi_total R \ 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 diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Lifting_Option.thy --- 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 \ 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 \ left_unique (rel_option R)" unfolding left_unique_def split_option_all by simp diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Lifting_Product.thy --- 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 diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Lifting_Set.thy --- 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. \x\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 \ left_total (rel_set A)" unfolding left_total_def rel_set_def apply safe apply (rename_tac X, rule_tac x="{y. \x\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 \ left_unique (rel_set A)" unfolding left_unique_def rel_set_def by fast diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Lifting_Sum.thy --- 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 \ left_total R2 \ 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 \ left_unique R2 \ left_unique (rel_sum R1 R2)" using assms unfolding left_unique_def split_sum_all by simp diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/List.thy --- 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 \ 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 \ left_unique (list_all2 R)" unfolding left_unique_def apply (subst (2) all_comm, subst (1) all_comm) diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Tools/Lifting/lifting_def.ML --- 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 diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Tools/Lifting/lifting_info.ML --- 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 *) diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Tools/Lifting/lifting_setup.ML --- 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 diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Topological_Spaces.thy --- 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) diff -r 7e8a369eb10d -r beb3b6851665 src/HOL/Transfer.thy --- 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 \ 'b \ bool) \ bool" + where "left_total R \ (\x. \y. R x y)" + +definition left_unique :: "('a \ 'b \ bool) \ bool" + where "left_unique R \ (\x y z. R x z \ R y z \ x = y)" + definition right_total :: "('a \ 'b \ bool) \ bool" where "right_total R \ (\y. \x. R x y)" @@ -149,6 +155,21 @@ (\x y z. R x y \ R x z \ y = z) \ (\x y z. R x z \ R y z \ x = y)" +lemma left_uniqueI: "(\x y z. \ A x z; A y z \ \ x = y) \ left_unique A" +unfolding left_unique_def by blast + +lemma left_uniqueD: "\ left_unique A; A x z; A y z \ \ x = y" +unfolding left_unique_def by blast + +lemma left_totalI: + "(\x. \y. R x y) \ left_total R" +unfolding left_total_def by blast + +lemma left_totalE: + assumes "left_total R" + obtains "(\x. \y. R x y)" +using assms unfolding left_total_def by blast + lemma bi_uniqueDr: "\ bi_unique A; A x y; A x z \ \ y = z" by(simp add: bi_unique_def) @@ -192,12 +213,41 @@ "bi_unique R \ (R ===> R ===> op =) (op =) (op =)" unfolding bi_unique_def rel_fun_def by auto +lemma [simp]: + shows left_unique_conversep: "left_unique A\\ \ right_unique A" + and right_unique_conversep: "right_unique A\\ \ left_unique A" +by(auto simp add: left_unique_def right_unique_def) + +lemma [simp]: + shows left_total_conversep: "left_total A\\ \ right_total A" + and right_total_conversep: "right_total A\\ \ left_total A" +by(simp_all add: left_total_def right_total_def) + lemma bi_unique_conversep [simp]: "bi_unique R\\ = bi_unique R" by(auto simp add: bi_unique_def) lemma bi_total_conversep [simp]: "bi_total R\\ = bi_total R" by(auto simp add: bi_total_def) +lemma bi_total_iff: "bi_total A = (right_total A \ left_total A)" +unfolding left_total_def right_total_def bi_total_def by blast + +lemma bi_total_conv_left_right: "bi_total R \ left_total R \ right_total R" +by(simp add: left_total_def right_total_def bi_total_def) + +lemma bi_unique_iff: "bi_unique A \ right_unique A \ left_unique A" +unfolding left_unique_def right_unique_def bi_unique_def by blast + +lemma bi_unique_conv_left_right: "bi_unique R \ left_unique R \ right_unique R" +by(auto simp add: left_unique_def right_unique_def bi_unique_def) + +lemma bi_totalI: "left_total R \ right_total R \ bi_total R" +unfolding bi_total_iff .. + +lemma bi_uniqueI: "left_unique R \ right_unique R \ bi_unique R" +unfolding bi_unique_iff .. + + text {* Properties are preserved by relation composition. *} lemma OO_def: "R OO S = (\x z. \y. R x y \ S y z)" @@ -217,21 +267,52 @@ "\right_unique A; right_unique B\ \ right_unique (A OO B)" unfolding right_unique_def OO_def by fast +lemma left_total_OO: "left_total R \ left_total S \ left_total (R OO S)" +unfolding left_total_def OO_def by fast + +lemma left_unique_OO: "left_unique R \ left_unique S \ 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]: + "\left_unique A; left_total B\ \ left_total (A ===> B)" + unfolding left_total_def rel_fun_def + apply (rule allI, rename_tac f) + apply (rule_tac x="\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]: + "\left_total A; left_unique B\ \ 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]: "\right_unique A; right_total B\ \ 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]: "\bi_unique A; bi_total B\ \ bi_total (A ===> B)" - unfolding bi_total_def rel_fun_def - apply safe - apply (rename_tac f) - apply (rule_tac x="\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="\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]: "\bi_total A; bi_unique B\ \ 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 \ (A ===> A ===> op \) (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 =)"