author kuncar Tue Feb 18 23:03:47 2014 +0100 (2014-02-18) 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 | revisions src/HOL/Tools/Lifting/lifting_def.ML file | annotate | diff | revisions src/HOL/Tools/Lifting/lifting_info.ML file | annotate | diff | revisions src/HOL/Tools/Lifting/lifting_setup.ML file | annotate | diff | revisions src/HOL/Tools/transfer.ML file | annotate | diff | revisions
```     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 -
1.21 -lemma reflp_fun1:
1.22 -  assumes "is_equality R"
1.23 -  assumes "reflp' S"
1.24 -  shows "reflp (R ===> S)"
1.25 -using assms unfolding is_equality_def reflp'_def reflp_def fun_rel_def by blast
1.26 +lemma Quotient_composition_ge_eq:
1.27 +  assumes "left_total T"
1.28 +  assumes "R \<ge> op="
1.29 +  shows "(T OO R OO T\<inverse>\<inverse>) \<ge> op="
1.30 +using assms unfolding left_total_def by fast
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.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.30 -
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.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.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.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
```