add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
authorhuffman
Wed Apr 04 16:03:01 2012 +0200 (2012-04-04)
changeset 473553d9d98e0f1a4
parent 47354 95846613e414
child 47356 19fb95255ec9
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
src/HOL/Tools/transfer.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Tools/transfer.ML	Wed Apr 04 12:25:58 2012 +0200
     1.2 +++ b/src/HOL/Tools/transfer.ML	Wed Apr 04 16:03:01 2012 +0200
     1.3 @@ -113,6 +113,10 @@
     1.4      rtac thm2 i
     1.5    end handle Match => no_tac | TERM _ => no_tac)
     1.6  
     1.7 +val post_simps =
     1.8 +  @{thms App_def Abs_def transfer_forall_eq [symmetric]
     1.9 +    transfer_implies_eq [symmetric] transfer_bforall_unfold}
    1.10 +
    1.11  fun transfer_tac ctxt = SUBGOAL (fn (t, i) =>
    1.12    let
    1.13      val bs = bnames t
    1.14 @@ -128,8 +132,7 @@
    1.15           rtac @{thm equal_elim_rule1} i THEN
    1.16           rtac (Thm.reflexive (cert ctxt (fst (rename bs u)))) i) i,
    1.17         (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
    1.18 -       rewrite_goal_tac @{thms App_def Abs_def} i,
    1.19 -       rewrite_goal_tac @{thms transfer_forall_eq [symmetric] transfer_implies_eq [symmetric]} i,
    1.20 +       rewrite_goal_tac post_simps i,
    1.21         rtac @{thm _} i]
    1.22    end)
    1.23  
     2.1 --- a/src/HOL/Transfer.thy	Wed Apr 04 12:25:58 2012 +0200
     2.2 +++ b/src/HOL/Transfer.thy	Wed Apr 04 16:03:01 2012 +0200
     2.3 @@ -62,12 +62,19 @@
     2.4  definition transfer_implies where
     2.5    "transfer_implies \<equiv> op \<longrightarrow>"
     2.6  
     2.7 +definition transfer_bforall :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
     2.8 +  where "transfer_bforall \<equiv> (\<lambda>P Q. \<forall>x. P x \<longrightarrow> Q x)"
     2.9 +
    2.10  lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))"
    2.11    unfolding atomize_all transfer_forall_def ..
    2.12  
    2.13  lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)"
    2.14    unfolding atomize_imp transfer_implies_def ..
    2.15  
    2.16 +lemma transfer_bforall_unfold:
    2.17 +  "Trueprop (transfer_bforall P (\<lambda>x. Q x)) \<equiv> (\<And>x. P x \<Longrightarrow> Q x)"
    2.18 +  unfolding transfer_bforall_def atomize_imp atomize_all ..
    2.19 +
    2.20  lemma transfer_start: "\<lbrakk>Rel (op =) P Q; P\<rbrakk> \<Longrightarrow> Q"
    2.21    unfolding Rel_def by simp
    2.22