introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
authorkuncar
Tue Aug 13 15:59:22 2013 +0200 (2013-08-13)
changeset 53011aeee0a4be6cf
parent 53010 ec5e6f69bd65
child 53012 cb82606b8215
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
src/HOL/Lifting.thy
src/HOL/Quotient.thy
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Lifting.thy	Tue Aug 13 15:59:22 2013 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Tue Aug 13 15:59:22 2013 +0200
     1.3 @@ -16,7 +16,9 @@
     1.4  
     1.5  subsection {* Function map *}
     1.6  
     1.7 -notation map_fun (infixr "--->" 55)
     1.8 +context
     1.9 +begin
    1.10 +interpretation lifting_syntax .
    1.11  
    1.12  lemma map_fun_id:
    1.13    "(id ---> id) = id"
    1.14 @@ -599,6 +601,8 @@
    1.15    shows "Domainp T = P"
    1.16  by (simp add: invariant_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
    1.17  
    1.18 +end
    1.19 +
    1.20  subsection {* ML setup *}
    1.21  
    1.22  ML_file "Tools/Lifting/lifting_util.ML"
     2.1 --- a/src/HOL/Quotient.thy	Tue Aug 13 15:59:22 2013 +0200
     2.2 +++ b/src/HOL/Quotient.thy	Tue Aug 13 15:59:22 2013 +0200
     2.3 @@ -28,6 +28,10 @@
     2.4    shows "((op =) OOO R) = R"
     2.5    by (auto simp add: fun_eq_iff)
     2.6  
     2.7 +context
     2.8 +begin
     2.9 +interpretation lifting_syntax .
    2.10 +
    2.11  subsection {* Quotient Predicate *}
    2.12  
    2.13  definition
    2.14 @@ -578,6 +582,7 @@
    2.15    shows "(Rep ---> Abs) id = id"
    2.16    by (simp add: fun_eq_iff Quotient3_abs_rep [OF a])
    2.17  
    2.18 +end
    2.19  
    2.20  locale quot_type =
    2.21    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.22 @@ -812,10 +817,15 @@
    2.23  lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
    2.24    by (simp add: Quot_True_def)
    2.25  
    2.26 +context 
    2.27 +begin
    2.28 +interpretation lifting_syntax .
    2.29  
    2.30  text {* Tactics for proving the lifted theorems *}
    2.31  ML_file "Tools/Quotient/quotient_tacs.ML"
    2.32  
    2.33 +end
    2.34 +
    2.35  subsection {* Methods / Interface *}
    2.36  
    2.37  method_setup lifting =
    2.38 @@ -862,9 +872,7 @@
    2.39    {* lift theorems to quotient types *}
    2.40  
    2.41  no_notation
    2.42 -  rel_conj (infixr "OOO" 75) and
    2.43 -  map_fun (infixr "--->" 55) and
    2.44 -  fun_rel (infixr "===>" 55)
    2.45 +  rel_conj (infixr "OOO" 75)
    2.46  
    2.47  end
    2.48  
     3.1 --- a/src/HOL/Transfer.thy	Tue Aug 13 15:59:22 2013 +0200
     3.2 +++ b/src/HOL/Transfer.thy	Tue Aug 13 15:59:22 2013 +0200
     3.3 @@ -12,10 +12,20 @@
     3.4  subsection {* Relator for function space *}
     3.5  
     3.6  definition
     3.7 -  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
     3.8 +  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
     3.9  where
    3.10    "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
    3.11  
    3.12 +locale lifting_syntax
    3.13 +begin
    3.14 +  notation fun_rel (infixr "===>" 55)
    3.15 +  notation map_fun (infixr "--->" 55)
    3.16 +end
    3.17 +
    3.18 +context
    3.19 +begin
    3.20 +interpretation lifting_syntax .
    3.21 +
    3.22  lemma fun_relI [intro]:
    3.23    assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
    3.24    shows "(A ===> B) f g"
    3.25 @@ -112,6 +122,8 @@
    3.26    shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
    3.27    using assms unfolding Rel_def fun_rel_def by fast
    3.28  
    3.29 +end
    3.30 +
    3.31  ML_file "Tools/transfer.ML"
    3.32  setup Transfer.setup
    3.33  
    3.34 @@ -121,6 +133,10 @@
    3.35  
    3.36  hide_const (open) Rel
    3.37  
    3.38 +context
    3.39 +begin
    3.40 +interpretation lifting_syntax .
    3.41 +
    3.42  text {* Handling of domains *}
    3.43  
    3.44  lemma Domaimp_refl[transfer_domain_rule]:
    3.45 @@ -358,3 +374,5 @@
    3.46    unfolding transfer_forall_def by (rule All_transfer)
    3.47  
    3.48  end
    3.49 +
    3.50 +end