Theory Transfer

header {* Transfer Principle *}

theory Transfer
imports StarType
begin

subsection {* Preliminaries *}

text {* These transform expressions like @{term "{n. f (P n)} ∈ \<U>"} *}

lemma fuf_ex:
  "({n. ∃x. P n x} ∈ \<U>) = (∃X. {n. P n (X n)} ∈ \<U>)"
proof
  assume "{n. ∃x. P n x} ∈ \<U>"
  hence "{n. P n (SOME x. P n x)} ∈ \<U>"
    by (auto elim: someI Filter_FUFNat [THEN Filter.subset])
  thus "∃X. {n. P n (X n)} ∈ \<U>" by fast
next
  show "∃X. {n. P n (X n)} ∈ \<U> ==> {n. ∃x. P n x} ∈ \<U>"
    by (auto elim: Filter_FUFNat [THEN Filter.subset])
qed

lemma fuf_not: "({n. ¬ P n} ∈ \<U>) = ({n. P n} ∉ \<U>)"
 apply (subst Collect_neg_eq)
 apply (rule Ultrafilter_FUFNat [THEN Ultrafilter.Compl_iff])
done

lemma fuf_conj:
  "({n. P n ∧ Q n} ∈ \<U>) = ({n. P n} ∈ \<U> ∧ {n. Q n} ∈ \<U>)"
 apply (subst Collect_conj_eq)
 apply (rule Filter_FUFNat [THEN Filter.Int_iff])
done

lemma fuf_disj:
  "({n. P n ∨ Q n} ∈ \<U>) = ({n. P n} ∈ \<U> ∨ {n. Q n} ∈ \<U>)"
 apply (subst Collect_disj_eq)
 apply (rule Ultrafilter_FUFNat [THEN Ultrafilter.Un_iff])
done

lemma fuf_imp:
  "({n. P n --> Q n} ∈ \<U>) = ({n. P n} ∈ \<U> --> {n. Q n} ∈ \<U>)"
by (simp only: imp_conv_disj fuf_disj fuf_not)

lemma fuf_iff:
  "({n. P n = Q n} ∈ \<U>) = (({n. P n} ∈ \<U>) = ({n. Q n} ∈ \<U>))"
by (simp add: iff_conv_conj_imp fuf_conj fuf_imp)

lemma fuf_all:
  "({n. ∀x. P n x} ∈ \<U>) = (∀X. {n. P n (X n)} ∈ \<U>)"
 apply (rule Not_eq_iff [THEN iffD1])
 apply (simp add: fuf_not [symmetric])
 apply (rule fuf_ex)
done

lemma fuf_if_bool:
  "({n. if P n then Q n else R n} ∈ \<U>) =
    (if {n. P n} ∈ \<U> then {n. Q n} ∈ \<U> else {n. R n} ∈ \<U>)"
by (simp add: if_bool_eq_conj fuf_conj fuf_imp fuf_not)

lemma fuf_eq:
  "({n. X n = Y n} ∈ \<U>) = (star_n X = star_n Y)"
by (rule star_n_eq_iff [symmetric])

lemma fuf_if:
  "(STAR n. if P n then X n else Y n) =
    (if {n. P n} ∈ \<U> then star_n X else star_n Y)"
by (auto simp add: star_n_eq_iff fuf_not [symmetric] elim: ultra)

subsection {* Starting the transfer proof *}

