src/HOL/Transfer.thy

 (*  Title:      HOL/Transfer.thy
     Author:     Brian Huffman, TU Muenchen
     Author:     Ondrej Kuncar, TU Muenchen
 *)
 
-section {* Generic theorem transfer using relations *}
+section \<open>Generic theorem transfer using relations\<close>
 
 theory Transfer
 imports Basic_BNF_LFPs Hilbert_Choice Metis
 begin
 
-subsection {* Relator for function space *}
+subsection \<open>Relator for function space\<close>
 
 locale lifting_syntax
 begin
   notation rel_fun (infixr "===>" 55)
   notation map_fun (infixr "--->" 55)

 lemma rel_fun_eq_rel:
 shows "rel_fun (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
   by (simp add: rel_fun_def)
 
 
-subsection {* Transfer method *}
-
-text {* Explicit tag for relation membership allows for
-  backward proof methods. *}
+subsection \<open>Transfer method\<close>
+
+text \<open>Explicit tag for relation membership allows for
+  backward proof methods.\<close>
 
 definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   where "Rel r \<equiv> r"
 
-text {* Handling of equality relations *}
+text \<open>Handling of equality relations\<close>
 
 definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   where "is_equality R \<longleftrightarrow> R = (op =)"
 
 lemma is_equality_eq: "is_equality (op =)"
   unfolding is_equality_def by simp
 
-text {* Reverse implication for monotonicity rules *}
+text \<open>Reverse implication for monotonicity rules\<close>
 
 definition rev_implies where
   "rev_implies x y \<longleftrightarrow> (y \<longrightarrow> x)"
 
-text {* Handling of meta-logic connectives *}
+text \<open>Handling of meta-logic connectives\<close>
 
 definition transfer_forall where
   "transfer_forall \<equiv> All"
 
 definition transfer_implies where

 lemma Rel_abs:
   assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
   shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
   using assms unfolding Rel_def rel_fun_def by fast
 
-subsection {* Predicates on relations, i.e. ``class constraints'' *}
+subsection \<open>Predicates on relations, i.e. ``class constraints''\<close>
 
 definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
 
 definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"

 lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R"
 unfolding bi_unique_alt_def ..
 
 end
 
-subsection {* Equality restricted by a predicate *}
+subsection \<open>Equality restricted by a predicate\<close>
 
 definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
 
 lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id"

 
 context
 begin
 interpretation lifting_syntax .
 
-text {* Handling of domains *}
+text \<open>Handling of domains\<close>
 
 lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
   by auto
 
 lemma Domainp_refl[transfer_domain_rule]:

 
 lemma Domainp_prod_fun_eq[relator_domain]:
   "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
 by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
 
-text {* Properties are preserved by relation composition. *}
+text \<open>Properties are preserved by relation composition.\<close>
 
 lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"
   by auto
 
 lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)"

 
 lemma left_unique_OO: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
 unfolding left_unique_def OO_def by blast
 
 
-subsection {* Properties of relators *}
+subsection \<open>Properties of relators\<close>
 
 lemma left_total_eq[transfer_rule]: "left_total op="
   unfolding left_total_def by blast
 
 lemma left_unique_eq[transfer_rule]: "left_unique op="

 ML_file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
 
 declare pred_fun_def [simp]
 declare rel_fun_eq [relator_eq]
 
-subsection {* Transfer rules *}
+subsection \<open>Transfer rules\<close>
 
 context
 begin
 interpretation lifting_syntax .
 

     (transfer_bforall (Domainp A)) transfer_forall"
   using assms unfolding right_total_def
   unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff
   by fast
 
-text {* Transfer rules using implication instead of equality on booleans. *}
+text \<open>Transfer rules using implication instead of equality on booleans.\<close>
 
 lemma transfer_forall_transfer [transfer_rule]:
   "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
   "right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall"
   "right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall"

 
 lemma eq_imp_transfer [transfer_rule]:
   "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
   unfolding right_unique_alt_def2 .
 
-text {* Transfer rules using equality. *}
+text \<open>Transfer rules using equality.\<close>
 
 lemma left_unique_transfer [transfer_rule]:
   assumes "right_total A"
   assumes "right_total B"
   assumes "bi_unique A"

   {
     assume "R\<^sup>*\<^sup>* x y" "A y y'"
     thus "R'\<^sup>*\<^sup>* x' y'"
     proof(induction arbitrary: y')
       case base
-      with `bi_unique A` `A x x'` have "x' = y'" by(rule bi_uniqueDr)
+      with \<open>bi_unique A\<close> \<open>A x x'\<close> have "x' = y'" by(rule bi_uniqueDr)
       thus ?case by simp
     next
       case (step y z z')
-      from `bi_total A` obtain y' where "A y y'" unfolding bi_total_def by blast
+      from \<open>bi_total A\<close> obtain y' where "A y y'" unfolding bi_total_def by blast
       hence "R'\<^sup>*\<^sup>* x' y'" by(rule step.IH)
-      moreover from R `A y y'` `A z z'` `R y z`
+      moreover from R \<open>A y y'\<close> \<open>A z z'\<close> \<open>R y z\<close>
       have "R' y' z'" by(auto dest: rel_funD)
       ultimately show ?case ..
     qed
   next
     assume "R'\<^sup>*\<^sup>* x' y'" "A y y'"
     thus "R\<^sup>*\<^sup>* x y"
     proof(induction arbitrary: y)
       case base
-      with `bi_unique A` `A x x'` have "x = y" by(rule bi_uniqueDl)
+      with \<open>bi_unique A\<close> \<open>A x x'\<close> have "x = y" by(rule bi_uniqueDl)
       thus ?case by simp
     next
       case (step y' z' z)
-      from `bi_total A` obtain y where "A y y'" unfolding bi_total_def by blast
+      from \<open>bi_total A\<close> obtain y where "A y y'" unfolding bi_total_def by blast
       hence "R\<^sup>*\<^sup>* x y" by(rule step.IH)
-      moreover from R `A y y'` `A z z'` `R' y' z'`
+      moreover from R \<open>A y y'\<close> \<open>A z z'\<close> \<open>R' y' z'\<close>
       have "R y z" by(auto dest: rel_funD)
       ultimately show ?case ..
     qed
   }
 qed