implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules

--- a/src/HOL/Lifting.thy	Tue Feb 18 21:00:13 2014 +0100
+++ b/src/HOL/Lifting.thy	Tue Feb 18 23:03:47 2014 +0100
@@ -439,39 +439,23 @@
 
 text {* Proving reflexivity *}
 
-definition reflp' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where "reflp' R \<equiv> reflp R"
-
 lemma Quotient_to_left_total:
   assumes q: "Quotient R Abs Rep T"
   and r_R: "reflp R"
   shows "left_total T"
 using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
 
-lemma reflp_Quotient_composition:
-  assumes "left_total R"
-  assumes "reflp T"
-  shows "reflp (R OO T OO R\<inverse>\<inverse>)"
-using assms unfolding reflp_def left_total_def by fast
-
-lemma reflp_fun1:
-  assumes "is_equality R"
-  assumes "reflp' S"
-  shows "reflp (R ===> S)"
-using assms unfolding is_equality_def reflp'_def reflp_def fun_rel_def by blast
+lemma Quotient_composition_ge_eq:
+  assumes "left_total T"
+  assumes "R \<ge> op="
+  shows "(T OO R OO T\<inverse>\<inverse>) \<ge> op="
+using assms unfolding left_total_def by fast
 
-lemma reflp_fun2:
-  assumes "is_equality R"
-  assumes "is_equality S"
-  shows "reflp (R ===> S)"
-using assms unfolding is_equality_def reflp_def fun_rel_def by blast
-
-lemma is_equality_Quotient_composition:
-  assumes "is_equality T"
-  assumes "left_total R"
-  assumes "left_unique R"
-  shows "is_equality (R OO T OO R\<inverse>\<inverse>)"
-using assms unfolding is_equality_def left_total_def left_unique_def OO_def conversep_iff
-by fastforce
+lemma Quotient_composition_le_eq:
+  assumes "left_unique T"
+  assumes "R \<le> op="
+  shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
+using assms unfolding left_unique_def by fast
 
 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
@@ -479,8 +463,14 @@
 lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
 unfolding left_unique_def OO_def by fast
 
-lemma reflp_equality: "reflp (op =)"
-by (auto intro: reflpI)
+lemma invariant_le_eq:
+  "invariant P \<le> op=" unfolding invariant_def by blast
+
+lemma reflp_ge_eq:
+  "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast
+
+lemma ge_eq_refl:
+  "R \<ge> op= \<Longrightarrow> R x x" by blast
 
 text {* Proving a parametrized correspondence relation *}
 
@@ -649,19 +639,10 @@
 setup Lifting_Info.setup
 
 lemmas [reflexivity_rule] = 
-  reflp_equality reflp_Quotient_composition is_equality_Quotient_composition 
-  left_total_fun left_unique_fun left_total_eq left_unique_eq left_total_composition
-  left_unique_composition
-
-text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
-  because we don't want to get reflp' variant of these theorems *}
-
-setup{*
-Context.theory_map 
-  (fold
-    (snd oo (Thm.apply_attribute Lifting_Info.add_reflexivity_rule_raw_attribute)) 
-      [@{thm reflp_fun1}, @{thm reflp_fun2}])
-*}
+  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]
@@ -674,6 +655,6 @@
 
 ML_file "Tools/Lifting/lifting_setup.ML"
 
-hide_const (open) invariant POS NEG reflp'
+hide_const (open) invariant POS NEG
 
 end

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

--- a/src/HOL/Tools/Lifting/lifting_info.ML	Tue Feb 18 21:00:13 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Feb 18 23:03:47 2014 +0100
@@ -28,7 +28,6 @@
   val get_invariant_commute_rules: Proof.context -> thm list
   
   val get_reflexivity_rules: Proof.context -> thm list
-  val add_reflexivity_rule_raw_attribute: attribute
   val add_reflexivity_rule_attribute: attribute
 
   type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
@@ -276,33 +275,14 @@
 (* info about reflexivity rules *)
 
 fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt))
