# HG changeset patch
# User huffman
# Date 1126041069 -7200
# Node ID fadf6e1faa16715a6a78b3e13dd09d4d0ca15a97
# Parent  d7acf9f05eb29cad8793e607131afa1c7bdb9918
transfer principle tactic

diff -r d7acf9f05eb2 -r fadf6e1faa16 src/HOL/Hyperreal/Transfer.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/Transfer.thy	Tue Sep 06 23:11:09 2005 +0200
@@ -0,0 +1,417 @@
+(*  Title       : HOL/Hyperreal/Transfer.thy
+    ID          : $Id$
+    Author      : Brian Huffman
+*)
+
+header {* Transfer Principle *}
+
+theory Transfer
+imports StarType
+begin
+
+subsection {* Preliminaries *}
+
+text {* These transform expressions like @{term "{n. f (P n)} \<in> \<U>"} *}
+
+lemma fuf_ex:
+  "({n. \<exists>x. P n x} \<in> \<U>) = (\<exists>X. {n. P n (X n)} \<in> \<U>)"
+proof
+  assume "{n. \<exists>x. P n x} \<in> \<U>"
+  hence "{n. P n (SOME x. P n x)} \<in> \<U>"
+    by (auto elim: someI filter.subset [OF filter_FUFNat])
+  thus "\<exists>X. {n. P n (X n)} \<in> \<U>" by fast
+next
+  show "\<exists>X. {n. P n (X n)} \<in> \<U> \<Longrightarrow> {n. \<exists>x. P n x} \<in> \<U>"
+    by (auto elim: filter.subset [OF filter_FUFNat])
+qed
+
+lemma fuf_not: "({n. \<not> P n} \<in> \<U>) = ({n. P n} \<notin> \<U>)"
+ apply (subst Collect_neg_eq)
+ apply (rule ultrafilter.Compl_iff [OF ultrafilter_FUFNat])
+done
+
+lemma fuf_conj:
+  "({n. P n \<and> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<and> {n. Q n} \<in> \<U>)"
+ apply (subst Collect_conj_eq)
+ apply (rule filter.Int_iff [OF filter_FUFNat])
+done
+
+lemma fuf_disj:
+  "({n. P n \<or> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<or> {n. Q n} \<in> \<U>)"
+ apply (subst Collect_disj_eq)
+ apply (rule ultrafilter.Un_iff [OF ultrafilter_FUFNat])
+done
+
+lemma fuf_imp:
+  "({n. P n \<longrightarrow> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<longrightarrow> {n. Q n} \<in> \<U>)"
+by (simp only: imp_conv_disj fuf_disj fuf_not)
+
+lemma fuf_iff:
+  "({n. P n = Q n} \<in> \<U>) = (({n. P n} \<in> \<U>) = ({n. Q n} \<in> \<U>))"
+by (simp add: iff_conv_conj_imp fuf_conj fuf_imp)
+
+lemma fuf_all:
+  "({n. \<forall>x. P n x} \<in> \<U>) = (\<forall>X. {n. P n (X n)} \<in> \<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} \<in> \<U>) =
+    (if {n. P n} \<in> \<U> then {n. Q n} \<in> \<U> else {n. R n} \<in> \<U>)"
+by (simp add: if_bool_eq_conj fuf_conj fuf_imp fuf_not)
+
+lemma fuf_eq:
+  "({n. X n = Y n} \<in> \<U>) = (star_n X = star_n Y)"
+by (rule star_n_eq_iff [symmetric])
+
+lemma fuf_if:
+  "star_n (\<lambda>n. if P n then X n else Y n) =
+    (if {n. P n} \<in> \<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 \<equiv> 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}).
+*}
+
+text {* This introduction rule starts each transfer proof. *}
+
+lemma transfer_start:
+  "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
+by (subgoal_tac "P \<equiv> Q", simp, simp add: 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} \<in> \<U>"}. At type
+  @{typ "'a star"} it takes the form @{term "star_n (\<lambda>n. X n)"}. At type
+  @{typ "'a star set"} it looks like @{term "Iset (star_n (\<lambda>n. A n))"}.
+  And at type @{typ "'a star \<Rightarrow> 'b star"} it has the form
+  @{term "Ifun (star_n (\<lambda>n. F n))"}.
+*}
+
+subsubsection {* Boolean operators *}
+
+lemma transfer_not:
+  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
+by (simp only: fuf_not)
+
+lemma transfer_conj:
+  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
+by (simp only: fuf_conj)
+
+lemma transfer_disj:
+  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
+by (simp only: fuf_disj)
+
+lemma transfer_imp:
+  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
+by (simp only: fuf_imp)
+
+lemma transfer_iff:
+  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
+by (simp only: fuf_iff)
+
+lemma transfer_if_bool:
+  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
+by (simp only: fuf_if_bool)
+
+lemma transfer_all_bool:
+  "\<lbrakk>\<And>x. p x \<equiv> {n. P n x} \<in> \<U>\<rbrakk> \<Longrightarrow> \<forall>x::bool. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
+by (simp only: all_bool_eq fuf_conj)
+
+lemma transfer_ex_bool:
+  "\<lbrakk>\<And>x. p x \<equiv> {n. P n x} \<in> \<U>\<rbrakk> \<Longrightarrow> \<exists>x::bool. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
+by (simp only: ex_bool_eq fuf_disj)
+
+subsubsection {* Equals, If *}
+
+lemma transfer_eq:
+  "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
+by (simp only: fuf_eq)
+
+lemma transfer_if:
+  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
+    \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
+by (simp only: fuf_if)
+
+subsubsection {* Quantifiers *}
+
+lemma transfer_all:
+  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
+by (simp only: all_star_eq fuf_all)
+
+lemma transfer_ex:
+  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
+by (simp only: ex_star_eq fuf_ex)
+
+lemma transfer_ex1:
+  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> \<exists>!x. p x \<equiv> {n. \<exists>!x. P n x} \<in> \<U>"
+by (simp only: Ex1_def transfer_ex transfer_conj
+   transfer_all transfer_imp transfer_eq)
+
+subsubsection {* Functions *}
+
+lemma transfer_Ifun:
+  "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk>
+    \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
+by (simp only: Ifun_star_n)
+
+lemma transfer_fun_eq:
+  "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
+    \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
+      \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
+by (simp only: expand_fun_eq transfer_all)
+
+subsubsection {* Sets *}
+
+lemma transfer_Iset:
+  "\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))"
+by simp
+
+lemma transfer_Collect:
+  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
+by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n)
+
+lemma transfer_mem:
+  "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
+    \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
+by (simp only: Iset_star_n)
+
+lemma transfer_set_eq:
+  "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
+    \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
+by (simp only: expand_set_eq transfer_all transfer_iff transfer_mem)
+
+lemma transfer_ball:
+  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
+by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
+
+lemma transfer_bex:
+  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
+by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
+
+subsubsection {* Miscellaneous *}
+
+lemma transfer_unstar:
+  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
+by (simp only: unstar_star_n)
+
+lemma transfer_star_n: "star_n X \<equiv> star_n (\<lambda>n. X n)"
+by (rule reflexive)
+
+lemma transfer_bool: "p \<equiv> {n. p} \<in> \<U>"
+by (simp add: atomize_eq)
+
+lemmas transfer_intros =
+  transfer_star_n
+  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_unstar
+  transfer_bool
+  transfer_eq
+  transfer_if
+
+  transfer_set_eq
+  transfer_Iset
+  transfer_Collect
+  transfer_mem
+  transfer_ball
+  transfer_bex
+
+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.unstar" ]
+
+  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 "\<lbrakk>P \<equiv> ?Q; ?Q \<equiv> P'\<rbrakk> \<Longrightarrow> P \<equiv> P'"}, which
+  introduces a new unbound schematic variable @{text ?Q}. The first
+  premise @{text "P \<equiv> ?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' \<equiv> 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 \<star> x \<equiv> star_n (\<lambda>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 "\<lambda>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: "\<And>f g. (Ifun f = Ifun g) = (f = g)"
+by transfer (rule refl)
+
+lemma unstar_inject: "\<And>x y. (unstar x = unstar y) = (x = y)"
+by transfer (rule refl)
+
+lemma Iset_inject: "\<And>A B. (Iset A = Iset B) = (A = B)"
+by transfer (rule refl)
+
+end