src/HOL/IMP/Abs_Int2_ivl.thy

 
 lemma add_mono_Fin_le:
   "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
 by(drule (1) add_mono) simp
 
-interpretation Val_abs
+interpretation Val_semilattice
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 proof
   case goal1 thus ?case by transfer (simp add: le_iff_subset)
 next
   case goal2 show ?case by transfer (simp add: \<gamma>_rep_def)

     apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le)
     by(auto simp: empty_rep_def is_empty_rep_def)
 qed
 
 
-interpretation Val_abs1_gamma
+interpretation Val_lattice_gamma
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 defines aval_ivl is aval'
 proof
   case goal1 show ?case by(simp add: \<gamma>_inf)
 next
   case goal2 show ?case unfolding bot_ivl_def by transfer simp
 qed
 
-interpretation Val_abs1
+interpretation Val_inv
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
 proof
   case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def)

       uminus_ivl.abs_eq uminus_rep_def \<gamma>_ivl_nice)
     apply(simp add: \<gamma>_aboveI[of i2] \<gamma>_belowI[of i1])
     done
 qed
 
-interpretation Abs_Int1
+interpretation Abs_Int_inv
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
 defines inv_aval_ivl is inv_aval''
 and inv_bval_ivl is inv_bval''

 lemma mono_below: "iv1 \<le> iv2 \<Longrightarrow> below iv1 \<le> below iv2"
 apply transfer
 apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split)
 by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
 
-interpretation Abs_Int1_mono
+interpretation Abs_Int_inv_mono
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
 proof
   case goal1 thus ?case by (rule mono_plus_ivl)