src/HOL/Transfer.thy
changeset 51956 a4d81cdebf8b
parent 51955 04d9381bebff
child 52354 acb4f932dd24
     1.1 --- a/src/HOL/Transfer.thy	Mon May 13 12:13:24 2013 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Mon May 13 13:59:04 2013 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:      HOL/Transfer.thy
     1.5      Author:     Brian Huffman, TU Muenchen
     1.6 +    Author:     Ondrej Kuncar, TU Muenchen
     1.7  *)
     1.8  
     1.9  header {* Generic theorem transfer using relations *}
    1.10 @@ -103,10 +104,6 @@
    1.11    shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
    1.12    using assms unfolding Rel_def fun_rel_def by fast
    1.13  
    1.14 -text {* Handling of domains *}
    1.15 -
    1.16 -definition DOM :: "('a => 'b => bool) => ('a => bool) => bool" where "DOM T R \<equiv> Domainp T = R"
    1.17 -
    1.18  ML_file "Tools/transfer.ML"
    1.19  setup Transfer.setup
    1.20  
    1.21 @@ -116,6 +113,10 @@
    1.22  
    1.23  hide_const (open) Rel
    1.24  
    1.25 +text {* Handling of domains *}
    1.26 +
    1.27 +lemma Domaimp_refl[transfer_domain_rule]:
    1.28 +  "Domainp T = Domainp T" ..
    1.29  
    1.30  subsection {* Predicates on relations, i.e. ``class constraints'' *}
    1.31  
    1.32 @@ -264,6 +265,21 @@
    1.33    shows "(A ===> A ===> op =) (op =) (op =)"
    1.34    using assms unfolding bi_unique_def fun_rel_def by auto
    1.35  
    1.36 +lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
    1.37 +  by auto
    1.38 +
    1.39 +lemma right_total_Ex_transfer[transfer_rule]:
    1.40 +  assumes "right_total A"
    1.41 +  shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
    1.42 +using assms unfolding right_total_def Bex_def fun_rel_def Domainp_iff[abs_def]
    1.43 +by blast
    1.44 +
    1.45 +lemma right_total_All_transfer[transfer_rule]:
    1.46 +  assumes "right_total A"
    1.47 +  shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All"
    1.48 +using assms unfolding right_total_def Ball_def fun_rel_def Domainp_iff[abs_def]
    1.49 +by blast
    1.50 +
    1.51  lemma All_transfer [transfer_rule]:
    1.52    assumes "bi_total A"
    1.53    shows "((A ===> op =) ===> op =) All All"
    1.54 @@ -304,13 +320,6 @@
    1.55    "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
    1.56    unfolding funpow_def by transfer_prover
    1.57  
    1.58 -text {* Fallback rule for transferring universal quantifiers over
    1.59 -  correspondence relations that are not bi-total, and do not have
    1.60 -  custom transfer rules (e.g. relations between function types). *}
    1.61 -
    1.62 -lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
    1.63 -  by auto
    1.64 -
    1.65  lemma Domainp_forall_transfer [transfer_rule]:
    1.66    assumes "right_total A"
    1.67    shows "((A ===> op =) ===> op =)
    1.68 @@ -319,9 +328,6 @@
    1.69    unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff
    1.70    by metis
    1.71  
    1.72 -text {* Preferred rule for transferring universal quantifiers over
    1.73 -  bi-total correspondence relations (later rules are tried first). *}
    1.74 -
    1.75  lemma forall_transfer [transfer_rule]:
    1.76    "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
    1.77    unfolding transfer_forall_def by (rule All_transfer)