Theory With_Type

section ‹‹With_Type› -- Setting up the \<^term>‹with_type› mechanism›

theory With_Type
  imports "HOL-Types_To_Sets.Types_To_Sets" Misc_With_Type "HOL-Eisbach.Eisbach"
  keywords "with_type_case" :: prf_asm % "proof"
begin

definition with_type_wellformed where
  ― ‹This states, roughly, that if operations \<^term>‹rp› satisfy the axioms of the class,
      then they are in the domain of the relation between abstract/concrete operations.›
  ‹with_type_wellformed C S R ⟷ (∀r rp. bi_unique r ⟶ right_total r ⟶ S = Collect (Domainp r) ⟶ C S rp ⟶ Domainp (R r) rp)›
    for C :: ‹'rep set ⇒ 'rep_ops ⇒ bool›
    and S :: ‹'rep set›
    and R :: ‹('rep ⇒ 'abs ⇒ bool) ⇒ ('rep_ops ⇒ 'abs_ops ⇒ bool)›

text ‹
In the following definition, roughly speaking, \<^term>‹with_type C R S rep_ops P› means that predicate \<^term>‹P› holds whenever
type \<^typ>‹'abs› (called the abstract type, and determined by the type of \<^term>‹P›)
is an instance of the type class described by C,R, and is a stands in 1-1 correspondence 
to the subset \<^term>‹S› of some concrete type \<^typ>‹'rep› (i.e., as if defined by
‹typedef 'abs = S›).

\<^term>‹S› -- the carrier set of the representation of the type (concrete type)

\<^term>‹rep_ops› -- operations on the concrete type (i.e., operations like addition or similar)

\<^term>‹C› -- the properties that \<^term>‹S› and \<^term>‹rep_ops› are guaranteed to satisfy
(basically, the type-class definition)

\<^term>‹R› -- transfers a relation \<^term>‹r› between concrete/abstract type to a relation
between concrete/abstract operations (\<^term>‹r› is always bi-unique and right-total)

\<^term>‹P› -- the predicate that we claim holds.
It can work on the type \<^typ>‹'abs› (which is type-classed) but it also gets \<^term>‹rep› and \<^term>‹abs_ops›
where \<^term>‹rep› is an embedding of the abstract into the concrete type, and \<^term>‹abs_ops› operations on the abstract type.

The intuitive meaning of \<^term>‹with_type C R S rep_ops P› is that \<^term>‹P› holds for
any type \<^typ>‹'t› that that can be represented by a concrete representation \<^term>‹(S,rep_ops)›
and that has a type class matching the specification \<^term>‹(C,R)›.
›
definition ‹with_type = (λC R S rep_ops P. S≠{} ∧ C S rep_ops ∧ with_type_wellformed C S R
    ∧ (∀rep abs_ops. bij_betw rep UNIV S ⟶ (R (λx y. x = rep y) rep_ops abs_ops) ⟶ 
            P rep abs_ops))›
  for S :: ‹'rep set› and P :: ‹('abs ⇒ 'rep) ⇒ 'abs_ops ⇒ bool›
  and R :: ‹('rep ⇒ 'abs ⇒ bool) ⇒ ('rep_ops ⇒ 'abs_ops ⇒ bool)›
  and C :: ‹'rep set ⇒ 'rep_ops ⇒ bool›
  and rep_ops :: ‹'rep_ops›

text ‹For every type class that we want to use with \<^const>‹with_type›, we need to define two
  constants specifying the axioms of the class (\<^term>‹WITH_TYPE_CLASS_classname›) and
  specifying how a relation between concrete/abstract type is lifted to a relation between
  concrete/abstract operations (\<^term>‹WITH_TYPE_REL_classname›). Here we give the
  trivial definitions for the default type class \<^class>‹type››
definition ‹WITH_TYPE_CLASS_type S ops = True› for S :: ‹'rep set› and ops :: unit
definition ‹WITH_TYPE_REL_type r = ((=) :: unit ⇒ _ ⇒ _)› for r :: ‹'rep ⇒ 'abs ⇒ bool›

named_theorems with_type_intros
  ― ‹In this named fact collection, we collect introduction rules that are used to automatically
  discharge some simple premises in automated methods (currently only ‹with_type_intro›).›

