1.1 --- a/src/HOL/Lifting.thy	Tue Feb 18 21:00:13 2014 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Tue Feb 18 23:03:47 2014 +0100
     1.3 @@ -439,39 +439,23 @@
     1.4  
     1.5  text {* Proving reflexivity *}
     1.6  
     1.7 -definition reflp' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where "reflp' R \<equiv> reflp R"
     1.8 -
     1.9  lemma Quotient_to_left_total:
    1.10    assumes q: "Quotient R Abs Rep T"
    1.11    and r_R: "reflp R"
    1.12    shows "left_total T"
    1.13  using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
    1.14  
    1.15 -lemma reflp_Quotient_composition:
    1.16 -  assumes "left_total R"
    1.17 -  assumes "reflp T"
    1.18 -  shows "reflp (R OO T OO R\<inverse>\<inverse>)"
    1.19 -using assms unfolding reflp_def left_total_def by fast
    1.20 +lemma Quotient_composition_ge_eq:
    1.21 +  assumes "left_total T"
    1.22 +  assumes "R \<ge> op="
    1.23 +  shows "(T OO R OO T\<inverse>\<inverse>) \<ge> op="
    1.24 +using assms unfolding left_total_def by fast
    1.25  
    1.26 -lemma reflp_fun1:
    1.27 -  assumes "is_equality R"
    1.28 -  assumes "reflp' S"
    1.29 -  shows "reflp (R ===> S)"
    1.30 -using assms unfolding is_equality_def reflp'_def reflp_def fun_rel_def by blast
    1.31 -
    1.32 -lemma reflp_fun2:
    1.33 -  assumes "is_equality R"
    1.34 -  assumes "is_equality S"
    1.35 -  shows "reflp (R ===> S)"
    1.36 -using assms unfolding is_equality_def reflp_def fun_rel_def by blast
    1.37 -
    1.38 -lemma is_equality_Quotient_composition:
    1.39 -  assumes "is_equality T"
    1.40 -  assumes "left_total R"
    1.41 -  assumes "left_unique R"
    1.42 -  shows "is_equality (R OO T OO R\<inverse>\<inverse>)"
    1.43 -using assms unfolding is_equality_def left_total_def left_unique_def OO_def conversep_iff
    1.44 -by fastforce
    1.45 +lemma Quotient_composition_le_eq:
    1.46 +  assumes "left_unique T"
    1.47 +  assumes "R \<le> op="
    1.48 +  shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
    1.49 +using assms unfolding left_unique_def by fast
    1.50  
    1.51  lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
    1.52  unfolding left_total_def OO_def by fast
    1.53 @@ -479,8 +463,14 @@
    1.54  lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
    1.55  unfolding left_unique_def OO_def by fast
    1.56  
    1.57 -lemma reflp_equality: "reflp (op =)"
    1.58 -by (auto intro: reflpI)
    1.59 +lemma invariant_le_eq:
    1.60 +  "invariant P \<le> op=" unfolding invariant_def by blast
    1.61 +
    1.62 +lemma reflp_ge_eq:
    1.63 +  "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast
    1.64 +
    1.65 +lemma ge_eq_refl:
    1.66 +  "R \<ge> op= \<Longrightarrow> R x x" by blast
    1.67  
    1.68  text {* Proving a parametrized correspondence relation *}
    1.69  
    1.70 @@ -649,19 +639,10 @@
    1.71  setup Lifting_Info.setup
    1.72  
    1.73  lemmas [reflexivity_rule] = 
    1.74 -  reflp_equality reflp_Quotient_composition is_equality_Quotient_composition 
    1.75 -  left_total_fun left_unique_fun left_total_eq left_unique_eq left_total_composition
    1.76 -  left_unique_composition
    1.77 -
    1.78 -text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
    1.79 -  because we don't want to get reflp' variant of these theorems *}
    1.80 -
    1.81 -setup{*
    1.82 -Context.theory_map 
    1.83 -  (fold
    1.84 -    (snd oo (Thm.apply_attribute Lifting_Info.add_reflexivity_rule_raw_attribute)) 
    1.85 -      [@{thm reflp_fun1}, @{thm reflp_fun2}])
    1.86 -*}
    1.87 +  order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq
    1.88 +  Quotient_composition_ge_eq
    1.89 +  left_total_eq left_unique_eq left_total_composition left_unique_composition
    1.90 +  left_total_fun left_unique_fun
    1.91  
    1.92  (* setup for the function type *)
    1.93  declare fun_quotient[quot_map]
    1.94 @@ -674,6 +655,6 @@
    1.95  
    1.96  ML_file "Tools/Lifting/lifting_setup.ML"
    1.97  
    1.98 -hide_const (open) invariant POS NEG reflp'
    1.99 +hide_const (open) invariant POS NEG
   1.100  
   1.101  end

     2.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Feb 18 21:00:13 2014 +0100
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Feb 18 23:03:47 2014 +0100
     2.3 @@ -31,7 +31,7 @@
     2.4    let
     2.5      fun intro_reflp_tac (ct, i) = 
     2.6      let
     2.7 -      val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm reflpD}
     2.8 +      val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm ge_eq_refl}
     2.9        val concl_pat = Drule.strip_imp_concl (cprop_of rule)
    2.10        val insts = Thm.first_order_match (concl_pat, ct)
    2.11      in

     3.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Tue Feb 18 21:00:13 2014 +0100
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Feb 18 23:03:47 2014 +0100
     3.3 @@ -28,7 +28,6 @@
     3.4    val get_invariant_commute_rules: Proof.context -> thm list
     3.5    
     3.6    val get_reflexivity_rules: Proof.context -> thm list
     3.7 -  val add_reflexivity_rule_raw_attribute: attribute
     3.8    val add_reflexivity_rule_attribute: attribute
     3.9  
    3.10    type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
    3.11 @@ -276,33 +275,14 @@
    3.12  (* info about reflexivity rules *)
    3.13  
    3.14  fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt))
    3.15 -  
    3.16  
    3.17 -(* Conversion to create a reflp' variant of a reflexivity rule  *)
    3.18 -fun safe_reflp_conv ct =
    3.19 -  Conv.try_conv (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm reflp'_def}))) ct
    3.20 -
    3.21 -fun prep_reflp_conv ct = (
    3.22 -      Conv.implies_conv safe_reflp_conv prep_reflp_conv
    3.23 -      else_conv
    3.24 -      safe_reflp_conv
    3.25 -      else_conv
    3.26 -      Conv.all_conv) ct
    3.27 -
    3.28 -fun add_reflexivity_rule_raw thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
    3.29 -val add_reflexivity_rule_raw_attribute = Thm.declaration_attribute add_reflexivity_rule_raw
    3.30 -
    3.31 -fun add_reflexivity_rule thm = add_reflexivity_rule_raw thm #>
    3.32 -  add_reflexivity_rule_raw (Conv.fconv_rule prep_reflp_conv thm)
    3.33 +fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
    3.34  val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
    3.35  
    3.36 -
    3.37  val relfexivity_rule_setup =
    3.38    let
    3.39      val name = @{binding reflexivity_rule}
    3.40 -    fun del_thm_raw thm = Data.map (map_reflexivity_rules (Item_Net.remove thm))
    3.41 -    fun del_thm thm = del_thm_raw thm #>
    3.42 -      del_thm_raw (Conv.fconv_rule prep_reflp_conv thm)
    3.43 +    fun del_thm thm = Data.map (map_reflexivity_rules (Item_Net.remove thm))
    3.44      val del = Thm.declaration_attribute del_thm
    3.45      val text = "rules that are used to prove that a relation is reflexive"
    3.46      val content = Item_Net.content o get_reflexivity_rules'
    3.47 @@ -370,19 +350,42 @@
    3.48      Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule
    3.49    end;
    3.50  
    3.51 +fun add_reflexivity_rules mono_rule ctxt =
    3.52 +  let
    3.53 +    fun find_eq_rule thm ctxt =
    3.54 +      let
    3.55 +        val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o concl_of) thm;
    3.56 +        val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs;
    3.57 +      in
    3.58 +        find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs, 
    3.59 +          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules
    3.60 +      end
    3.61 +
    3.62 +    val eq_rule = find_eq_rule mono_rule (Context.proof_of ctxt);
    3.63 +    val eq_rule = if is_some eq_rule then the eq_rule else error 
    3.64 +      "No corresponding rule that the relator preserves equality was found."
    3.65 +  in
    3.66 +    ctxt
    3.67 +    |> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule]))
    3.68 +    |> add_reflexivity_rule 
    3.69 +      (Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule]))
    3.70 +  end
    3.71 +
    3.72  fun add_mono_rule mono_rule ctxt = 
    3.73    let
    3.74 -    val mono_rule = introduce_polarities mono_rule
    3.75 +    val pol_mono_rule = introduce_polarities mono_rule
    3.76      val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
    3.77 -      dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule
    3.78 +      dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) pol_mono_rule
    3.79      val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name 
    3.80        then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
    3.81        else ()
    3.82 -    val neg_mono_rule = negate_mono_rule mono_rule
    3.83 -    val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule, 
    3.84 +    val neg_mono_rule = negate_mono_rule pol_mono_rule
    3.85 +    val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule, 
    3.86        pos_distr_rules = [], neg_distr_rules = []}
    3.87    in
    3.88 -    Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) ctxt
    3.89 +    ctxt 
    3.90 +    |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data)))
    3.91 +    |> add_reflexivity_rules mono_rule
    3.92    end;
    3.93  
    3.94  local 

     4.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Feb 18 21:00:13 2014 +0100
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Feb 18 23:03:47 2014 +0100
     4.3 @@ -252,7 +252,7 @@
     4.4      val lthy = case opt_reflp_thm of
     4.5        SOME reflp_thm => lthy
     4.6          |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
     4.7 -              [reflp_thm])
     4.8 +              [reflp_thm RS @{thm reflp_ge_eq}])
     4.9          |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
    4.10                [[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
    4.11          |> define_code_constr gen_code quot_thm

     5.1 --- a/src/HOL/Tools/transfer.ML	Tue Feb 18 21:00:13 2014 +0100
     5.2 +++ b/src/HOL/Tools/transfer.ML	Tue Feb 18 23:03:47 2014 +0100
     5.3 @@ -12,6 +12,7 @@
     5.4  
     5.5    val prep_conv: conv
     5.6    val get_transfer_raw: Proof.context -> thm list
     5.7 +  val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
     5.8    val get_relator_eq: Proof.context -> thm list
     5.9    val get_sym_relator_eq: Proof.context -> thm list
    5.10    val get_relator_eq_raw: Proof.context -> thm list
    5.11 @@ -40,6 +41,8 @@
    5.12  (** Theory Data **)
    5.13  
    5.14  val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);
    5.15 +val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq 
    5.16 +  o HOLogic.dest_Trueprop o Thm.concl_of);
    5.17  
    5.18  structure Data = Generic_Data
    5.19  (
    5.20 @@ -56,7 +59,7 @@
    5.21        known_frees = [],
    5.22        compound_lhs = compound_xhs_empty_net,
    5.23        compound_rhs = compound_xhs_empty_net,
    5.24 -      relator_eq = Thm.full_rules,
    5.25 +      relator_eq = rewr_rules,
    5.26        relator_eq_raw = Thm.full_rules,
    5.27        relator_domain = Thm.full_rules }
    5.28    val extend = I
    5.29 @@ -90,6 +93,8 @@
    5.30  fun get_compound_rhs ctxt = ctxt
    5.31    |> (#compound_rhs o Data.get o Context.Proof)
    5.32  
    5.33 +fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt
    5.34 +
    5.35  fun get_relator_eq ctxt = ctxt
    5.36    |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
    5.37    |> map safe_mk_meta_eq