Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set



Dear Lukas Stevens and Akihisa Yamada/All,

I would like to make a side remark with regard to the discussion and ask a couple of related questions to the developers/maintainers of Isabelle.

------------------------------------------------

While I am also not certain whether and how one could construct a rewrite system capable of coping with the problem outlined by Lukas Stevens (although it seems like the application of the attribute "simplified" with the default simpset can remove "True" in most cases, so it may be worth trying to understand the principle employed), there is little that could stop one from batch-processing the theorems after the locale interpretation: see the code listing in the appendix. Potentially, one can even override the theorems that were produced during the interpretation in this manner. However, keep in mind that the code is merely a very rough sketch of the idea, not a working implementation (e.g. one would need to consider how to propagate the effects of the attributes that were applied to the original theorems and several other issues). 

------------------------------------------------

In this context, I would like to ask two questions to the developers of Isabelle:
1. I am curious as to what exactly is preventing from allowing users to provide more general/arbitrary theorem transformations during the locale interpretation, instead of plain rewriting.
2. I am curious if there is a way to allow for an application of a given predefined rewrite system repeatedly to different distinct interpretations. For example, if one was to develop a rewrite system for eliminating "True" from theorems, it would be useful to allow for its repeated application without code duplication. However, at the moment, it seems like one would have to restate the relevant terms explicitly for every interpretation (unless I am mistaken, and there already exists an implementation of this functionality).

Kind Regards,
Mikhail Chekhov

theory Scratch
  imports Main
  keywords "attributes_for_qual" :: thy_defn
begin

ML‹

(*copied with amendments from the file Proof_Context.ML
in the main distribution of Isabelle2021-RC2*)
fun get_local_facts verbose ctxt =
  let
    val facts = Proof_Context.facts_of ctxt
    val props = map #1 (Facts.props facts)
    val local_facts =
      (if null props then [] else [("<unnamed>", props)]) @
        Facts.dest_static
          verbose [Global_Theory.facts_of (Proof_Context.theory_of ctxt)] facts
  in local_facts end;

fun append_local c = "local." ^ c ^ ".";
fun remove_local c = String.extract (c, 6, NONE);

fun prep_attrb_facts ctxt attrbs (b, thms)  =
  let
    val facts' =
      ((b, attrbs) ||> map (Attrib.check_src ctxt), single (thms, []))
      |> single
      |> Attrib.partial_evaluation ctxt
  in facts' end;

fun process_simplify (qualc, attrbs) ctxt =
  let
    val mk_name = remove_local
      #> curry (swap #> op^) "'"
      #> Binding.qualified_name
    val thmss = get_local_facts false ctxt
      |> filter (fn (c, _) => String.isPrefix (append_local qualc) c)
      |> map (apfst mk_name)
    val factss = thmss |> map (prep_attrb_facts ctxt attrbs)
  in fold (curry (uncurry Local_Theory.notes #> snd)) factss ctxt end;

val _ = Outer_Syntax.local_theory
  \<^command_keyword>‹attributes_for_qual›
    "apply attributes to a set of theorems in the local context"
  (Parse.string -- Parse.attribs >> process_simplify);



axiomatization P :: "'a ⇒ bool"
axiomatization Z :: "'a ⇒ bool"

locale foo =
  fixes A :: "'a set"
begin

lemma bar: "X ⊆ A ⟹ Z A ⟹ P X"
  sorry

end

locale bar
begin

sublocale foo: foo UNIV
  rewrites "Y ⊆ UNIV ≡ True"
    and "⋀Q. (True ⟹ PROP Q) ≡ Q"
    and "⋀Q. (True ⟹ Q) ≡ Trueprop Q"
  by auto

attributes_for_qual "foo" [simplified]

thm foo.bar'

end

end


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.