# HG changeset patch # User ballarin # Date 1229088395 -3600 # Node ID fcc9606fe14139c2ad95b58f66a1168cce006919 # Parent cfea1f3719b316801ac78147e1ca69daffa50591 Ported to new locales. diff -r cfea1f3719b3 -r fcc9606fe141 src/HOL/ex/LocaleTest2.thy --- 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)" ..