More porting to new locales.
--- 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])
--- 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
--- 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)
--- 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
--- 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
--- 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"
--- 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
--- 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]
--- 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)"
--- 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