meaningful transfer certificate
authorhaftmann
Thu Mar 18 13:56:33 2010 +0100 (2010-03-18)
changeset 35821ee34f03a7d26
parent 35820 b57c3afd1484
child 35822 67e4de90d2c2
meaningful transfer certificate
src/HOL/Nat_Transfer.thy
src/HOL/Tools/transfer.ML
     1.1 --- a/src/HOL/Nat_Transfer.thy	Thu Mar 18 13:56:33 2010 +0100
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Thu Mar 18 13:56:33 2010 +0100
     1.3 @@ -10,12 +10,13 @@
     1.4  
     1.5  subsection {* Generic transfer machinery *}
     1.6  
     1.7 -definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
     1.8 -  where "transfer_morphism f A \<longleftrightarrow> True"
     1.9 +definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
    1.10 +  where "transfer_morphism f A \<longleftrightarrow> (\<forall>P. (\<forall>x. P x) \<longrightarrow> (\<forall>y. A y \<longrightarrow> P (f y)))"
    1.11  
    1.12  lemma transfer_morphismI:
    1.13 -  "transfer_morphism f A"
    1.14 -  by (simp add: transfer_morphism_def)
    1.15 +  assumes "\<And>P y. (\<And>x. P x) \<Longrightarrow> A y \<Longrightarrow> P (f y)"
    1.16 +  shows "transfer_morphism f A"
    1.17 +  using assms by (auto simp add: transfer_morphism_def)
    1.18  
    1.19  use "Tools/transfer.ML"
    1.20  
    1.21 @@ -27,7 +28,7 @@
    1.22  text {* set up transfer direction *}
    1.23  
    1.24  lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
    1.25 -  by (fact transfer_morphismI)
    1.26 +  by (rule transfer_morphismI) simp
    1.27  
    1.28  declare transfer_morphism_nat_int [transfer add
    1.29    mode: manual
    1.30 @@ -266,7 +267,7 @@
    1.31  text {* set up transfer direction *}
    1.32  
    1.33  lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)"
    1.34 -  by (fact transfer_morphismI)
    1.35 +by (rule transfer_morphismI) simp
    1.36  
    1.37  declare transfer_morphism_int_nat [transfer add
    1.38    mode: manual
     2.1 --- a/src/HOL/Tools/transfer.ML	Thu Mar 18 13:56:33 2010 +0100
     2.2 +++ b/src/HOL/Tools/transfer.ML	Thu Mar 18 13:56:33 2010 +0100
     2.3 @@ -23,11 +23,13 @@
     2.4  
     2.5  val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of;
     2.6  
     2.7 +val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI});
     2.8 +
     2.9  fun check_morphism_key ctxt key =
    2.10    let
    2.11 -    val _ = (Thm.match o pairself Thm.cprop_of) (@{thm transfer_morphismI}, key)
    2.12 -      handle Pattern.MATCH => error
    2.13 -        ("Transfer: expected theorem of the form " ^ quote (Display.string_of_thm ctxt @{thm transfer_morphismI}));
    2.14 +    val _ = Thm.match (transfer_morphism_key, Thm.cprop_of key)
    2.15 +      handle Pattern.MATCH => error ("Transfer: expected theorem of the form "
    2.16 +        ^ quote (Syntax.string_of_term ctxt (Thm.term_of transfer_morphism_key)));
    2.17    in direction_of key end;
    2.18  
    2.19  type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list,