lemma [with_type_intros]: ‹WITH_TYPE_CLASS_type S ops›
  by (simp add: WITH_TYPE_CLASS_type_def)

text ‹We need to show that \<^term>‹WITH_TYPE_CLASS_classname› and \<^term>‹WITH_TYPE_REL_classname›
  are wellbehaved. We do this here for class \<^class>‹type›. We will need this lemma also for
  registering the type class \<^class>‹type› later.›
lemma with_type_wellformed_type[with_type_intros]:
  ‹with_type_wellformed WITH_TYPE_CLASS_type S WITH_TYPE_REL_type›
  by (simp add: WITH_TYPE_REL_type_def WITH_TYPE_CLASS_type_def with_type_wellformed_def Domainp_iff)

lemma with_type_simple: ‹with_type WITH_TYPE_CLASS_type WITH_TYPE_REL_type S () P ⟷ S≠{} ∧ (∀rep. bij_betw rep UNIV S ⟶ P rep ())›
  ― ‹For class \<^class>‹type›, \<^const>‹with_type› can be rewritten in a much more compact and simpler way.›
  by (auto simp: with_type_def WITH_TYPE_REL_type_def WITH_TYPE_CLASS_type_def with_type_wellformed_def)

lemma with_typeI:
  assumes ‹S ≠ {}›
  assumes ‹C S p›
  assumes ‹with_type_wellformed C S R›
  assumes main: ‹⋀(rep :: 'abs ⇒ 'rep) abs_ops. bij_betw rep UNIV S ⟹ R (λx y. x = rep y) p abs_ops ⟹ P rep abs_ops›
  shows ‹with_type C R S p P›
  using assms
  by (auto intro!: simp: with_type_def)

lemma with_type_mp:
  assumes ‹with_type C R S p P›
  assumes ‹⋀rep abs_ops. bij_betw rep UNIV S ⟹ C S p ⟹ P rep abs_ops ⟹ Q rep abs_ops›
  shows ‹with_type C R S p Q›
  using assms by (auto simp add: with_type_def case_prod_beta type_definition_bij_betw_iff)

lemma with_type_nonempty: ‹with_type C R S p P ⟹ S ≠ {}›
  by (simp add: with_type_def case_prod_beta)

lemma with_type_prepare_cancel:
  ― ‹Auxiliary lemma used by the implementation of the ‹cancel_with_type›-mechanism (see below)›
  fixes S :: ‹'rep set› and P :: bool
    and R :: ‹('rep ⇒ 'abs ⇒ bool) ⇒ ('rep_ops ⇒ 'abs_ops ⇒ bool)›
    and C :: ‹'rep set ⇒ 'rep_ops ⇒ bool›
    and p :: ‹'rep_ops›
  assumes wt: ‹with_type C R S p (λ(_::'abs⇒'rep) _. P)›
  assumes ex: ‹(∃(rep::'abs⇒'rep) abs. type_definition rep abs S)›
  shows P
proof -
  from ex
  obtain rep :: ‹'abs ⇒ 'rep› and abs where td: ‹type_definition rep abs S›
    by auto
  then have bij: ‹bij_betw rep UNIV S›
    by (simp add: bij_betw_def inj_on_def type_definition.Rep_inject type_definition.Rep_range)
  define r where ‹r = (λx y. x = rep y)›
  have [simp]: ‹bi_unique r› ‹right_total r›
    using r_def td typedef_bi_unique apply blast
    by (simp add: r_def right_totalI)
  have aux1: ‹(⋀x. rep x ∈ S) ⟹ x ∈ S ⟹ x = rep (abs x)› for x b
    using td type_definition.Abs_inverse by fastforce
  have Sr: ‹S = Collect (Domainp r)›
    using type_definition.Rep[OF td]
    by (auto simp: r_def intro!: DomainPI aux1)
  from wt have nice: ‹with_type_wellformed C S R› and ‹C S p›
    by (simp_all add: with_type_def case_prod_beta)
  from nice[unfolded with_type_wellformed_def, rule_format, OF ‹bi_unique r› ‹right_total r› Sr ‹C S p›]
  obtain abs_ops where abs_ops: ‹R (λx y. x = rep y) p abs_ops›
    apply atomize_elim by (auto simp: r_def)
  from bij abs_ops wt
  show P
    by (auto simp: with_type_def case_prod_beta)