text {*
  A transfer theorem asserts an equivalence @{prop "P ≡ P'"}
  between two related propositions. Proposition @{term P} may
  refer to constants having star types, like @{typ "'a star"}.
  Proposition @{term P'} is syntactically similar, but only
  refers to ordinary types (i.e. @{term P'} is the un-starred
  version of @{term P}).
*}

lemma Trueprop_inject: "(Trueprop P ≡ Trueprop Q) ≡ (P ≡ Q)"
proof
  assume "Trueprop P ≡ Trueprop Q" have "P = Q"
  proof
    assume "P" show "Q" by (rule equal_elim_rule1)
  next
    assume "Q" show "P" by (rule equal_elim_rule1 [OF symmetric])
  qed
  thus "P ≡ Q" by simp
next
  assume "P ≡ Q" thus "Trueprop P ≡ Trueprop Q" by simp
qed

text {* This introduction rule starts each transfer proof. *}

lemma transfer_start:
"P ≡ {n. Q} ∈ \<U> ==> Trueprop P ≡ Trueprop Q"
by (simp add: Trueprop_inject atomize_eq)

subsection {* Transfer introduction rules *}

text {*
  The proof of a transfer theorem is completely syntax-directed.
  At each step in the proof, the top-level connective determines
  which introduction rule to apply. Each argument to the top-level
  connective generates a new subgoal.
*}

text {*
  Subgoals in a transfer proof always have the form of an equivalence.
  The left side can be any term, and may contain references to star
  types. The form of the right side depends on its type. At type
  @{typ bool} it takes the form @{term "{n. P n} ∈ \<U>"}. At type
  @{typ "'a star"} it takes the form @{term "STAR n. X n"}. At type
  @{typ "'a star set"} it looks like @{term "Iset (STAR n. A n)"}.
  And at type @{typ "'a star => 'b star"} it has the form
  @{term "Ifun (STAR n. F n)"}.
*}

subsubsection {* Boolean operators *}

lemma transfer_not:
  "[|p ≡ {n. P n} ∈ \<U>|] ==> ¬ p ≡ {n. ¬ P n} ∈ \<U>"
by (simp only: fuf_not)

lemma transfer_conj:
  "[|p ≡ {n. P n} ∈ \<U>; q ≡ {n. Q n} ∈ \<U>|]
    ==> p ∧ q ≡ {n. P n ∧ Q n} ∈ \<U>"
by (simp only: fuf_conj)

lemma transfer_disj:
  "[|p ≡ {n. P n} ∈ \<U>; q ≡ {n. Q n} ∈ \<U>|]
    ==> p ∨ q ≡ {n. P n ∨ Q n} ∈ \<U>"
by (simp only: fuf_disj)

lemma transfer_imp:
  "[|p ≡ {n. P n} ∈ \<U>; q ≡ {n. Q n} ∈ \<U>|]
    ==> p --> q ≡ {n. P n --> Q n} ∈ \<U>"
by (simp only: fuf_imp)

lemma transfer_iff:
  "[|p ≡ {n. P n} ∈ \<U>; q ≡ {n. Q n} ∈ \<U>|]
    ==> p = q ≡ {n. P n = Q n} ∈ \<U>"
by (simp only: fuf_iff)

lemma transfer_if_bool:
  "[|p ≡ {n. P n} ∈ \<U>; x ≡ {n. X n} ∈ \<U>; y ≡ {n. Y n} ∈ \<U>|]
    ==> (if p then x else y) ≡ {n. if P n then X n else Y n} ∈ \<U>"
by (simp only: fuf_if_bool)

lemma transfer_all_bool:
  "[|!!x. p x ≡ {n. P n x} ∈ \<U>|] ==> ∀x::bool. p x ≡ {n. ∀x. P n x} ∈ \<U>"
by (simp only: all_bool_eq fuf_conj)

lemma transfer_ex_bool:
  "[|!!x. p x ≡ {n. P n x} ∈ \<U>|] ==> ∃x::bool. p x ≡ {n. ∃x. P n x} ∈ \<U>"
by (simp only: ex_bool_eq fuf_disj)

subsubsection {* Equals, If *}

lemma transfer_star_eq:
  "[|x ≡ star_n X; y ≡ star_n Y|] ==> x = y ≡ {n. X n = Y n} ∈ \<U>"
by (simp only: fuf_eq)

lemma transfer_star_if:
  "[|p ≡ {n. P n} ∈ \<U>; x ≡ star_n X; y ≡ star_n Y|]
    ==> (if p then x else y) ≡ STAR n. if P n then X n else Y n"
by (simp only: fuf_if)

subsubsection {* Quantifiers *}

lemma transfer_all:
  "[|!!X. p (star_n X) ≡ {n. P n (X n)} ∈ \<U>|]
    ==> ∀x::'a star. p x ≡ {n. ∀x. P n x} ∈ \<U>"
by (simp only: all_star_eq fuf_all)

lemma transfer_ex:
  "[|!!X. p (star_n X) ≡ {n. P n (X n)} ∈ \<U>|]
    ==> ∃x::'a star. p x ≡ {n. ∃x. P n x} ∈ \<U>"
by (simp only: ex_star_eq fuf_ex)

lemma transfer_ex1:
  "[|!!X. p (star_n X) ≡ {n. P n (X n)} ∈ \<U>|]
    ==> ∃!x. p x ≡ {n. ∃!x. P n x} ∈ \<U>"
 apply (unfold Ex1_def)
 apply (simp only: transfer_ex transfer_conj
   transfer_all transfer_imp transfer_star_eq)
done

subsubsection {* Functions *}

lemma transfer_Ifun:
  "[|f ≡ star_n F; x ≡ star_n X|]
    ==> f ∗ x ≡ STAR n. F n (X n)"
by (simp only: Ifun_star_n)

lemma transfer_fun_eq:
  "[|!!X. f (star_n X) = g (star_n X) 
    ≡ {n. F n (X n) = G n (X n)} ∈ \<U>|]
      ==> f = g ≡ {n. F n = G n} ∈ \<U>"
by (simp only: expand_fun_eq transfer_all)

subsubsection {* Sets *}

lemma transfer_Iset:
  "[|a ≡ star_n A|] ==> Iset a ≡ Iset (STAR n. A n)"
by simp

lemma transfer_Collect:
  "[|!!X. p (star_n X) ≡ {n. P n (X n)} ∈ \<U>|]
    ==> Collect p ≡ Iset (STAR n. Collect (P n))"
by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n)

