left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
authorkuncar
Thu Apr 10 17:48:14 2014 +0200 (2014-04-10)
changeset 56518beb3b6851665
parent 56517 7e8a369eb10d
child 56519 c1048f5bbb45
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
src/Doc/Isar_Ref/HOL_Specific.thy
src/HOL/Library/FSet.thy
src/HOL/Lifting.thy
src/HOL/Lifting_Option.thy
src/HOL/Lifting_Product.thy
src/HOL/Lifting_Set.thy
src/HOL/Lifting_Sum.thy
src/HOL/List.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Topological_Spaces.thy
src/HOL/Transfer.thy
     1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Apr 10 17:48:13 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Apr 10 17:48:14 2014 +0200
     1.3 @@ -1597,7 +1597,6 @@
     1.4      @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
     1.5      @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
     1.6      @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
     1.7 -    @{attribute_def (HOL) "reflexivity_rule"} & : & @{text attribute} \\
     1.8      @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\
     1.9      @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\
    1.10      @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\
    1.11 @@ -1742,13 +1741,6 @@
    1.12      respectfulness theorem. For examples see @{file
    1.13      "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
    1.14  
    1.15 -  \item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
    1.16 -    that a relator respects left-totality and left_uniqueness. For examples 
    1.17 -    see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files 
    1.18 -    in the same directory.
    1.19 -    The property is used in a reflexivity prover, which is used for discharging respectfulness
    1.20 -    theorems for type copies and also for discharging assumptions of abstraction function equations.
    1.21 -
    1.22    \item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator.
    1.23      E.g., @{text "A \<le> B \<Longrightarrow> list_all2 A \<le> list_all2 B"}. For examples 
    1.24      see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} 
     2.1 --- a/src/HOL/Library/FSet.thy	Thu Apr 10 17:48:13 2014 +0200
     2.2 +++ b/src/HOL/Library/FSet.thy	Thu Apr 10 17:48:14 2014 +0200
     2.3 @@ -834,7 +834,7 @@
     2.4  apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
     2.5  by (auto simp add: rel_set_def)
     2.6  
     2.7 -lemma left_total_rel_fset[reflexivity_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
     2.8 +lemma left_total_rel_fset[transfer_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
     2.9  unfolding left_total_def 
    2.10  apply transfer
    2.11  apply (subst(asm) choice_iff)
    2.12 @@ -843,7 +843,7 @@
    2.13  by (auto simp add: rel_set_def)
    2.14  
    2.15  lemmas right_unique_rel_fset[transfer_rule] = right_unique_rel_set[Transfer.transferred]
    2.16 -lemmas left_unique_rel_fset[reflexivity_rule] = left_unique_rel_set[Transfer.transferred]
    2.17 +lemmas left_unique_rel_fset[transfer_rule] = left_unique_rel_set[Transfer.transferred]
    2.18  
    2.19  thm right_unique_rel_fset left_unique_rel_fset
    2.20  
     3.1 --- a/src/HOL/Lifting.thy	Thu Apr 10 17:48:13 2014 +0200
     3.2 +++ b/src/HOL/Lifting.thy	Thu Apr 10 17:48:14 2014 +0200
     3.3 @@ -24,82 +24,6 @@
     3.4    "(id ---> id) = id"
     3.5    by (simp add: fun_eq_iff)
     3.6  
     3.7 -subsection {* Other predicates on relations *}
     3.8 -
     3.9 -definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    3.10 -  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
    3.11 -
    3.12 -lemma left_totalI:
    3.13 -  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
    3.14 -unfolding left_total_def by blast
    3.15 -
    3.16 -lemma left_totalE:
    3.17 -  assumes "left_total R"
    3.18 -  obtains "(\<And>x. \<exists>y. R x y)"
    3.19 -using assms unfolding left_total_def by blast
    3.20 -
    3.21 -lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)"
    3.22 -unfolding left_total_def right_total_def bi_total_def by blast
    3.23 -
    3.24 -lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
    3.25 -by(simp add: left_total_def right_total_def bi_total_def)
    3.26 -
    3.27 -definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    3.28 -  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
    3.29 -
    3.30 -lemma left_unique_transfer [transfer_rule]:
    3.31 -  assumes "right_total A"
    3.32 -  assumes "right_total B"
    3.33 -  assumes "bi_unique A"
    3.34 -  shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
    3.35 -using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
    3.36 -by metis
    3.37 -
    3.38 -lemma bi_unique_iff: "bi_unique A = (right_unique A \<and> left_unique A)"
    3.39 -unfolding left_unique_def right_unique_def bi_unique_def by blast
    3.40 -
    3.41 -lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
    3.42 -by(auto simp add: left_unique_def right_unique_def bi_unique_def)
    3.43 -
    3.44 -lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
    3.45 -unfolding left_unique_def by blast
    3.46 -
    3.47 -lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
    3.48 -unfolding left_unique_def by blast
    3.49 -
    3.50 -lemma left_total_fun:
    3.51 -  "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
    3.52 -  unfolding left_total_def rel_fun_def
    3.53 -  apply (rule allI, rename_tac f)
    3.54 -  apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
    3.55 -  apply clarify
    3.56 -  apply (subgoal_tac "(THE x. A x y) = x", simp)
    3.57 -  apply (rule someI_ex)
    3.58 -  apply (simp)
    3.59 -  apply (rule the_equality)
    3.60 -  apply assumption
    3.61 -  apply (simp add: left_unique_def)
    3.62 -  done
    3.63 -
    3.64 -lemma left_unique_fun:
    3.65 -  "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
    3.66 -  unfolding left_total_def left_unique_def rel_fun_def
    3.67 -  by (clarify, rule ext, fast)
    3.68 -
    3.69 -lemma left_total_eq: "left_total op=" unfolding left_total_def by blast
    3.70 -
    3.71 -lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast
    3.72 -
    3.73 -lemma [simp]:
    3.74 -  shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
    3.75 -  and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
    3.76 -by(auto simp add: left_unique_def right_unique_def)
    3.77 -
    3.78 -lemma [simp]:
    3.79 -  shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
    3.80 -  and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
    3.81 -by(simp_all add: left_total_def right_total_def)
    3.82 -
    3.83  subsection {* Quotient Predicate *}
    3.84  
    3.85  definition
    3.86 @@ -391,6 +315,9 @@
    3.87    assumes 1: "Quotient R Abs Rep T" and 2: "reflp R"
    3.88  begin
    3.89  
    3.90 +lemma Quotient_left_total: "left_total T"
    3.91 +  using 1 2 unfolding Quotient_alt_def left_total_def reflp_def by auto
    3.92 +
    3.93  lemma Quotient_bi_total: "bi_total T"
    3.94    using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
    3.95  
    3.96 @@ -464,12 +391,6 @@
    3.97    shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
    3.98  using assms unfolding left_unique_def by blast
    3.99  
   3.100 -lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
   3.101 -unfolding left_total_def OO_def by fast
   3.102 -
   3.103 -lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
   3.104 -unfolding left_unique_def OO_def by blast
   3.105 -
   3.106  lemma invariant_le_eq:
   3.107    "invariant P \<le> op=" unfolding invariant_def by blast
   3.108  
   3.109 @@ -487,18 +408,6 @@
   3.110  definition  NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   3.111  "NEG A B \<equiv> B \<le> A"
   3.112  
   3.113 -(*
   3.114 -  The following two rules are here because we don't have any proper
   3.115 -  left-unique ant left-total relations. Left-unique and left-total
   3.116 -  assumptions show up in distributivity rules for the function type.
   3.117 -*)
   3.118 -
   3.119 -lemma bi_unique_left_unique[transfer_rule]: "bi_unique R \<Longrightarrow> left_unique R"
   3.120 -unfolding bi_unique_def left_unique_def by blast
   3.121 -
   3.122 -lemma bi_total_left_total[transfer_rule]: "bi_total R \<Longrightarrow> left_total R"
   3.123 -unfolding bi_total_def left_total_def by blast
   3.124 -
   3.125  lemma pos_OO_eq:
   3.126    shows "POS (A OO op=) A"
   3.127  unfolding POS_def OO_def by blast
   3.128 @@ -635,10 +544,10 @@
   3.129  using assms by blast
   3.130  
   3.131  lemma pcr_Domainp_total:
   3.132 -  assumes "bi_total B"
   3.133 +  assumes "left_total B"
   3.134    assumes "Domainp A = P"
   3.135    shows "Domainp (A OO B) = P"
   3.136 -using assms unfolding bi_total_def 
   3.137 +using assms unfolding left_total_def 
   3.138  by fast
   3.139  
   3.140  lemma Quotient_to_Domainp:
   3.141 @@ -660,12 +569,6 @@
   3.142  ML_file "Tools/Lifting/lifting_info.ML"
   3.143  setup Lifting_Info.setup
   3.144  
   3.145 -lemmas [reflexivity_rule] = 
   3.146 -  order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq
   3.147 -  Quotient_composition_ge_eq
   3.148 -  left_total_eq left_unique_eq left_total_composition left_unique_composition
   3.149 -  left_total_fun left_unique_fun
   3.150 -
   3.151  (* setup for the function type *)
   3.152  declare fun_quotient[quot_map]
   3.153  declare fun_mono[relator_mono]
   3.154 @@ -676,7 +579,7 @@
   3.155  ML_file "Tools/Lifting/lifting_def.ML"
   3.156  
   3.157  ML_file "Tools/Lifting/lifting_setup.ML"
   3.158 -
   3.159 +                           
   3.160  hide_const (open) invariant POS NEG
   3.161  
   3.162  end
     4.1 --- a/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:13 2014 +0200
     4.2 +++ b/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:14 2014 +0200
     4.3 @@ -39,11 +39,11 @@
     4.4  using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
     4.5  by (auto iff: fun_eq_iff split: option.split)
     4.6  
     4.7 -lemma left_total_rel_option[reflexivity_rule]:
     4.8 +lemma left_total_rel_option[transfer_rule]:
     4.9    "left_total R \<Longrightarrow> left_total (rel_option R)"
    4.10    unfolding left_total_def split_option_all split_option_ex by simp
    4.11  
    4.12 -lemma left_unique_rel_option [reflexivity_rule]:
    4.13 +lemma left_unique_rel_option [transfer_rule]:
    4.14    "left_unique R \<Longrightarrow> left_unique (rel_option R)"
    4.15    unfolding left_unique_def split_option_all by simp
    4.16  
     5.1 --- a/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:13 2014 +0200
     5.2 +++ b/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:14 2014 +0200
     5.3 @@ -30,13 +30,13 @@
     5.4    shows "Domainp (rel_prod T1 T2) = (pred_prod P1 P2)"
     5.5  using assms unfolding rel_prod_def pred_prod_def by blast
     5.6  
     5.7 -lemma left_total_rel_prod [reflexivity_rule]:
     5.8 +lemma left_total_rel_prod [transfer_rule]:
     5.9    assumes "left_total R1"
    5.10    assumes "left_total R2"
    5.11    shows "left_total (rel_prod R1 R2)"
    5.12    using assms unfolding left_total_def rel_prod_def by auto
    5.13  
    5.14 -lemma left_unique_rel_prod [reflexivity_rule]:
    5.15 +lemma left_unique_rel_prod [transfer_rule]:
    5.16    assumes "left_unique R1" and "left_unique R2"
    5.17    shows "left_unique (rel_prod R1 R2)"
    5.18    using assms unfolding left_unique_def rel_prod_def by auto
     6.1 --- a/src/HOL/Lifting_Set.thy	Thu Apr 10 17:48:13 2014 +0200
     6.2 +++ b/src/HOL/Lifting_Set.thy	Thu Apr 10 17:48:14 2014 +0200
     6.3 @@ -54,14 +54,14 @@
     6.4  apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
     6.5  done
     6.6  
     6.7 -lemma left_total_rel_set[reflexivity_rule]: 
     6.8 +lemma left_total_rel_set[transfer_rule]: 
     6.9    "left_total A \<Longrightarrow> left_total (rel_set A)"
    6.10    unfolding left_total_def rel_set_def
    6.11    apply safe
    6.12    apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
    6.13  done
    6.14  
    6.15 -lemma left_unique_rel_set[reflexivity_rule]: 
    6.16 +lemma left_unique_rel_set[transfer_rule]: 
    6.17    "left_unique A \<Longrightarrow> left_unique (rel_set A)"
    6.18    unfolding left_unique_def rel_set_def
    6.19    by fast
     7.1 --- a/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:13 2014 +0200
     7.2 +++ b/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:14 2014 +0200
     7.3 @@ -26,11 +26,11 @@
     7.4  using assms
     7.5  by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
     7.6  
     7.7 -lemma left_total_rel_sum[reflexivity_rule]:
     7.8 +lemma left_total_rel_sum[transfer_rule]:
     7.9    "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (rel_sum R1 R2)"
    7.10    using assms unfolding left_total_def split_sum_all split_sum_ex by simp
    7.11  
    7.12 -lemma left_unique_rel_sum [reflexivity_rule]:
    7.13 +lemma left_unique_rel_sum [transfer_rule]:
    7.14    "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (rel_sum R1 R2)"
    7.15    using assms unfolding left_unique_def split_sum_all by simp
    7.16  
     8.1 --- a/src/HOL/List.thy	Thu Apr 10 17:48:13 2014 +0200
     8.2 +++ b/src/HOL/List.thy	Thu Apr 10 17:48:14 2014 +0200
     8.3 @@ -6619,14 +6619,14 @@
     8.4    by (auto iff: fun_eq_iff)
     8.5  qed 
     8.6  
     8.7 -lemma left_total_list_all2[reflexivity_rule]:
     8.8 +lemma left_total_list_all2[transfer_rule]:
     8.9    "left_total R \<Longrightarrow> left_total (list_all2 R)"
    8.10    unfolding left_total_def
    8.11    apply safe
    8.12    apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
    8.13  done
    8.14  
    8.15 -lemma left_unique_list_all2 [reflexivity_rule]:
    8.16 +lemma left_unique_list_all2 [transfer_rule]:
    8.17    "left_unique R \<Longrightarrow> left_unique (list_all2 R)"
    8.18    unfolding left_unique_def
    8.19    apply (subst (2) all_comm, subst (1) all_comm)
     9.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 10 17:48:13 2014 +0200
     9.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 10 17:48:14 2014 +0200
     9.3 @@ -29,12 +29,18 @@
     9.4  
     9.5  fun mono_eq_prover ctxt prop =
     9.6    let
     9.7 -    val rules = Lifting_Info.get_reflexivity_rules ctxt
     9.8 +    val refl_rules = Lifting_Info.get_reflexivity_rules ctxt
     9.9 +    val transfer_rules = Transfer.get_transfer_raw ctxt
    9.10 +    
    9.11 +    fun main_tac (t, i) =
    9.12 +      case HOLogic.dest_Trueprop t of 
    9.13 +        Const (@{const_name "less_eq"}, _) $ _ $ _ => REPEAT_ALL_NEW (resolve_tac refl_rules) i
    9.14 +        |  _ => REPEAT_ALL_NEW (resolve_tac transfer_rules) i
    9.15    in
    9.16 -    SOME (Goal.prove ctxt [] [] prop (K (REPEAT_ALL_NEW (resolve_tac rules) 1)))
    9.17 +    SOME (Goal.prove ctxt [] [] prop (K (SUBGOAL main_tac 1)))
    9.18        handle ERROR _ => NONE
    9.19    end
    9.20 -   
    9.21 +
    9.22  fun try_prove_reflexivity ctxt prop =
    9.23    let
    9.24      val thy = Proof_Context.theory_of ctxt
    9.25 @@ -511,7 +517,7 @@
    9.26              @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
    9.27              @{thm rel_fun_def[THEN eq_reflection]}]
    9.28          fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
    9.29 -        val invariant_assms_tac_rules = @{thm left_unique_composition} :: 
    9.30 +        val invariant_assms_tac_rules = @{thm left_unique_OO} :: 
    9.31              invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
    9.32          val invariant_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac invariant_assms_tac_rules) 
    9.33            THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
    10.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Apr 10 17:48:13 2014 +0200
    10.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Apr 10 17:48:14 2014 +0200
    10.3 @@ -279,18 +279,6 @@
    10.4  fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
    10.5  val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
    10.6  
    10.7 -val relfexivity_rule_setup =
    10.8 -  let
    10.9 -    val name = @{binding reflexivity_rule}
   10.10 -    fun del_thm thm = Data.map (map_reflexivity_rules (Item_Net.remove thm))
   10.11 -    val del = Thm.declaration_attribute del_thm
   10.12 -    val text = "rules that are used to prove that a relation is reflexive"
   10.13 -    val content = Item_Net.content o get_reflexivity_rules'
   10.14 -  in
   10.15 -    Attrib.setup name (Attrib.add_del add_reflexivity_rule_attribute del) text
   10.16 -    #> Global_Theory.add_thms_dynamic (name, content)
   10.17 -  end
   10.18 -
   10.19  (* info about relator distributivity theorems *)
   10.20  
   10.21  fun map_relator_distr_data' f1 f2 f3 f4
   10.22 @@ -518,13 +506,18 @@
   10.23    quot_map_attribute_setup
   10.24    #> quot_del_attribute_setup
   10.25    #> Invariant_Commute.setup
   10.26 -  #> relfexivity_rule_setup
   10.27    #> relator_distr_attribute_setup
   10.28  
   10.29  (* setup fixed invariant rules *)
   10.30  
   10.31  val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context}) 
   10.32 -  [@{thm composed_equiv_rel_invariant}, @{thm composed_equiv_rel_eq_invariant}])
   10.33 +  @{thms composed_equiv_rel_invariant composed_equiv_rel_eq_invariant})
   10.34 +
   10.35 +(* setup fixed reflexivity rules *)
   10.36 +
   10.37 +val _ = Context.>> (fold add_reflexivity_rule 
   10.38 +  @{thms order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq
   10.39 +    bi_unique_OO bi_total_OO right_unique_OO right_total_OO left_unique_OO left_total_OO})
   10.40  
   10.41  (* outer syntax commands *)
   10.42  
    11.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 10 17:48:13 2014 +0200
    11.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 10 17:48:14 2014 +0200
    11.3 @@ -253,8 +253,6 @@
    11.4        SOME reflp_thm => lthy
    11.5          |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
    11.6                [reflp_thm RS @{thm reflp_ge_eq}])
    11.7 -        |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
    11.8 -              [[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
    11.9          |> define_code_constr gen_code quot_thm
   11.10        | NONE => lthy
   11.11          |> define_abs_type gen_code quot_thm
   11.12 @@ -298,7 +296,8 @@
   11.13  end
   11.14  
   11.15  local 
   11.16 -  val OO_rules = [@{thm bi_total_OO}, @{thm bi_unique_OO}, @{thm right_total_OO}, @{thm right_unique_OO}]
   11.17 +  val OO_rules = @{thms left_total_OO left_unique_OO right_total_OO right_unique_OO bi_total_OO
   11.18 +    bi_unique_OO}
   11.19  in
   11.20    fun parametrize_class_constraint ctxt pcr_def constraint =
   11.21      let
   11.22 @@ -325,7 +324,8 @@
   11.23        
   11.24        val check_assms =
   11.25          let 
   11.26 -          val right_names = ["bi_total", "bi_unique", "right_total", "right_unique"]
   11.27 +          val right_names = ["right_total", "right_unique", "left_total", "left_unique", "bi_total",
   11.28 +            "bi_unique"]
   11.29        
   11.30            fun is_right_name name = member op= right_names (Long_Name.base_name name)
   11.31        
   11.32 @@ -451,10 +451,10 @@
   11.33        thms
   11.34      end
   11.35  
   11.36 -  fun parametrize_total_domain bi_total pcrel_def ctxt =
   11.37 +  fun parametrize_total_domain left_total pcrel_def ctxt =
   11.38      let
   11.39        val thm =
   11.40 -        (bi_total RS @{thm pcr_Domainp_total})
   11.41 +        (left_total RS @{thm pcr_Domainp_total})
   11.42            |> fold_Domainp_pcrel pcrel_def 
   11.43            |> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt)
   11.44      in
   11.45 @@ -521,7 +521,8 @@
   11.46                let 
   11.47                  val thms =
   11.48                    [("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
   11.49 -                   ("bi_total",       @{thm Quotient_bi_total}       )]
   11.50 +                   ("left_total",     @{thm Quotient_left_total}     ),
   11.51 +                   ("bi_total",       @{thm Quotient_bi_total})]
   11.52                in
   11.53                  fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   11.54                      [[quot_thm, reflp_thm] MRSL thm])) thms lthy
   11.55 @@ -559,14 +560,17 @@
   11.56            case opt_reflp_thm of
   11.57              SOME reflp_thm =>
   11.58                let
   11.59 +                val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total})
   11.60                  val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
   11.61 -                val domain_thms = parametrize_total_domain bi_total pcrel_def lthy
   11.62 +                val domain_thms = parametrize_total_domain left_total pcrel_def lthy
   11.63                  val id_abs_transfer = generate_parametric_id lthy rty
   11.64                    (Lifting_Term.parametrize_transfer_rule lthy
   11.65                      ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
   11.66 +                val left_total = parametrize_class_constraint lthy pcrel_def left_total
   11.67                  val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
   11.68                  val thms = 
   11.69                    [("id_abs_transfer",id_abs_transfer),
   11.70 +                   ("left_total",     left_total     ),  
   11.71                     ("bi_total",       bi_total       )]
   11.72                in
   11.73                  lthy
   11.74 @@ -652,7 +656,8 @@
   11.75                let 
   11.76                  val thms =
   11.77                    [("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
   11.78 -                   ("bi_total",       @{thm Quotient_bi_total}       )]
   11.79 +                   ("left_total",     @{thm Quotient_left_total}     ),
   11.80 +                   ("bi_total",     @{thm Quotient_bi_total}         )]
   11.81                in
   11.82                  fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   11.83                      [[quot_thm, reflp_thm] MRSL thm])) thms lthy
   11.84 @@ -662,9 +667,10 @@
   11.85                |> (snd oo Local_Theory.note) ((qualify "domain", [transfer_domain_attr]), [dom_thm])
   11.86          val thms = 
   11.87            [("rep_transfer", @{thm typedef_rep_transfer}),
   11.88 -           ("bi_unique",    @{thm typedef_bi_unique}   ),
   11.89 +           ("left_unique",  @{thm typedef_left_unique} ),
   11.90             ("right_unique", @{thm typedef_right_unique}), 
   11.91 -           ("right_total",  @{thm typedef_right_total} )]
   11.92 +           ("right_total",  @{thm typedef_right_total} ),
   11.93 +           ("bi_unique",    @{thm typedef_bi_unique}   )]
   11.94        in
   11.95          fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   11.96            [[typedef_thm, T_def] MRSL thm])) thms lthy
   11.97 @@ -679,14 +685,17 @@
   11.98            case opt_reflp_thm of
   11.99              SOME reflp_thm =>
  11.100                let
  11.101 +                val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total})
  11.102                  val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
  11.103 -                val domain_thms = parametrize_total_domain bi_total pcrel_def lthy
  11.104 +                val domain_thms = parametrize_total_domain left_total pcrel_def lthy
  11.105 +                val left_total = parametrize_class_constraint lthy pcrel_def left_total
  11.106                  val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
  11.107                  val id_abs_transfer = generate_parametric_id lthy rty
  11.108                    (Lifting_Term.parametrize_transfer_rule lthy
  11.109                      ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
  11.110                  val thms = 
  11.111 -                  [("bi_total",       bi_total       ),
  11.112 +                  [("left_total",     left_total     ),
  11.113 +                   ("bi_total",       bi_total       ),
  11.114                     ("id_abs_transfer",id_abs_transfer)]              
  11.115                in
  11.116                  lthy
  11.117 @@ -708,8 +717,9 @@
  11.118              (Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL @{thm typedef_rep_transfer})))
  11.119            ::
  11.120            (map_snd (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm))
  11.121 -          [("bi_unique",    @{thm typedef_bi_unique} ),
  11.122 -           ("right_unique", @{thm typedef_right_unique}), 
  11.123 +          [("left_unique",  @{thm typedef_left_unique} ),
  11.124 +           ("right_unique", @{thm typedef_right_unique}),
  11.125 +           ("bi_unique",    @{thm typedef_bi_unique} ),
  11.126             ("right_total",  @{thm typedef_right_total} )])
  11.127        in
  11.128          fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
  11.129 @@ -724,8 +734,6 @@
  11.130      lthy
  11.131        |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), 
  11.132              [quot_thm])
  11.133 -      |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
  11.134 -           [[typedef_thm, T_def] MRSL @{thm typedef_left_unique}])
  11.135        |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
  11.136        |> setup_transfer_rules
  11.137    end
    12.1 --- a/src/HOL/Topological_Spaces.thy	Thu Apr 10 17:48:13 2014 +0200
    12.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Apr 10 17:48:14 2014 +0200
    12.3 @@ -2486,7 +2486,7 @@
    12.4  apply(auto simp add: rel_fun_def)
    12.5  done
    12.6  
    12.7 -lemma left_total_rel_filter [reflexivity_rule]:
    12.8 +lemma left_total_rel_filter [transfer_rule]:
    12.9    assumes [transfer_rule]: "bi_total A" "bi_unique A"
   12.10    shows "left_total (rel_filter A)"
   12.11  proof(rule left_totalI)
   12.12 @@ -2511,7 +2511,7 @@
   12.13  unfolding bi_total_conv_left_right using assms
   12.14  by(simp add: left_total_rel_filter right_total_rel_filter)
   12.15  
   12.16 -lemma left_unique_rel_filter [reflexivity_rule]:
   12.17 +lemma left_unique_rel_filter [transfer_rule]:
   12.18    assumes "left_unique A"
   12.19    shows "left_unique (rel_filter A)"
   12.20  proof(rule left_uniqueI)
    13.1 --- a/src/HOL/Transfer.thy	Thu Apr 10 17:48:13 2014 +0200
    13.2 +++ b/src/HOL/Transfer.thy	Thu Apr 10 17:48:14 2014 +0200
    13.3 @@ -135,6 +135,12 @@
    13.4  
    13.5  subsection {* Predicates on relations, i.e. ``class constraints'' *}
    13.6  
    13.7 +definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    13.8 +  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
    13.9 +
   13.10 +definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   13.11 +  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
   13.12 +
   13.13  definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   13.14    where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)"
   13.15  
   13.16 @@ -149,6 +155,21 @@
   13.17      (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
   13.18      (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
   13.19  
   13.20 +lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
   13.21 +unfolding left_unique_def by blast
   13.22 +
   13.23 +lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
   13.24 +unfolding left_unique_def by blast
   13.25 +
   13.26 +lemma left_totalI:
   13.27 +  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
   13.28 +unfolding left_total_def by blast
   13.29 +
   13.30 +lemma left_totalE:
   13.31 +  assumes "left_total R"
   13.32 +  obtains "(\<And>x. \<exists>y. R x y)"
   13.33 +using assms unfolding left_total_def by blast
   13.34 +
   13.35  lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
   13.36  by(simp add: bi_unique_def)
   13.37  
   13.38 @@ -192,12 +213,41 @@
   13.39    "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
   13.40    unfolding bi_unique_def rel_fun_def by auto
   13.41  
   13.42 +lemma [simp]:
   13.43 +  shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
   13.44 +  and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
   13.45 +by(auto simp add: left_unique_def right_unique_def)
   13.46 +
   13.47 +lemma [simp]:
   13.48 +  shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
   13.49 +  and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
   13.50 +by(simp_all add: left_total_def right_total_def)
   13.51 +
   13.52  lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
   13.53  by(auto simp add: bi_unique_def)
   13.54  
   13.55  lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
   13.56  by(auto simp add: bi_total_def)
   13.57  
   13.58 +lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)"
   13.59 +unfolding left_total_def right_total_def bi_total_def by blast
   13.60 +
   13.61 +lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
   13.62 +by(simp add: left_total_def right_total_def bi_total_def)
   13.63 +
   13.64 +lemma bi_unique_iff: "bi_unique A  \<longleftrightarrow> right_unique A \<and> left_unique A"
   13.65 +unfolding left_unique_def right_unique_def bi_unique_def by blast
   13.66 +
   13.67 +lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
   13.68 +by(auto simp add: left_unique_def right_unique_def bi_unique_def)
   13.69 +
   13.70 +lemma bi_totalI: "left_total R \<Longrightarrow> right_total R \<Longrightarrow> bi_total R"
   13.71 +unfolding bi_total_iff ..
   13.72 +
   13.73 +lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R"
   13.74 +unfolding bi_unique_iff ..
   13.75 +
   13.76 +
   13.77  text {* Properties are preserved by relation composition. *}
   13.78  
   13.79  lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"
   13.80 @@ -217,21 +267,52 @@
   13.81    "\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)"
   13.82    unfolding right_unique_def OO_def by fast
   13.83  
   13.84 +lemma left_total_OO: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
   13.85 +unfolding left_total_def OO_def by fast
   13.86 +
   13.87 +lemma left_unique_OO: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
   13.88 +unfolding left_unique_def OO_def by blast
   13.89 +
   13.90  
   13.91  subsection {* Properties of relators *}
   13.92  
   13.93 -lemma right_total_eq [transfer_rule]: "right_total (op =)"
   13.94 +lemma left_total_eq[transfer_rule]: "left_total op=" 
   13.95 +  unfolding left_total_def by blast
   13.96 +
   13.97 +lemma left_unique_eq[transfer_rule]: "left_unique op=" 
   13.98 +  unfolding left_unique_def by blast
   13.99 +
  13.100 +lemma right_total_eq [transfer_rule]: "right_total op="
  13.101    unfolding right_total_def by simp
  13.102  
  13.103 -lemma right_unique_eq [transfer_rule]: "right_unique (op =)"
  13.104 +lemma right_unique_eq [transfer_rule]: "right_unique op="
  13.105    unfolding right_unique_def by simp
  13.106  
  13.107 -lemma bi_total_eq [transfer_rule]: "bi_total (op =)"
  13.108 +lemma bi_total_eq[transfer_rule]: "bi_total (op =)"
  13.109    unfolding bi_total_def by simp
  13.110  
  13.111 -lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)"
  13.112 +lemma bi_unique_eq[transfer_rule]: "bi_unique (op =)"
  13.113    unfolding bi_unique_def by simp
  13.114  
  13.115 +lemma left_total_fun[transfer_rule]:
  13.116 +  "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
  13.117 +  unfolding left_total_def rel_fun_def
  13.118 +  apply (rule allI, rename_tac f)
  13.119 +  apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
  13.120 +  apply clarify
  13.121 +  apply (subgoal_tac "(THE x. A x y) = x", simp)
  13.122 +  apply (rule someI_ex)
  13.123 +  apply (simp)
  13.124 +  apply (rule the_equality)
  13.125 +  apply assumption
  13.126 +  apply (simp add: left_unique_def)
  13.127 +  done
  13.128 +
  13.129 +lemma left_unique_fun[transfer_rule]:
  13.130 +  "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
  13.131 +  unfolding left_total_def left_unique_def rel_fun_def
  13.132 +  by (clarify, rule ext, fast)
  13.133 +
  13.134  lemma right_total_fun [transfer_rule]:
  13.135    "\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
  13.136    unfolding right_total_def rel_fun_def
  13.137 @@ -251,35 +332,15 @@
  13.138    unfolding right_total_def right_unique_def rel_fun_def
  13.139    by (clarify, rule ext, fast)
  13.140  
  13.141 -lemma bi_total_fun [transfer_rule]:
  13.142 +lemma bi_total_fun[transfer_rule]:
  13.143    "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
  13.144 -  unfolding bi_total_def rel_fun_def
  13.145 -  apply safe
  13.146 -  apply (rename_tac f)
  13.147 -  apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
  13.148 -  apply clarify
  13.149 -  apply (subgoal_tac "(THE x. A x y) = x", simp)
  13.150 -  apply (rule someI_ex)
  13.151 -  apply (simp)
  13.152 -  apply (rule the_equality)
  13.153 -  apply assumption
  13.154 -  apply (simp add: bi_unique_def)
  13.155 -  apply (rename_tac g)
  13.156 -  apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
  13.157 -  apply clarify
  13.158 -  apply (subgoal_tac "(THE y. A x y) = y", simp)
  13.159 -  apply (rule someI_ex)
  13.160 -  apply (simp)
  13.161 -  apply (rule the_equality)
  13.162 -  apply assumption
  13.163 -  apply (simp add: bi_unique_def)
  13.164 -  done
  13.165 +  unfolding bi_unique_iff bi_total_iff
  13.166 +  by (blast intro: right_total_fun left_total_fun)
  13.167  
  13.168 -lemma bi_unique_fun [transfer_rule]:
  13.169 +lemma bi_unique_fun[transfer_rule]:
  13.170    "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
  13.171 -  unfolding bi_total_def bi_unique_def rel_fun_def fun_eq_iff
  13.172 -  by fast+
  13.173 -
  13.174 +  unfolding bi_unique_iff bi_total_iff
  13.175 +  by (blast intro: right_unique_fun left_unique_fun)
  13.176  
  13.177  subsection {* Transfer rules *}
  13.178  
  13.179 @@ -318,6 +379,16 @@
  13.180    "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
  13.181    unfolding right_unique_alt_def .
  13.182  
  13.183 +text {* Transfer rules using equality. *}
  13.184 +
  13.185 +lemma left_unique_transfer [transfer_rule]:
  13.186 +  assumes "right_total A"
  13.187 +  assumes "right_total B"
  13.188 +  assumes "bi_unique A"
  13.189 +  shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
  13.190 +using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
  13.191 +by metis
  13.192 +
  13.193  lemma eq_transfer [transfer_rule]:
  13.194    assumes "bi_unique A"
  13.195    shows "(A ===> A ===> op =) (op =) (op =)"