-  
 
-(* Conversion to create a reflp' variant of a reflexivity rule  *)
-fun safe_reflp_conv ct =
-  Conv.try_conv (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm reflp'_def}))) ct
-
-fun prep_reflp_conv ct = (
-      Conv.implies_conv safe_reflp_conv prep_reflp_conv
-      else_conv
-      safe_reflp_conv
-      else_conv
-      Conv.all_conv) ct
-
-fun add_reflexivity_rule_raw thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
-val add_reflexivity_rule_raw_attribute = Thm.declaration_attribute add_reflexivity_rule_raw
-
-fun add_reflexivity_rule thm = add_reflexivity_rule_raw thm #>
-  add_reflexivity_rule_raw (Conv.fconv_rule prep_reflp_conv thm)
+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_raw thm = Data.map (map_reflexivity_rules (Item_Net.remove thm))
-    fun del_thm thm = del_thm_raw thm #>
-      del_thm_raw (Conv.fconv_rule prep_reflp_conv thm)
+    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'
@@ -370,19 +350,42 @@
     Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule
   end;
 
+fun add_reflexivity_rules mono_rule ctxt =
+  let
+    fun find_eq_rule thm ctxt =
+      let
+        val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o concl_of) thm;
+        val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs;
+      in
+        find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs, 
+          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules
+      end
+
+    val eq_rule = find_eq_rule mono_rule (Context.proof_of ctxt);
+    val eq_rule = if is_some eq_rule then the eq_rule else error 
+      "No corresponding rule that the relator preserves equality was found."
+  in
+    ctxt
+    |> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule]))
+    |> add_reflexivity_rule 
+      (Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule]))
+  end
+
 fun add_mono_rule mono_rule ctxt = 
   let
-    val mono_rule = introduce_polarities mono_rule
+    val pol_mono_rule = introduce_polarities mono_rule
     val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
-      dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule
+      dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) pol_mono_rule
     val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name 
       then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
       else ()
-    val neg_mono_rule = negate_mono_rule mono_rule
-    val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule, 
+    val neg_mono_rule = negate_mono_rule pol_mono_rule
+    val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule, 
       pos_distr_rules = [], neg_distr_rules = []}
   in
-    Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) ctxt
+    ctxt 
+    |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data)))
+    |> add_reflexivity_rules mono_rule
   end;
 
 local 

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Feb 18 21:00:13 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Feb 18 23:03:47 2014 +0100
@@ -252,7 +252,7 @@
     val lthy = case opt_reflp_thm of
       SOME reflp_thm => lthy
         |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
-              [reflp_thm])
+              [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

--- a/src/HOL/Tools/transfer.ML	Tue Feb 18 21:00:13 2014 +0100
+++ b/src/HOL/Tools/transfer.ML	Tue Feb 18 23:03:47 2014 +0100
@@ -12,6 +12,7 @@
 
   val prep_conv: conv
   val get_transfer_raw: Proof.context -> thm list
+  val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
   val get_relator_eq: Proof.context -> thm list
   val get_sym_relator_eq: Proof.context -> thm list
   val get_relator_eq_raw: Proof.context -> thm list
@@ -40,6 +41,8 @@
 (** Theory Data **)
 
 val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);
+val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq 
+  o HOLogic.dest_Trueprop o Thm.concl_of);
 
 structure Data = Generic_Data
 (
@@ -56,7 +59,7 @@
       known_frees = [],
       compound_lhs = compound_xhs_empty_net,
       compound_rhs = compound_xhs_empty_net,
-      relator_eq = Thm.full_rules,
+      relator_eq = rewr_rules,
       relator_eq_raw = Thm.full_rules,
       relator_domain = Thm.full_rules }
   val extend = I
@@ -90,6 +93,8 @@
 fun get_compound_rhs ctxt = ctxt
   |> (#compound_rhs o Data.get o Context.Proof)
 
+fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt
+
 fun get_relator_eq ctxt = ctxt
   |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
   |> map safe_mk_meta_eq