# HG changeset patch # User kuncar # Date 1392761027 -3600 # Node ID a64d49f49ca394a9f884a35c01579bc58cf1a2d0 # Parent 439d40b226d1a4ab707ae1f7d8e9026f3a275166 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules diff -r 439d40b226d1 -r a64d49f49ca3 src/HOL/Lifting.thy --- 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 \ 'a \ bool) \ bool" where "reflp' R \ 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\\)" -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 \ op=" + shows "(T OO R OO T\\) \ 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\\)" -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 \ op=" + shows "(T OO R OO T\\) \ op=" +using assms unfolding left_unique_def by fast lemma left_total_composition: "left_total R \ left_total S \ left_total (R OO S)" unfolding left_total_def OO_def by fast @@ -479,8 +463,14 @@ lemma left_unique_composition: "left_unique R \ left_unique S \ 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 \ op=" unfolding invariant_def by blast + +lemma reflp_ge_eq: + "reflp R \ R \ op=" unfolding reflp_def by blast + +lemma ge_eq_refl: + "R \ op= \ 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 diff -r 439d40b226d1 -r a64d49f49ca3 src/HOL/Tools/Lifting/lifting_def.ML --- 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 diff -r 439d40b226d1 -r a64d49f49ca3 src/HOL/Tools/Lifting/lifting_info.ML --- 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 diff -r 439d40b226d1 -r a64d49f49ca3 src/HOL/Tools/Lifting/lifting_setup.ML --- 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 diff -r 439d40b226d1 -r a64d49f49ca3 src/HOL/Tools/transfer.ML --- 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