lemma transfer_mem:
  "[|x ≡ star_n X; a ≡ Iset (star_n A)|]
    ==> x ∈ a ≡ {n. X n ∈ A n} ∈ \<U>"
by (simp only: Iset_star_n)

lemma Iset_inject [rule_format]:
  "∀A B. (Iset A = Iset B) = (A = B)"
by (simp add: expand_set_eq all_star_eq
        star_n_eq_iff fuf_all fuf_iff Iset_star_n)

lemma transfer_set_eq:
  "[|x ≡ Iset (star_n X); y ≡ Iset (star_n Y)|]
    ==> x = y ≡ {n. X n = Y n} ∈ \<U>"
by (simp only: Iset_inject fuf_eq)

subsubsection {* Miscellaneous *}

lemma transfer_Ibool:
  "p ≡ star_n P ==> Ibool p ≡ {n. P n} ∈ \<U>"
by (simp only: Ibool_star_n)

lemma transfer_STAR: "STAR n. X n ≡ STAR n. X n"
by (rule reflexive)

lemma transfer_bool: "p ≡ {n. p} ∈ \<U>"
by (simp add: atomize_eq)

lemmas transfer_intros =
  transfer_STAR
  transfer_Ifun
  transfer_fun_eq

  transfer_not
  transfer_conj
  transfer_disj
  transfer_imp
  transfer_iff
  transfer_if_bool
  transfer_all_bool
  transfer_ex_bool

  transfer_all
  transfer_ex
  transfer_ex1

  transfer_Ibool
  transfer_bool
  transfer_star_eq
  transfer_star_if

  transfer_set_eq
  transfer_Iset
  transfer_Collect
  transfer_mem

subsection {* Transfer tactic *}

text {*
  We start by giving ML bindings for the theorems that
  will used by the transfer tactic. Ideally, some of the
  lists of theorems should be expandable.
  To @{text star_class_defs} we would like to add theorems
  about @{term nat_of}, @{term int_of}, @{term meet},
  @{term join}, etc.
  Also, we would like to create introduction rules for new
  constants.
*}

ML_setup {*
val atomizers = map thm ["atomize_all", "atomize_imp", "atomize_eq"]
val Ifun_defs = thms "Ifun_defs" @ [thm "Iset_of_def"]
val star_class_defs = thms "star_class_defs"
val transfer_defs = atomizers @ Ifun_defs @ star_class_defs

val transfer_start = thm "transfer_start"
val transfer_intros = thms "transfer_intros"
val transfer_Ifun = thm "transfer_Ifun"
*}

text {*
  Next we define the ML function @{text unstar_term}.
  This function takes a term, and gives back an equivalent
  term that does not contain any references to the @{text star}
  type constructor. Hopefully the resulting term will still be
  type-correct: Any constant whose type contains @{text star}
  should either be polymorphic (so that it will still work at
  the un-starred instance) or listed in @{text star_consts}
  (so it can be removed).
  Maybe @{text star_consts} should be extensible?
*}