qed

lemma with_type_transfer_class:
  ― ‹Auxiliary lemma used by ML function ‹cancel_with_type››
  includes lifting_syntax
  fixes Rep :: ‹'abs ⇒ 'rep›
    and C S
    and R :: ‹('rep⇒'abs⇒bool) ⇒ ('rep_ops ⇒ 'abs_ops ⇒ bool)›
    and R2 :: ‹('rep⇒'abs2⇒bool) ⇒ ('rep_ops ⇒ 'abs_ops2 ⇒ bool)›
  assumes trans: ‹⋀r :: 'rep ⇒ 'abs2 ⇒ bool. bi_unique r ⟹ right_total r ⟹ (R2 r ===> (⟷)) (C (Collect (Domainp r))) axioms›
  assumes nice: ‹with_type_wellformed C S R2›
  assumes wt: ‹with_type C R S p P›
  assumes ex: ‹∃(Rep :: 'abs2⇒'rep) Abs. type_definition Rep Abs S›
  shows ‹∃x::'abs_ops2. axioms x›
proof -
  from ex obtain Rep :: ‹'abs2⇒'rep› and Abs where td: ‹type_definition Rep Abs S›
    by auto
  define r where ‹r x y = (x = Rep y)› for x y
  have bi_unique_r: ‹bi_unique r›
    using bi_unique_def td type_definition.Rep_inject r_def by fastforce
  have right_total_r: ‹right_total r›
    by (simp add: right_totalI r_def)
  have right_total_R[transfer_rule]: ‹right_total (r ===> r ===> r)›
    by (meson bi_unique_r right_total_r bi_unique_alt_def right_total_fun)
  note trans = trans[OF bi_unique_r, OF right_total_r, transfer_rule]

  from td
  have rS: ‹Collect (Domainp r) = S›
    by (auto simp: r_def Domainp_iff type_definition.Rep  elim!: type_definition.Rep_cases[where P=‹Ex _›])

  from wt have sg: ‹C S p›
    by (simp_all add: with_type_def case_prod_beta)

  with nice have ‹Domainp (R2 r) p›
    by (simp add: bi_unique_r with_type_wellformed_def rS right_total_r)
  
  with sg
  have ‹∃x :: 'abs_ops2. axioms x›
    apply (transfer' fixing: R2 S p)
    using apply_rsp' local.trans rS by fastforce
  
  then obtain abs_plus :: 'abs_ops2 
    where abs_plus: ‹axioms abs_plus›
    apply atomize_elim by auto

  then show ?thesis
    by auto
qed

lemma with_type_transfer_class2:
  ― ‹Auxiliary lemma used by ML function ‹cancel_with_type››
  includes lifting_syntax
  fixes Rep :: ‹'abs ⇒ 'rep›
    and C S
    and R :: ‹('rep⇒'abs⇒bool) ⇒ ('rep_ops ⇒ 'abs itself ⇒ bool)›
    and R2 :: ‹('rep⇒'abs2⇒bool) ⇒ ('rep_ops ⇒ 'abs2 itself ⇒ bool)›
  assumes trans: ‹⋀r :: 'rep ⇒ 'abs2 ⇒ bool. bi_unique r ⟹ right_total r ⟹ (R2 r ===> (⟷)) (C (Collect (Domainp r))) axioms›
  assumes nice: ‹with_type_wellformed C S R2› (* Not used, but the ML-code expects it to be there currently. *)
  assumes rel_itself: ‹⋀(r :: 'rep ⇒ 'abs2 ⇒ bool) p. bi_unique r ⟹ right_total r ⟹ (R2 r) p TYPE('abs2)›
  assumes wt: ‹with_type C R S p P›
  assumes ex: ‹∃(Rep :: 'abs2⇒'rep) Abs. type_definition Rep Abs S›
  shows ‹axioms TYPE('abs2)›
proof -
  from ex obtain Rep :: ‹'abs2⇒'rep› and Abs where td: ‹type_definition Rep Abs S›
    by auto
  define r where ‹r x y = (x = Rep y)› for x y
  have bi_unique_r: ‹bi_unique r›
    using bi_unique_def td type_definition.Rep_inject r_def by fastforce
  have right_total_r: ‹right_total r›
    by (simp add: right_totalI r_def)
  have right_total_R[transfer_rule]: ‹right_total (r ===> r ===> r)›
    by (meson bi_unique_r right_total_r bi_unique_alt_def right_total_fun)

  from td
  have rS: ‹Collect (Domainp r) = S›
    by (auto simp: r_def Domainp_iff type_definition.Rep elim!: type_definition.Rep_cases[where P=‹Ex _›])

  note trans = trans[OF bi_unique_r, OF right_total_r, unfolded rS, transfer_rule]

  note rel_itself = rel_itself[OF bi_unique_r, OF right_total_r, of p, transfer_rule]

  from wt have sg: ‹C S p›
    by (simp_all add: with_type_def case_prod_beta)
  then show ‹axioms TYPE('abs2)›
    by transfer
qed

text ‹Syntactic constants for rendering \<^const>‹with_type› nicely.›
syntax "_with_type" :: "type ⇒ 'a => 'b ⇒ 'c" (‹let _ = _ in _› [0,0,10] 10)
syntax "_with_type_with" :: "type ⇒ 'a => args ⇒ 'b ⇒ 'c" (‹let _ = _ with _ in _› [0,0,10] 10)
syntax (output) "_with_type_sort_annotation" :: "type ⇒ sort ⇒ type" (‹_::_›)
  ― ‹An auxiliary syntactic constant used to enforce the printing of sort constraints in certain terms.›

ML_file "with_type.ML"


text ‹Register the type class \<^class>‹type› with the \<^const>‹with_type›-mechanism.
  This enables readable syntax, and contains information needed by various tools
  such as the ‹cancel_with_type› attribute.›
setup ‹
With_Type.add_with_type_info_global {
  class = \<^class>‹type›,
  rep_class = \<^const_name>‹WITH_TYPE_CLASS_type›,
  rep_rel = \<^const_name>‹WITH_TYPE_REL_type›,
  with_type_wellformed = @{thm with_type_wellformed_type},
  param_names = [],
  transfer = NONE,
  rep_rel_itself = NONE
}›

text ‹Enabling input/output syntax for \<^const>‹with_type›. This allows to write, e.g.,
  ‹let 't::type = S in P›, and the various relevant parameters such as \<^const>‹WITH_TYPE_CLASS_type› etc.
  are automatically looked up based on the indicated type class.
  This only works with type classes that have been registered beforehand.

  Using the syntax when printing can be disabled by ‹declare [[with_type_syntax=false]]›.›
parse_translation ‹[
  (\<^syntax_const>‹_with_type›, With_Type.with_type_parse_translation),
  (\<^syntax_const>‹_with_type_with›, With_Type.with_type_parse_translation)
]›
typed_print_translation ‹[ (\<^const_syntax>‹with_type›, With_Type.with_type_print_translation) ]›


text ‹Example of input syntax:›
term ‹let 't::type = N in rep_t = rep_t›


text ‹Removes a toplevel ‹let 't=…› from a proposition ‹let 't=… in P›.
  This only works if \<^term>‹P› does not refer to the type \<^typ>‹'t›.›
attribute_setup cancel_with_type =
  ‹Thm.rule_attribute [] (With_Type.cancel_with_type o Context.proof_of) |> Scan.succeed›
  ‹Transforms (let 't=… in P) into P›


text ‹Convenience method for proving a theorem of the form ‹let 't=…›.›
method with_type_intro = rule with_typeI; (intro with_type_intros)?


text ‹Method for doing a modus ponens inside ‹let 't=…›.
Use as: ‹using PREMISE proof with_type_mp›.
And inside the proof, use the command ‹with_type_case› before proving the main goal.
Try ‹print_theorems› after ‹with_type_case› to see what it sets up.
›
method_setup with_type_mp = ‹Scan.succeed () >> 
  (fn (_) => fn ctxt => CONTEXT_METHOD (fn facts =>
      Method.RUNTIME (With_Type.with_type_mp_tac ⌂ facts)))›

ML ‹
val _ =
  Outer_Syntax.command \<^command_keyword>‹with_type_case› "Sets up local proof after the \<^method>‹with_type_mp› method (for the main goal)."
    (Scan.repeat (Parse.maybe Parse.binding) >> (fn args => Toplevel.proof (With_Type.with_type_case_cmd args)))
›


end