Theory With_Type

section With_Type› -- Setting up the termwith_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 termrp 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, termwith_type C R S rep_ops P means that predicate termP holds whenever
type typ'abs (called the abstract type, and determined by the type of termP)
is an instance of the type class described by C,R, and is a stands in 1-1 correspondence 
to the subset termS of some concrete type typ'rep (i.e., as if defined by
typedef 'abs = S›).

termS -- the carrier set of the representation of the type (concrete type)

termrep_ops -- operations on the concrete type (i.e., operations like addition or similar)

termC -- the properties that termS and termrep_ops are guaranteed to satisfy
(basically, the type-class definition)

termR -- transfers a relation termr between concrete/abstract type to a relation
between concrete/abstract operations (termr is always bi-unique and right-total)

termP -- the predicate that we claim holds.
It can work on the type typ'abs (which is type-classed) but it also gets termrep and termabs_ops
where termrep is an embedding of the abstract into the concrete type, and termabs_ops operations on the abstract type.

The intuitive meaning of termwith_type C R S rep_ops P is that termP 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 constwith_type, we need to define two
  constants specifying the axioms of the class (termWITH_TYPE_CLASS_classname) and
  specifying how a relation between concrete/abstract type is lifted to a relation between
  concrete/abstract operations (termWITH_TYPE_REL_classname). Here we give the
  trivial definitions for the default type class classtype
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 termWITH_TYPE_CLASS_classname and termWITH_TYPE_REL_classname
  are wellbehaved. We do this here for class classtype. We will need this lemma also for
  registering the type class classtype 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 classtype, constwith_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'absbool)  ('rep_ops  'abs_ops  bool)
    and R2 :: ('rep'abs2bool)  ('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'absbool)  ('rep_ops  'abs itself  bool)
    and R2 :: ('rep'abs2bool)  ('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 constwith_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 classtype with the constwith_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 = classtype,
  rep_class = const_nameWITH_TYPE_CLASS_type,
  rep_rel = const_nameWITH_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 constwith_type. This allows to write, e.g.,
  let 't::type = S in P›, and the various relevant parameters such as constWITH_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_syntaxwith_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 termP 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_keywordwith_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