src/HOL/IMP/Abs_Int1_parity.thy

 "plus_parity x Either  = Either"
 
 text{* First we instantiate the abstract value interface and prove that the
 functions on type @{typ parity} have all the necessary properties: *}
 
-interpretation Val_semilattice
+permanent_interpretation Val_semilattice
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof txt{* of the locale axioms *}
   fix a b :: parity
   assume "a \<le> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
     by(auto simp: less_eq_parity_def)

 
 text{* Instantiating the abstract interpretation locale requires no more
 proofs (they happened in the instatiation above) but delivers the
 instantiated abstract interpreter which we call @{text AI_parity}: *}
 
-interpretation Abs_Int
+permanent_interpretation Abs_Int
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 defines aval_parity is aval' and step_parity is step' and AI_parity is AI
 ..
 
 

 value "show_acom (the(AI_parity test2_parity))"
 
 
 subsubsection "Termination"
 
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof
   case goal1 thus ?case
     by(induction a1 a2 rule: plus_parity.induct)
       (auto simp add:less_eq_parity_def)
 qed
 
 definition m_parity :: "parity \<Rightarrow> nat" where
 "m_parity x = (if x = Either then 0 else 1)"
 
-interpretation Abs_Int_measure
+permanent_interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 and m = m_parity and h = "1"
 proof
   case goal1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
 next