author kuncar Tue, 18 Feb 2014 23:03:47 +0100 changeset 55563 a64d49f49ca3 parent 55562 439d40b226d1 child 55564 e81ee43ab290
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
 src/HOL/Lifting.thy file | annotate | diff | comparison | revisions src/HOL/Tools/Lifting/lifting_def.ML file | annotate | diff | comparison | revisions src/HOL/Tools/Lifting/lifting_info.ML file | annotate | diff | comparison | revisions src/HOL/Tools/Lifting/lifting_setup.ML file | annotate | diff | comparison | revisions src/HOL/Tools/transfer.ML file | annotate | diff | comparison | revisions
```--- 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
-      [@{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

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))
-
+fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm))

-
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;

+  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]))
+      (Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule]))
+  end
+
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)))
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```