# HG changeset patch
# User ballarin
# Date 1229436552 -3600
# Node ID 2d62b637fa8034f804fccd4aa5bbe3d4ab0c195c
# Parent  60f7fb56f8cd64081be199e5aa098d6d68a294f3
More porting to new locales.

diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -321,7 +321,7 @@
   ss <[r] merges f qs ss \<or> 
   merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w" (is "PROP ?P")
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P" apply(insert semilat)
     apply (unfold lesssub_def)
     apply (simp (no_asm_simp) add: merges_incr)
@@ -351,7 +351,7 @@
    (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
   (is "PROP ?P")
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P" apply(insert semilat)
 apply (unfold iter_def stables_def)
 apply (rule_tac P = "%(ss,w).
@@ -457,7 +457,7 @@
                  kildall r f step ss0 <=[r] ts)"
   (is "PROP ?P")
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P"
 apply (unfold kildall_def)
 apply(case_tac "iter f step ss0 (unstables r step ss0)")
@@ -474,7 +474,7 @@
   \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
   (is "PROP ?P")
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P"
 apply(unfold is_bcv_def wt_step_def)
 apply(insert semilat kildall_properties[of A])
diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -197,7 +197,7 @@
   have "merge c pc ?step (c!Suc pc) =
     (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
     then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
-    else \<top>)" unfolding merge_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
+    else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
   moreover {
     fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
     with less have "s' <=_r \<phi>!pc'" by auto
diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -380,7 +380,7 @@
 lemma Listn_sl_aux:
 assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))"
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
 show ?thesis
 apply (unfold Listn.sl_def)
 apply (simp (no_asm) only: semilat_Def split_conv)
diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/MicroJava/BV/SemilatAlg.thy
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -67,7 +67,7 @@
 lemma plusplus_closed: assumes "semilat (A, r, f)" shows
   "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A" (is "PROP ?P")
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P" proof (induct x)
     show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
     fix y x xs
@@ -164,7 +164,7 @@
   shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> 
   \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y" 
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
 
   let "b <=_r ?map ++_f y" = ?thesis
 
diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/Statespace/StateSpaceEx.thy
--- a/src/HOL/Statespace/StateSpaceEx.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -37,7 +37,7 @@
 projection~/ injection functions that convert from abstract values to
 @{typ "nat"} and @{text "bool"}. The logical content of the locale is: *}
 
-locale vars' =
+class_locale vars' =
   fixes n::'name and b::'name
   assumes "distinct [n, b]" 
 
@@ -204,7 +204,7 @@
   assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
   shows True
 proof
-  interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
+  class_interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
   term "s<a := i>\<cdot>a = i"
 qed
 
diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/Statespace/StateSpaceLocale.thy
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -16,7 +16,7 @@
 concrete values.*}
 
 
-locale project_inject =
+class_locale project_inject =
  fixes project :: "'value \<Rightarrow> 'a"
  and   "inject":: "'a \<Rightarrow> 'value"
  assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/Word/WordArith.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -22,7 +22,7 @@
 proof
 qed (unfold word_sle_def word_sless_def, auto)
 
-interpretation signed: linorder ["word_sle" "word_sless"] 
+class_interpretation signed: linorder ["word_sle" "word_sless"] 
   by (rule signed_linorder)
 
 lemmas word_arith_wis = 
@@ -858,11 +858,11 @@
 lemmas td_ext_unat = refl [THEN td_ext_unat']
 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard]
 
-interpretation word_unat:
-  td_ext ["unat::'a::len word => nat" 
-          of_nat 
-          "unats (len_of TYPE('a::len))"
-          "%i. i mod 2 ^ len_of TYPE('a::len)"]
+interpretation word_unat!:
+  td_ext "unat::'a::len word => nat" 
+         of_nat 
+         "unats (len_of TYPE('a::len))"
+         "%i. i mod 2 ^ len_of TYPE('a::len)"
   by (rule td_ext_unat)
 
 lemmas td_unat = word_unat.td_thm
diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -344,11 +344,11 @@
 
 lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size]
 
-interpretation test_bit:
-  td_ext ["op !! :: 'a::len0 word => nat => bool"
-          set_bits
-          "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
-          "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"]
+interpretation test_bit!:
+  td_ext "op !! :: 'a::len0 word => nat => bool"
+         set_bits
+         "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
+         "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
   by (rule td_ext_nth)
 
 declare test_bit.Rep' [simp del]
diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/Word/WordDefinition.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -423,19 +423,19 @@
    and interpretations do not produce thm duplicates. I.e. 
    we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
    because the latter is the same thm as the former *)
-interpretation word_sint:
-  td_ext ["sint ::'a::len word => int" 
+interpretation word_sint!:
+  td_ext "sint ::'a::len word => int" 
           word_of_int 
           "sints (len_of TYPE('a::len))"
           "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -
-               2 ^ (len_of TYPE('a::len) - 1)"]
+               2 ^ (len_of TYPE('a::len) - 1)"
   by (rule td_ext_sint)
 
-interpretation word_sbin:
-  td_ext ["sint ::'a::len word => int" 
+interpretation word_sbin!:
+  td_ext "sint ::'a::len word => int" 
           word_of_int 
           "sints (len_of TYPE('a::len))"
-          "sbintrunc (len_of TYPE('a::len) - 1)"]
+          "sbintrunc (len_of TYPE('a::len) - 1)"
   by (rule td_ext_sbin)
 
 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm, standard]
@@ -635,10 +635,10 @@
   apply simp
   done
 
-interpretation word_bl:
-  type_definition ["to_bl :: 'a::len0 word => bool list"
-                   of_bl  
-                   "{bl. length bl = len_of TYPE('a::len0)}"]
+interpretation word_bl!:
+  type_definition "to_bl :: 'a::len0 word => bool list"
+                  of_bl  
+                  "{bl. length bl = len_of TYPE('a::len0)}"
   by (rule td_bl)
 
 lemma word_size_bl: "size w == size (to_bl w)"
diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/Word/WordGenLib.thy
--- a/src/HOL/Word/WordGenLib.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/Word/WordGenLib.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -107,16 +107,16 @@
   apply (rule word_or_not)
   done
 
-interpretation word_bool_alg:
-  boolean ["op AND" "op OR" bitNOT 0 max_word]
+interpretation word_bool_alg!:
+  boolean "op AND" "op OR" bitNOT 0 max_word
   by (rule word_boolean)
 
 lemma word_xor_and_or:
   "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
 
-interpretation word_bool_alg:
-  boolean_xor ["op AND" "op OR" bitNOT 0 max_word "op XOR"]
+interpretation word_bool_alg!:
+  boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
   apply (rule boolean_xor.intro)
    apply (rule word_boolean)
   apply (rule boolean_xor_axioms.intro)
@@ -363,7 +363,7 @@
    apply (erule contrapos_pn, simp)
    apply (drule arg_cong[where f=of_nat])
    apply simp
-   apply (subst (asm) word_unat.Rep_Abs_A.Rep_inverse[of n])
+   apply (subst (asm) word_unat.Rep_inverse[of n])
    apply simp
   apply simp
   done