src/HOL/Transfer.thy
changeset 58182 82478e6c60cb
parent 58128 43a1ba26a8cb
child 58386 6999f55645ea
     1.1 --- a/src/HOL/Transfer.thy	Thu Sep 04 09:02:43 2014 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Thu Sep 04 11:20:59 2014 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  imports Hilbert_Choice Metis Option
     1.5  begin
     1.6  
     1.7 -(* We include Option here although it's not needed here. 
     1.8 -   By doing this, we avoid a diamond problem for BNF and 
     1.9 +(* We import Option here although it's not needed here.
    1.10 +   By doing this, we avoid a diamond problem for BNF and
    1.11     FP sugar interpretation defined in this file. *)
    1.12  
    1.13  subsection {* Relator for function space *}
    1.14 @@ -227,18 +227,18 @@
    1.15  
    1.16  subsection {* Equality restricted by a predicate *}
    1.17  
    1.18 -definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
    1.19 +definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.20    where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
    1.21  
    1.22 -lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id" 
    1.23 -unfolding eq_onp_def Grp_def by auto 
    1.24 +lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id"
    1.25 +unfolding eq_onp_def Grp_def by auto
    1.26  
    1.27  lemma eq_onp_to_eq:
    1.28    assumes "eq_onp P x y"
    1.29    shows "x = y"
    1.30  using assms by (simp add: eq_onp_def)
    1.31  
    1.32 -lemma eq_onp_top_eq_eq: "eq_onp top = op=" 
    1.33 +lemma eq_onp_top_eq_eq: "eq_onp top = op="
    1.34  by (simp add: eq_onp_def)
    1.35  
    1.36  lemma eq_onp_same_args:
    1.37 @@ -298,10 +298,10 @@
    1.38  
    1.39  subsection {* Properties of relators *}
    1.40  
    1.41 -lemma left_total_eq[transfer_rule]: "left_total op=" 
    1.42 +lemma left_total_eq[transfer_rule]: "left_total op="
    1.43    unfolding left_total_def by blast
    1.44  
    1.45 -lemma left_unique_eq[transfer_rule]: "left_unique op=" 
    1.46 +lemma left_unique_eq[transfer_rule]: "left_unique op="
    1.47    unfolding left_unique_def by blast
    1.48  
    1.49  lemma right_total_eq [transfer_rule]: "right_total op="
    1.50 @@ -366,7 +366,7 @@
    1.51  
    1.52  end
    1.53  
    1.54 -ML_file "Tools/Transfer/transfer_bnf.ML" 
    1.55 +ML_file "Tools/Transfer/transfer_bnf.ML"
    1.56  
    1.57  declare pred_fun_def [simp]
    1.58  declare rel_fun_eq [relator_eq]
    1.59 @@ -486,13 +486,13 @@
    1.60    shows "((A ===> B) ===> op=) mono mono"
    1.61  unfolding mono_def[abs_def] by transfer_prover
    1.62  
    1.63 -lemma right_total_relcompp_transfer[transfer_rule]: 
    1.64 +lemma right_total_relcompp_transfer[transfer_rule]:
    1.65    assumes [transfer_rule]: "right_total B"
    1.66 -  shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) 
    1.67 +  shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=)
    1.68      (\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO"
    1.69  unfolding OO_def[abs_def] by transfer_prover
    1.70  
    1.71 -lemma relcompp_transfer[transfer_rule]: 
    1.72 +lemma relcompp_transfer[transfer_rule]:
    1.73    assumes [transfer_rule]: "bi_total B"
    1.74    shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO"
    1.75  unfolding OO_def[abs_def] by transfer_prover
    1.76 @@ -507,13 +507,13 @@
    1.77    shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp"
    1.78  unfolding Domainp_iff[abs_def] by transfer_prover
    1.79  
    1.80 -lemma reflp_transfer[transfer_rule]: 
    1.81 +lemma reflp_transfer[transfer_rule]:
    1.82    "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp"
    1.83    "right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp"
    1.84    "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
    1.85    "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
    1.86    "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
    1.87 -using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def 
    1.88 +using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
    1.89  by fast+
    1.90  
    1.91  lemma right_unique_transfer [transfer_rule]: