rationalized lemmas
authorblanchet
Mon Jan 20 20:42:43 2014 +0100 (2014-01-20)
changeset 550848ee9aabb2bca
parent 55083 0a689157e3ce
child 55085 0e8e4dc55866
rationalized lemmas
src/HOL/BNF_LFP.thy
src/HOL/BNF_Util.thy
src/HOL/Basic_BNFs.thy
src/HOL/Lifting_Sum.thy
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/BNF_LFP.thy	Mon Jan 20 20:21:12 2014 +0100
     1.2 +++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 20:42:43 2014 +0100
     1.3 @@ -222,7 +222,7 @@
     1.4  lemma meta_spec2:
     1.5    assumes "(\<And>x y. PROP P x y)"
     1.6    shows "PROP P x y"
     1.7 -by (rule `(\<And>x y. PROP P x y)`)
     1.8 +by (rule assms)
     1.9  
    1.10  lemma nchotomy_relcomppE:
    1.11    "\<lbrakk>\<And>y. \<exists>x. y = f x; (r OO s) a c; \<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.12 @@ -234,10 +234,15 @@
    1.13  lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
    1.14    unfolding vimage2p_def by auto
    1.15  
    1.16 +lemma id_transfer: "fun_rel A A id id"
    1.17 +unfolding fun_rel_def by simp
    1.18 +
    1.19  ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
    1.20  ML_file "Tools/BNF/bnf_lfp_util.ML"
    1.21  ML_file "Tools/BNF/bnf_lfp_tactics.ML"
    1.22  ML_file "Tools/BNF/bnf_lfp.ML"
    1.23  ML_file "Tools/BNF/bnf_lfp_compat.ML"
    1.24  
    1.25 +hide_fact (open) id_transfer
    1.26 +
    1.27  end
     2.1 --- a/src/HOL/BNF_Util.thy	Mon Jan 20 20:21:12 2014 +0100
     2.2 +++ b/src/HOL/BNF_Util.thy	Mon Jan 20 20:42:43 2014 +0100
     2.3 @@ -10,9 +10,23 @@
     2.4  
     2.5  theory BNF_Util
     2.6  imports BNF_Cardinal_Arithmetic
     2.7 -  Transfer (*FIXME: define fun_rel here, reuse in Transfer once this theory is in HOL*)
     2.8  begin
     2.9  
    2.10 +definition
    2.11 +  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
    2.12 +where
    2.13 +  "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
    2.14 +
    2.15 +lemma fun_relI [intro]:
    2.16 +  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
    2.17 +  shows "fun_rel A B f g"
    2.18 +  using assms by (simp add: fun_rel_def)
    2.19 +
    2.20 +lemma fun_relD:
    2.21 +  assumes "fun_rel A B f g" and "A x y"
    2.22 +  shows "B (f x) (g y)"
    2.23 +  using assms by (simp add: fun_rel_def)
    2.24 +
    2.25  definition collect where
    2.26  "collect F x = (\<Union>f \<in> F. f x)"
    2.27  
     3.1 --- a/src/HOL/Basic_BNFs.thy	Mon Jan 20 20:21:12 2014 +0100
     3.2 +++ b/src/HOL/Basic_BNFs.thy	Mon Jan 20 20:42:43 2014 +0100
     3.3 @@ -11,7 +11,6 @@
     3.4  
     3.5  theory Basic_BNFs
     3.6  imports BNF_Def
     3.7 -   (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
     3.8  begin
     3.9  
    3.10  bnf ID: 'a
     4.1 --- a/src/HOL/Lifting_Sum.thy	Mon Jan 20 20:21:12 2014 +0100
     4.2 +++ b/src/HOL/Lifting_Sum.thy	Mon Jan 20 20:42:43 2014 +0100
     4.3 @@ -12,19 +12,12 @@
     4.4  
     4.5  abbreviation (input) "sum_pred \<equiv> sum_case"
     4.6  
     4.7 -lemma sum_rel_eq [relator_eq]:
     4.8 -  "sum_rel (op =) (op =) = (op =)"
     4.9 -  by (simp add: sum_rel_def fun_eq_iff split: sum.split)
    4.10 -
    4.11 -lemma sum_rel_mono[relator_mono]:
    4.12 -  assumes "A \<le> C"
    4.13 -  assumes "B \<le> D"
    4.14 -  shows "(sum_rel A B) \<le> (sum_rel C D)"
    4.15 -using assms by (auto simp: sum_rel_def split: sum.splits)
    4.16 +lemmas sum_rel_eq[relator_eq] = sum.rel_eq
    4.17 +lemmas sum_rel_mono[relator_mono] = sum.rel_mono
    4.18  
    4.19  lemma sum_rel_OO[relator_distr]:
    4.20    "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
    4.21 -by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split)
    4.22 +  by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split)
    4.23  
    4.24  lemma Domainp_sum[relator_domain]:
    4.25    assumes "Domainp R1 = P1"
    4.26 @@ -94,4 +87,3 @@
    4.27  end
    4.28  
    4.29  end
    4.30 -
     5.1 --- a/src/HOL/Transfer.thy	Mon Jan 20 20:21:12 2014 +0100
     5.2 +++ b/src/HOL/Transfer.thy	Mon Jan 20 20:42:43 2014 +0100
     5.3 @@ -6,16 +6,11 @@
     5.4  header {* Generic theorem transfer using relations *}
     5.5  
     5.6  theory Transfer
     5.7 -imports Hilbert_Choice
     5.8 +imports Hilbert_Choice Basic_BNFs
     5.9  begin
    5.10  
    5.11  subsection {* Relator for function space *}
    5.12  
    5.13 -definition
    5.14 -  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
    5.15 -where
    5.16 -  "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
    5.17 -
    5.18  locale lifting_syntax
    5.19  begin
    5.20    notation fun_rel (infixr "===>" 55)
    5.21 @@ -26,32 +21,20 @@
    5.22  begin
    5.23  interpretation lifting_syntax .
    5.24  
    5.25 -lemma fun_relI [intro]:
    5.26 -  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
    5.27 -  shows "(A ===> B) f g"
    5.28 -  using assms by (simp add: fun_rel_def)
    5.29 -
    5.30 -lemma fun_relD:
    5.31 -  assumes "(A ===> B) f g" and "A x y"
    5.32 -  shows "B (f x) (g y)"
    5.33 -  using assms by (simp add: fun_rel_def)
    5.34 -
    5.35  lemma fun_relD2:
    5.36 -  assumes "(A ===> B) f g" and "A x x"
    5.37 +  assumes "fun_rel A B f g" and "A x x"
    5.38    shows "B (f x) (g x)"
    5.39 -  using assms unfolding fun_rel_def by auto
    5.40 +  using assms by (rule fun_relD)
    5.41  
    5.42  lemma fun_relE:
    5.43 -  assumes "(A ===> B) f g" and "A x y"
    5.44 +  assumes "fun_rel A B f g" and "A x y"
    5.45    obtains "B (f x) (g y)"
    5.46    using assms by (simp add: fun_rel_def)
    5.47  
    5.48 -lemma fun_rel_eq:
    5.49 -  shows "((op =) ===> (op =)) = (op =)"
    5.50 -  by (auto simp add: fun_eq_iff elim: fun_relE)
    5.51 +lemmas fun_rel_eq = fun.rel_eq
    5.52  
    5.53  lemma fun_rel_eq_rel:
    5.54 -  shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
    5.55 +shows "fun_rel (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
    5.56    by (simp add: fun_rel_def)
    5.57  
    5.58