--- a/src/HOL/ex/LocaleTest2.thy Fri Dec 12 14:23:49 2008 +0100
+++ b/src/HOL/ex/LocaleTest2.thy Fri Dec 12 14:26:35 2008 +0100
@@ -469,13 +469,13 @@
subsubsection {* Total order @{text "<="} on @{typ int} *}
-interpretation int: dpo ["op <= :: [int, int] => bool"]
+interpretation int: dpo "op <= :: [int, int] => bool"
where "(dpo.less (op <=) (x::int) y) = (x < y)"
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
show "dpo (op <= :: [int, int] => bool)"
proof qed auto
- then interpret int: dpo ["op <= :: [int, int] => bool"] .
+ then interpret int: dpo "op <= :: [int, int] => bool" .
txt {* Gives interpreted version of @{text less_def} (without condition). *}
show "(dpo.less (op <=) (x::int) y) = (x < y)"
by (unfold int.less_def) auto
@@ -488,7 +488,7 @@
lemma "(op < :: [int, int] => bool) = op <"
apply (rule int.abs_test) done
-interpretation int: dlat ["op <= :: [int, int] => bool"]
+interpretation int: dlat "op <= :: [int, int] => bool"
where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
and join_eq: "dlat.join (op <=) (x::int) y = max x y"
proof -
@@ -497,7 +497,7 @@
apply (unfold int.is_inf_def int.is_sup_def)
apply arith+
done
- then interpret int: dlat ["op <= :: [int, int] => bool"] .
+ then interpret int: dlat "op <= :: [int, int] => bool" .
txt {* Interpretation to ease use of definitions, which are
conditional in general but unconditional after interpretation. *}
show "dlat.meet (op <=) (x::int) y = min x y"
@@ -512,7 +512,7 @@
by auto
qed
-interpretation int: dlo ["op <= :: [int, int] => bool"]
+interpretation int: dlo "op <= :: [int, int] => bool"
proof qed arith
text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -525,13 +525,13 @@
subsubsection {* Total order @{text "<="} on @{typ nat} *}
-interpretation nat: dpo ["op <= :: [nat, nat] => bool"]
+interpretation nat: dpo "op <= :: [nat, nat] => bool"
where "dpo.less (op <=) (x::nat) y = (x < y)"
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
show "dpo (op <= :: [nat, nat] => bool)"
proof qed auto
- then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
+ then interpret nat: dpo "op <= :: [nat, nat] => bool" .
txt {* Gives interpreted version of @{text less_def} (without condition). *}
show "dpo.less (op <=) (x::nat) y = (x < y)"
apply (unfold nat.less_def)
@@ -539,7 +539,7 @@
done
qed
-interpretation nat: dlat ["op <= :: [nat, nat] => bool"]
+interpretation nat: dlat "op <= :: [nat, nat] => bool"
where "dlat.meet (op <=) (x::nat) y = min x y"
and "dlat.join (op <=) (x::nat) y = max x y"
proof -
@@ -548,7 +548,7 @@
apply (unfold nat.is_inf_def nat.is_sup_def)
apply arith+
done
- then interpret nat: dlat ["op <= :: [nat, nat] => bool"] .
+ then interpret nat: dlat "op <= :: [nat, nat] => bool" .
txt {* Interpretation to ease use of definitions, which are
conditional in general but unconditional after interpretation. *}
show "dlat.meet (op <=) (x::nat) y = min x y"
@@ -563,7 +563,7 @@
by auto
qed
-interpretation nat: dlo ["op <= :: [nat, nat] => bool"]
+interpretation nat: dlo "op <= :: [nat, nat] => bool"
proof qed arith
text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -576,13 +576,13 @@
subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
-interpretation nat_dvd: dpo ["op dvd :: [nat, nat] => bool"]
+interpretation nat_dvd: dpo "op dvd :: [nat, nat] => bool"
where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
show "dpo (op dvd :: [nat, nat] => bool)"
proof qed (auto simp: dvd_def)
- then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
+ then interpret nat_dvd: dpo "op dvd :: [nat, nat] => bool" .
txt {* Gives interpreted version of @{text less_def} (without condition). *}
show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
apply (unfold nat_dvd.less_def)
@@ -590,7 +590,7 @@
done
qed
-interpretation nat_dvd: dlat ["op dvd :: [nat, nat] => bool"]
+interpretation nat_dvd: dlat "op dvd :: [nat, nat] => bool"
where "dlat.meet (op dvd) (x::nat) y = gcd x y"
and "dlat.join (op dvd) (x::nat) y = lcm x y"
proof -
@@ -602,7 +602,7 @@
apply (rule_tac x = "lcm x y" in exI)
apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
done
- then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] .
+ then interpret nat_dvd: dlat "op dvd :: [nat, nat] => bool" .
txt {* Interpretation to ease use of definitions, which are
conditional in general but unconditional after interpretation. *}
show "dlat.meet (op dvd) (x::nat) y = gcd x y"
@@ -818,7 +818,8 @@
end
-locale Dhom = Dgrp prod (infixl "**" 65) one + Dgrp sum (infixl "+++" 60) zero +
+locale Dhom = prod: Dgrp prod one + sum: Dgrp sum zero
+ for prod (infixl "**" 65) and one and sum (infixl "+++" 60) and zero +
fixes hom
assumes hom_mult [simp]: "hom (x ** y) = hom x +++ hom y"
@@ -837,14 +838,14 @@
subsubsection {* Interpretation of Functions *}
-interpretation Dfun: Dmonoid ["op o" "id :: 'a => 'a"]
+interpretation Dfun: Dmonoid "op o" "id :: 'a => 'a"
where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
(* and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
proof -
show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc)
note Dmonoid = this
(*
- from this interpret Dmonoid ["op o" "id :: 'a => 'a"] .
+ from this interpret Dmonoid "op o" "id :: 'a => 'a" .
*)
show "Dmonoid.unit (op o) (id :: 'a => 'a) f = bij f"
apply (unfold Dmonoid.unit_def [OF Dmonoid])
@@ -887,7 +888,7 @@
"(f :: unit => unit) = id"
by rule simp
-interpretation Dfun: Dgrp ["op o" "id :: unit => unit"]
+interpretation Dfun: Dgrp "op o" "id :: unit => unit"
where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
proof -
have "Dmonoid op o (id :: 'a => 'a)" ..