ML_setup {*
local
  fun unstar_typ (Type ("StarType.star",[t])) = unstar_typ t
    | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
    | unstar_typ T = T

  val star_consts =
    [ "StarType.star_of", "StarType.Ifun"
    , "StarType.Ifun_of", "StarType.Ifun2"
    , "StarType.Ifun2_of", "StarType.Ipred"
    , "StarType.Ipred_of", "StarType.Ipred2"
    , "StarType.Ipred2_of", "StarType.Iset"
    , "StarType.Iset_of", "StarType.Ibool" ]

  fun is_star_const a = exists (fn x => x = a) star_consts
in
  fun unstar_term (Const(a,T) $ x) = if (is_star_const a)
                     then (unstar_term x)
                     else (Const(a,unstar_typ T) $ unstar_term x)
    | unstar_term (f $ t) = unstar_term f $ unstar_term t
    | unstar_term (Const(a,T)) = Const(a,unstar_typ T)
    | unstar_term (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar_term t) 
    | unstar_term t = t
end
*}

text {*
  The @{text transfer_thm_of} function takes a term that
  represents a proposition, and proves that it is logically
  equivalent to the un-starred version. Assuming all goes
  well, it returns a theorem asserting the equivalence.
*}

text {*
  TODO: We need some error messages for when things go
  wrong. Errors may be caused by constants that don't have
  matching introduction rules, or quantifiers over wrong types.
*}

ML_setup {*
local
  val tacs =
    [ match_tac [transitive_thm] 1
    , resolve_tac [transfer_start] 1
    , REPEAT_ALL_NEW (resolve_tac transfer_intros) 1
    , match_tac [reflexive_thm] 1 ]
in
  fun transfer_thm_of sg ths t =
      let val u = unstar_term t
          val e = Const("==", propT --> propT --> propT)
          val c = cterm_of sg (e $ t $ u)
      in prove_goalw_cterm (transfer_defs @ ths) c (fn _ => tacs)
      end
end
*}

text {*
  Instead of applying the @{thm [source] transfer_start} rule
  right away, the proof of each transfer theorem starts with the
  transitivity rule @{text "[|P ≡ ?Q; ?Q ≡ P'|] ==> P ≡ P'"}, which
  introduces a new unbound schematic variable @{text ?Q}. The first
  premise @{text "P ≡ ?Q"} is solved by recursively using 
  @{thm [source] transfer_start} and @{thm [source] transfer_intros}.
  Each rule application adds constraints to the form of @{text ?Q};
  by the time the first premise is proved, @{text ?Q} is completely
  bound to the value of @{term P'}. Finally, the second premise is
  resolved with the reflexivity rule @{text "P' ≡ P'"}.
*}

text {*
  The delayed binding is necessary for the correct operation of the
  introduction rule @{thm [source] transfer_Ifun}:
  @{thm transfer_Ifun[of f _ x]}. With a subgoal of the form
  @{term "f ∗ x ≡ STAR n. F n (X n)"}, we would like to bind @{text ?F}
  to @{text F} and @{text ?X} to @{term X}. Unfortunately, higher-order
  unification finds more than one possible match, and binds @{text ?F}
  to @{term "λx. x"} by default. If the right-hand side of the subgoal
  contains an unbound schematic variable instead of the explicit
  application @{term "F n (X n)"}, then we can ensure that there is
  only one possible way to match the rule.
*}

ML_setup {*
fun transfer_tac ths =
    SUBGOAL (fn (t,i) =>
        (fn th =>
            let val tr = transfer_thm_of (sign_of_thm th) ths t
            in rewrite_goals_tac [tr] th
            end
        )
    )
*}

text {*
  Finally we set up the @{text transfer} method. It takes
  an optional list of definitions as arguments; they are
  passed along to @{text transfer_thm_of}, which expands
  the definitions before attempting to prove the transfer
  theorem.
*}

method_setup transfer = {*
  Method.thms_args
    (fn ths => Method.SIMPLE_METHOD' HEADGOAL (transfer_tac ths))
*} "transfer principle"

text {* Sample theorems *}

lemma Ifun_inject: "!!f g. (Ifun f = Ifun g) = (f = g)"
by transfer (rule refl)

lemma Ibool_inject: "!!x y. (Ibool x = Ibool y) = (x = y)"
by transfer (rule refl)

(*
ML {* Goalw transfer_defs
  "Trueprop (Iset_of {} = ({}::'a star set)) ≡
   Trueprop ({} = ({}::'a set))" *}
ML {* by (match_tac [transitive_thm] 1) *}
ML {* by (resolve_tac [transfer_start] 1) *}
ML {* by (REPEAT_ALL_NEW (resolve_tac transfer_intros) 1) *}
ML {* by (match_tac [reflexive_thm] 1) *}
*)
end