--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu Jan 03 21:48:05 2019 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu Jan 03 22:19:19 2019 +0100
@@ -9,24 +9,24 @@
begin
typedecl int
-instance int :: "term" ..
+instance int :: \<open>term\<close> ..
-consts plus :: "int => int => int" (infixl \<open>+\<close> 60)
- zero :: int (\<open>0\<close>)
- minus :: "int => int" (\<open>- _\<close>)
+consts plus :: \<open>int => int => int\<close> (infixl \<open>+\<close> 60)
+ zero :: \<open>int\<close> (\<open>0\<close>)
+ minus :: \<open>int => int\<close> (\<open>- _\<close>)
axiomatization where
- int_assoc: "(x + y::int) + z = x + (y + z)" and
- int_zero: "0 + x = x" and
- int_minus: "(-x) + x = 0" and
- int_minus2: "-(-x) = x"
+ int_assoc: \<open>(x + y::int) + z = x + (y + z)\<close> and
+ int_zero: \<open>0 + x = x\<close> and
+ int_minus: \<open>(-x) + x = 0\<close> and
+ int_minus2: \<open>-(-x) = x\<close>
section \<open>Inference of parameter types\<close>
locale param1 = fixes p
print_locale! param1
-locale param2 = fixes p :: 'b
+locale param2 = fixes p :: \<open>'b\<close>
print_locale! param2
(*
@@ -37,7 +37,7 @@
locale param3 = fixes p (infix \<open>..\<close> 50)
print_locale! param3
-locale param4 = fixes p :: "'a => 'a => 'a" (infix \<open>..\<close> 50)
+locale param4 = fixes p :: \<open>'a => 'a => 'a\<close> (infix \<open>..\<close> 50)
print_locale! param4
@@ -45,13 +45,13 @@
locale constraint1 =
fixes prod (infixl \<open>**\<close> 65)
- assumes l_id: "x ** y = x"
- assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+ assumes l_id: \<open>x ** y = x\<close>
+ assumes assoc: \<open>(x ** y) ** z = x ** (y ** z)\<close>
print_locale! constraint1
locale constraint2 =
fixes p and q
- assumes "p = q"
+ assumes \<open>p = q\<close>
print_locale! constraint2
@@ -59,35 +59,35 @@
locale semi =
fixes prod (infixl \<open>**\<close> 65)
- assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+ assumes assoc: \<open>(x ** y) ** z = x ** (y ** z)\<close>
print_locale! semi thm semi_def
locale lgrp = semi +
fixes one and inv
- assumes lone: "one ** x = x"
- and linv: "inv(x) ** x = one"
+ assumes lone: \<open>one ** x = x\<close>
+ and linv: \<open>inv(x) ** x = one\<close>
print_locale! lgrp thm lgrp_def lgrp_axioms_def
-locale add_lgrp = semi "(++)" for sum (infixl \<open>++\<close> 60) +
+locale add_lgrp = semi \<open>(++)\<close> for sum (infixl \<open>++\<close> 60) +
fixes zero and neg
- assumes lzero: "zero ++ x = x"
- and lneg: "neg(x) ++ x = zero"
+ assumes lzero: \<open>zero ++ x = x\<close>
+ and lneg: \<open>neg(x) ++ x = zero\<close>
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
-locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl \<open>++\<close> 60)
+locale rev_lgrp = semi \<open>%x y. y ++ x\<close> for sum (infixl \<open>++\<close> 60)
print_locale! rev_lgrp thm rev_lgrp_def
-locale hom = f: semi f + g: semi g for f and g
+locale hom = f: semi \<open>f\<close> + g: semi \<open>g\<close> for f and g
print_locale! hom thm hom_def
-locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta
+locale perturbation = semi + d: semi \<open>%x y. delta(x) ** delta(y)\<close> for delta
print_locale! perturbation thm perturbation_def
-locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
+locale pert_hom = d1: perturbation \<open>f\<close> \<open>d1\<close> + d2: perturbation \<open>f\<close> \<open>d2\<close> for f d1 d2
print_locale! pert_hom thm pert_hom_def
text \<open>Alternative expression, obtaining nicer names in \<open>semi f\<close>.\<close>
-locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
+locale pert_hom' = semi \<open>f\<close> + d1: perturbation \<open>f\<close> \<open>d1\<close> + d2: perturbation \<open>f\<close> \<open>d2\<close> for f d1 d2
print_locale! pert_hom' thm pert_hom'_def
@@ -96,32 +96,32 @@
locale logic =
fixes land (infixl \<open>&&\<close> 55)
and lnot (\<open>-- _\<close> [60] 60)
- assumes assoc: "(x && y) && z = x && (y && z)"
- and notnot: "-- (-- x) = x"
+ assumes assoc: \<open>(x && y) && z = x && (y && z)\<close>
+ and notnot: \<open>-- (-- x) = x\<close>
begin
definition lor (infixl \<open>||\<close> 50) where
- "x || y = --(-- x && -- y)"
+ \<open>x || y = --(-- x && -- y)\<close>
end
print_locale! logic
-locale use_decl = l: logic + semi "(||)"
+locale use_decl = l: logic + semi \<open>(||)\<close>
print_locale! use_decl thm use_decl_def
locale extra_type =
- fixes a :: 'a
- and P :: "'a => 'b => o"
+ fixes a :: \<open>'a\<close>
+ and P :: \<open>'a => 'b => o\<close>
begin
-definition test :: "'a => o"
- where "test(x) \<longleftrightarrow> (\<forall>b. P(x, b))"
+definition test :: \<open>'a => o\<close>
+ where \<open>test(x) \<longleftrightarrow> (\<forall>b. P(x, b))\<close>
end
-term extra_type.test thm extra_type.test_def
+term \<open>extra_type.test\<close> thm extra_type.test_def
-interpretation var?: extra_type "0" "%x y. x = 0" .
+interpretation var?: extra_type \<open>0\<close> \<open>%x y. x = 0\<close> .
thm var.test_def
@@ -143,12 +143,12 @@
declare [[show_hyps]]
locale "syntax" =
- fixes p1 :: "'a => 'b"
- and p2 :: "'b => o"
+ fixes p1 :: \<open>'a => 'b\<close>
+ and p2 :: \<open>'b => o\<close>
begin
-definition d1 :: "'a => o" (\<open>D1'(_')\<close>) where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
-definition d2 :: "'b => o" (\<open>D2'(_')\<close>) where "d2(x) \<longleftrightarrow> \<not> p2(x)"
+definition d1 :: \<open>'a => o\<close> (\<open>D1'(_')\<close>) where \<open>d1(x) \<longleftrightarrow> \<not> p2(p1(x))\<close>
+definition d2 :: \<open>'b => o\<close> (\<open>D2'(_')\<close>) where \<open>d2(x) \<longleftrightarrow> \<not> p2(x)\<close>
thm d1_def d2_def
@@ -156,7 +156,7 @@
thm syntax.d1_def syntax.d2_def
-locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
+locale syntax' = "syntax" \<open>p1\<close> \<open>p2\<close> for p1 :: \<open>'a => 'a\<close> and p2 :: \<open>'a => o\<close>
begin
thm d1_def d2_def (* should print as "D1(?x) <-> ..." and "D2(?x) <-> ..." *)
@@ -168,7 +168,7 @@
end
-locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o"
+locale syntax'' = "syntax" \<open>p3\<close> \<open>p2\<close> for p3 :: \<open>'a => 'b\<close> and p2 :: \<open>'b => o\<close>
begin
thm d1_def d2_def
@@ -194,14 +194,14 @@
fixes land (infixl \<open>&&\<close> 55)
and lor (infixl \<open>||\<close> 50)
and lnot (\<open>-- _\<close> [60] 60)
- assumes assoc: "(x && y) && z = x && (y && z)"
- and notnot: "-- (-- x) = x"
- defines "x || y == --(-- x && -- y)"
+ assumes assoc: \<open>(x && y) && z = x && (y && z)\<close>
+ and notnot: \<open>-- (-- x) = x\<close>
+ defines \<open>x || y == --(-- x && -- y)\<close>
begin
thm lor_def
-lemma "x || y = --(-- x && --y)"
+lemma \<open>x || y = --(-- x && --y)\<close>
by (unfold lor_def) (rule refl)
end
@@ -211,7 +211,7 @@
locale logic_def2 = logic_def
begin
-lemma "x || y = --(-- x && --y)"
+lemma \<open>x || y = --(-- x && --y)\<close>
by (unfold lor_def) (rule refl)
end
@@ -222,56 +222,56 @@
(* A somewhat arcane homomorphism example *)
definition semi_hom where
- "semi_hom(prod, sum, h) \<longleftrightarrow> (\<forall>x y. h(prod(x, y)) = sum(h(x), h(y)))"
+ \<open>semi_hom(prod, sum, h) \<longleftrightarrow> (\<forall>x y. h(prod(x, y)) = sum(h(x), h(y)))\<close>
lemma semi_hom_mult:
- "semi_hom(prod, sum, h) \<Longrightarrow> h(prod(x, y)) = sum(h(x), h(y))"
+ \<open>semi_hom(prod, sum, h) \<Longrightarrow> h(prod(x, y)) = sum(h(x), h(y))\<close>
by (simp add: semi_hom_def)
-locale semi_hom_loc = prod: semi prod + sum: semi sum
+locale semi_hom_loc = prod: semi \<open>prod\<close> + sum: semi \<open>sum\<close>
for prod and sum and h +
- assumes semi_homh: "semi_hom(prod, sum, h)"
+ assumes semi_homh: \<open>semi_hom(prod, sum, h)\<close>
notes semi_hom_mult = semi_hom_mult [OF semi_homh]
thm semi_hom_loc.semi_hom_mult
(* unspecified, attribute not applied in backgroud theory !!! *)
-lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
+lemma (in semi_hom_loc) \<open>h(prod(x, y)) = sum(h(x), h(y))\<close>
by (rule semi_hom_mult)
(* Referring to facts from within a context specification *)
lemma
- assumes x: "P \<longleftrightarrow> P"
+ assumes x: \<open>P \<longleftrightarrow> P\<close>
notes y = x
- shows True ..
+ shows \<open>True\<close> ..
section \<open>Theorem statements\<close>
lemma (in lgrp) lcancel:
- "x ** y = x ** z \<longleftrightarrow> y = z"
+ \<open>x ** y = x ** z \<longleftrightarrow> y = z\<close>
proof
- assume "x ** y = x ** z"
- then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
- then show "y = z" by (simp add: lone linv)
+ assume \<open>x ** y = x ** z\<close>
+ then have \<open>inv(x) ** x ** y = inv(x) ** x ** z\<close> by (simp add: assoc)
+ then show \<open>y = z\<close> by (simp add: lone linv)
qed simp
print_locale! lgrp
locale rgrp = semi +
fixes one and inv
- assumes rone: "x ** one = x"
- and rinv: "x ** inv(x) = one"
+ assumes rone: \<open>x ** one = x\<close>
+ and rinv: \<open>x ** inv(x) = one\<close>
begin
lemma rcancel:
- "y ** x = z ** x \<longleftrightarrow> y = z"
+ \<open>y ** x = z ** x \<longleftrightarrow> y = z\<close>
proof
- assume "y ** x = z ** x"
- then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
+ assume \<open>y ** x = z ** x\<close>
+ then have \<open>y ** (x ** inv(x)) = z ** (x ** inv(x))\<close>
by (simp add: assoc [symmetric])
- then show "y = z" by (simp add: rone rinv)
+ then show \<open>y = z\<close> by (simp add: rone rinv)
qed simp
end
@@ -281,18 +281,18 @@
subsection \<open>Patterns\<close>
lemma (in rgrp)
- assumes "y ** x = z ** x" (is ?a)
- shows "y = z" (is ?t)
+ assumes \<open>y ** x = z ** x\<close> (is \<open>?a\<close>)
+ shows \<open>y = z\<close> (is \<open>?t\<close>)
proof -
txt \<open>Weird proof involving patterns from context element and conclusion.\<close>
{
- assume ?a
- then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
+ assume \<open>?a\<close>
+ then have \<open>y ** (x ** inv(x)) = z ** (x ** inv(x))\<close>
by (simp add: assoc [symmetric])
- then have ?t by (simp add: rone rinv)
+ then have \<open>?t\<close> by (simp add: rone rinv)
}
note x = this
- show ?t by (rule x [OF \<open>?a\<close>])
+ show \<open>?t\<close> by (rule x [OF \<open>?a\<close>])
qed
@@ -303,15 +303,15 @@
proof unfold_locales
{
fix x
- have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
- then show "x ** one = x" by (simp add: assoc lcancel)
+ have \<open>inv(x) ** x ** one = inv(x) ** x\<close> by (simp add: linv lone)
+ then show \<open>x ** one = x\<close> by (simp add: assoc lcancel)
}
note rone = this
{
fix x
- have "inv(x) ** x ** inv(x) = inv(x) ** one"
+ have \<open>inv(x) ** x ** inv(x) = inv(x) ** one\<close>
by (simp add: linv lone rone)
- then show "x ** inv(x) = one" by (simp add: assoc lcancel)
+ then show \<open>x ** inv(x) = one\<close> by (simp add: assoc lcancel)
}
qed
@@ -322,7 +322,7 @@
(* use of derived theorem *)
lemma (in lgrp)
- "y ** x = z ** x \<longleftrightarrow> y = z"
+ \<open>y ** x = z ** x \<longleftrightarrow> y = z\<close>
apply (rule rcancel)
done
@@ -332,15 +332,15 @@
proof unfold_locales
{
fix x
- have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
- then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
+ have \<open>one ** (x ** inv(x)) = x ** inv(x)\<close> by (simp add: rinv rone)
+ then show \<open>one ** x = x\<close> by (simp add: assoc [symmetric] rcancel)
}
note lone = this
{
fix x
- have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
+ have \<open>inv(x) ** (x ** inv(x)) = one ** inv(x)\<close>
by (simp add: rinv lone rone)
- then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
+ then show \<open>inv(x) ** x = one\<close> by (simp add: assoc [symmetric] rcancel)
}
qed
@@ -353,30 +353,30 @@
(* Duality *)
locale order =
- fixes less :: "'a => 'a => o" (infix \<open><<\<close> 50)
- assumes refl: "x << x"
- and trans: "[| x << y; y << z |] ==> x << z"
+ fixes less :: \<open>'a => 'a => o\<close> (infix \<open><<\<close> 50)
+ assumes refl: \<open>x << x\<close>
+ and trans: \<open>[| x << y; y << z |] ==> x << z\<close>
-sublocale order < dual: order "%x y. y << x"
+sublocale order < dual: order \<open>%x y. y << x\<close>
apply unfold_locales apply (rule refl) apply (blast intro: trans)
done
print_locale! order (* Only two instances of order. *)
locale order' =
- fixes less :: "'a => 'a => o" (infix \<open><<\<close> 50)
- assumes refl: "x << x"
- and trans: "[| x << y; y << z |] ==> x << z"
+ fixes less :: \<open>'a => 'a => o\<close> (infix \<open><<\<close> 50)
+ assumes refl: \<open>x << x\<close>
+ and trans: \<open>[| x << y; y << z |] ==> x << z\<close>
locale order_with_def = order'
begin
-definition greater :: "'a => 'a => o" (infix \<open>>>\<close> 50) where
- "x >> y \<longleftrightarrow> y << x"
+definition greater :: \<open>'a => 'a => o\<close> (infix \<open>>>\<close> 50) where
+ \<open>x >> y \<longleftrightarrow> y << x\<close>
end
-sublocale order_with_def < dual: order' "(>>)"
+sublocale order_with_def < dual: order' \<open>(>>)\<close>
apply unfold_locales
unfolding greater_def
apply (rule refl) apply (blast intro: trans)
@@ -392,17 +392,17 @@
locale A5 =
fixes A and B and C and D and E
- assumes eq: "A \<longleftrightarrow> B \<longleftrightarrow> C \<longleftrightarrow> D \<longleftrightarrow> E"
+ assumes eq: \<open>A \<longleftrightarrow> B \<longleftrightarrow> C \<longleftrightarrow> D \<longleftrightarrow> E\<close>
-sublocale A5 < 1: A5 _ _ D E C
+sublocale A5 < 1: A5 _ _ \<open>D\<close> \<open>E\<close> \<open>C\<close>
print_facts
using eq apply (blast intro: A5.intro) done
-sublocale A5 < 2: A5 C _ E _ A
+sublocale A5 < 2: A5 \<open>C\<close> _ \<open>E\<close> _ \<open>A\<close>
print_facts
using eq apply (blast intro: A5.intro) done
-sublocale A5 < 3: A5 B C A _ _
+sublocale A5 < 3: A5 \<open>B\<close> \<open>C\<close> \<open>A\<close> _ _
print_facts
using eq apply (blast intro: A5.intro) done
@@ -414,25 +414,25 @@
(* Free arguments of instance *)
locale trivial =
- fixes P and Q :: o
- assumes Q: "P \<longleftrightarrow> P \<longleftrightarrow> Q"
+ fixes P and Q :: \<open>o\<close>
+ assumes Q: \<open>P \<longleftrightarrow> P \<longleftrightarrow> Q\<close>
begin
-lemma Q_triv: "Q" using Q by fast
+lemma Q_triv: \<open>Q\<close> using Q by fast
end
-sublocale trivial < x: trivial x _
+sublocale trivial < x: trivial \<open>x\<close> _
apply unfold_locales using Q by fast
print_locale! trivial
context trivial
begin
-thm x.Q [where ?x = True]
+thm x.Q [where ?x = \<open>True\<close>]
end
-sublocale trivial < y: trivial Q Q
+sublocale trivial < y: trivial \<open>Q\<close> \<open>Q\<close>
by unfold_locales
(* Succeeds since previous interpretation is more general. *)
@@ -441,13 +441,13 @@
subsection \<open>Sublocale, then interpretation in theory\<close>
-interpretation int?: lgrp "(+)" "0" "minus"
+interpretation int?: lgrp \<open>(+)\<close> \<open>0\<close> \<open>minus\<close>
proof unfold_locales
qed (rule int_assoc int_zero int_minus)+
thm int.assoc int.semi_axioms
-interpretation int2?: semi "(+)"
+interpretation int2?: semi \<open>(+)\<close>
by unfold_locales (* subsumed, thm int2.assoc not generated *)
ML \<open>(Global_Theory.get_thms @{theory} "int2.assoc";
@@ -460,18 +460,18 @@
subsection \<open>Interpretation in theory, then sublocale\<close>
-interpretation fol: logic "(+)" "minus"
+interpretation fol: logic \<open>(+)\<close> \<open>minus\<close>
by unfold_locales (rule int_assoc int_minus2)+
locale logic2 =
fixes land (infixl \<open>&&\<close> 55)
and lnot (\<open>-- _\<close> [60] 60)
- assumes assoc: "(x && y) && z = x && (y && z)"
- and notnot: "-- (-- x) = x"
+ assumes assoc: \<open>(x && y) && z = x && (y && z)\<close>
+ and notnot: \<open>-- (-- x) = x\<close>
begin
definition lor (infixl \<open>||\<close> 50) where
- "x || y = --(-- x && -- y)"
+ \<open>x || y = --(-- x && -- y)\<close>
end
@@ -497,59 +497,59 @@
locale logic_o =
fixes land (infixl \<open>&&\<close> 55)
and lnot (\<open>-- _\<close> [60] 60)
- assumes assoc_o: "(x && y) && z \<longleftrightarrow> x && (y && z)"
- and notnot_o: "-- (-- x) \<longleftrightarrow> x"
+ assumes assoc_o: \<open>(x && y) && z \<longleftrightarrow> x && (y && z)\<close>
+ and notnot_o: \<open>-- (-- x) \<longleftrightarrow> x\<close>
begin
definition lor_o (infixl \<open>||\<close> 50) where
- "x || y \<longleftrightarrow> --(-- x && -- y)"
+ \<open>x || y \<longleftrightarrow> --(-- x && -- y)\<close>
end
-interpretation x: logic_o "(\<and>)" "Not"
- rewrites bool_logic_o: "x.lor_o(x, y) \<longleftrightarrow> x \<or> y"
+interpretation x: logic_o \<open>(\<and>)\<close> \<open>Not\<close>
+ rewrites bool_logic_o: \<open>x.lor_o(x, y) \<longleftrightarrow> x \<or> y\<close>
proof -
- show bool_logic_o: "PROP logic_o((\<and>), Not)" by unfold_locales fast+
- show "logic_o.lor_o((\<and>), Not, x, y) \<longleftrightarrow> x \<or> y"
+ show bool_logic_o: \<open>PROP logic_o((\<and>), Not)\<close> by unfold_locales fast+
+ show \<open>logic_o.lor_o((\<and>), Not, x, y) \<longleftrightarrow> x \<or> y\<close>
by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
qed
thm x.lor_o_def bool_logic_o
-lemma lor_triv: "z \<longleftrightarrow> z" ..
+lemma lor_triv: \<open>z \<longleftrightarrow> z\<close> ..
-lemma (in logic_o) lor_triv: "x || y \<longleftrightarrow> x || y" by fast
+lemma (in logic_o) lor_triv: \<open>x || y \<longleftrightarrow> x || y\<close> by fast
-thm lor_triv [where z = True] (* Check strict prefix. *)
+thm lor_triv [where z = \<open>True\<close>] (* Check strict prefix. *)
x.lor_triv
subsection \<open>Rewrite morphisms in expressions\<close>
-interpretation y: logic_o "(\<or>)" "Not" rewrites bool_logic_o2: "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y"
+interpretation y: logic_o \<open>(\<or>)\<close> \<open>Not\<close> rewrites bool_logic_o2: \<open>logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y\<close>
proof -
- show bool_logic_o: "PROP logic_o((\<or>), Not)" by unfold_locales fast+
- show "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y" unfolding logic_o.lor_o_def [OF bool_logic_o] by fast
+ show bool_logic_o: \<open>PROP logic_o((\<or>), Not)\<close> by unfold_locales fast+
+ show \<open>logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y\<close> unfolding logic_o.lor_o_def [OF bool_logic_o] by fast
qed
subsection \<open>Inheritance of rewrite morphisms\<close>
locale reflexive =
- fixes le :: "'a => 'a => o" (infix \<open>\<sqsubseteq>\<close> 50)
- assumes refl: "x \<sqsubseteq> x"
+ fixes le :: \<open>'a => 'a => o\<close> (infix \<open>\<sqsubseteq>\<close> 50)
+ assumes refl: \<open>x \<sqsubseteq> x\<close>
begin
-definition less (infix \<open>\<sqsubset>\<close> 50) where "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
+definition less (infix \<open>\<sqsubset>\<close> 50) where \<open>x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y\<close>
end
axiomatization
- gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and
- gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o"
+ gle :: \<open>'a => 'a => o\<close> and gless :: \<open>'a => 'a => o\<close> and
+ gle' :: \<open>'a => 'a => o\<close> and gless' :: \<open>'a => 'a => o\<close>
where
- grefl: "gle(x, x)" and gless_def: "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" and
- grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y"
+ grefl: \<open>gle(x, x)\<close> and gless_def: \<open>gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y\<close> and
+ grefl': \<open>gle'(x, x)\<close> and gless'_def: \<open>gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y\<close>
text \<open>Setup\<close>
@@ -558,11 +558,11 @@
lemmas less_thm = less_def
end
-interpretation le: mixin gle rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+interpretation le: mixin \<open>gle\<close> rewrites \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)\<close>
proof -
- show "mixin(gle)" by unfold_locales (rule grefl)
+ show \<open>mixin(gle)\<close> by unfold_locales (rule grefl)
note reflexive = this[unfolded mixin_def]
- show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+ show \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)\<close>
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
@@ -573,11 +573,11 @@
lemmas less_thm2 = less_def
end
-interpretation le: mixin2 gle
+interpretation le: mixin2 \<open>gle\<close>
by unfold_locales
thm le.less_thm2 (* rewrite morphism applied *)
-lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
+lemma \<open>gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y\<close>
by (rule le.less_thm2)
text \<open>Rewrite morphism does not leak to a side branch.\<close>
@@ -587,11 +587,11 @@
lemmas less_thm3 = less_def
end
-interpretation le: mixin3 gle
+interpretation le: mixin3 \<open>gle\<close>
by unfold_locales
thm le.less_thm3 (* rewrite morphism not applied *)
-lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" by (rule le.less_thm3)
+lemma \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y\<close> by (rule le.less_thm3)
text \<open>Rewrite morphism only available in original context\<close>
@@ -599,12 +599,12 @@
locale mixin4_mixin = mixin4_base
-interpretation le: mixin4_mixin gle
- rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+interpretation le: mixin4_mixin \<open>gle\<close>
+ rewrites \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)\<close>
proof -
- show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
+ show \<open>mixin4_mixin(gle)\<close> by unfold_locales (rule grefl)
note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
- show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+ show \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)\<close>
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
@@ -613,16 +613,16 @@
lemmas less_thm4 = less_def
end
-locale mixin4_combined = le1?: mixin4_mixin le' + le2?: mixin4_copy le for le' le
+locale mixin4_combined = le1?: mixin4_mixin \<open>le'\<close> + le2?: mixin4_copy \<open>le\<close> for le' le
begin
lemmas less_thm4' = less_def
end
-interpretation le4: mixin4_combined gle' gle
+interpretation le4: mixin4_combined \<open>gle'\<close> \<open>gle\<close>
by unfold_locales (rule grefl')
thm le4.less_thm4' (* rewrite morphism not applied *)
-lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
+lemma \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y\<close>
by (rule le4.less_thm4')
text \<open>Inherited rewrite morphism applied to new theorem\<close>
@@ -631,22 +631,22 @@
locale mixin5_inherited = mixin5_base
-interpretation le5: mixin5_base gle
- rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+interpretation le5: mixin5_base \<open>gle\<close>
+ rewrites \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)\<close>
proof -
- show "mixin5_base(gle)" by unfold_locales
+ show \<open>mixin5_base(gle)\<close> by unfold_locales
note reflexive = this[unfolded mixin5_base_def mixin_def]
- show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+ show \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)\<close>
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
-interpretation le5: mixin5_inherited gle
+interpretation le5: mixin5_inherited \<open>gle\<close>
by unfold_locales
lemmas (in mixin5_inherited) less_thm5 = less_def
thm le5.less_thm5 (* rewrite morphism applied *)
-lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
+lemma \<open>gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y\<close>
by (rule le5.less_thm5)
text \<open>Rewrite morphism pushed down to existing inherited locale\<close>
@@ -655,23 +655,23 @@
locale mixin6_inherited = mixin5_base
-interpretation le6: mixin6_base gle
+interpretation le6: mixin6_base \<open>gle\<close>
by unfold_locales
-interpretation le6: mixin6_inherited gle
+interpretation le6: mixin6_inherited \<open>gle\<close>
by unfold_locales
-interpretation le6: mixin6_base gle
- rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+interpretation le6: mixin6_base \<open>gle\<close>
+ rewrites \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)\<close>
proof -
- show "mixin6_base(gle)" by unfold_locales
+ show \<open>mixin6_base(gle)\<close> by unfold_locales
note reflexive = this[unfolded mixin6_base_def mixin_def]
- show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+ show \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)\<close>
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
lemmas (in mixin6_inherited) less_thm6 = less_def
thm le6.less_thm6 (* mixin applied *)
-lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
+lemma \<open>gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y\<close>
by (rule le6.less_thm6)
text \<open>Existing rewrite morphism inherited through sublocale relation\<close>
@@ -680,22 +680,22 @@
locale mixin7_inherited = reflexive
-interpretation le7: mixin7_base gle
- rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+interpretation le7: mixin7_base \<open>gle\<close>
+ rewrites \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)\<close>
proof -
- show "mixin7_base(gle)" by unfold_locales
+ show \<open>mixin7_base(gle)\<close> by unfold_locales
note reflexive = this[unfolded mixin7_base_def mixin_def]
- show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+ show \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)\<close>
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
-interpretation le7: mixin7_inherited gle
+interpretation le7: mixin7_inherited \<open>gle\<close>
by unfold_locales
lemmas (in mixin7_inherited) less_thm7 = less_def
thm le7.less_thm7 (* before, rewrite morphism not applied *)
-lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
+lemma \<open>reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y\<close>
by (rule le7.less_thm7)
sublocale mixin7_inherited < mixin7_base
@@ -704,13 +704,13 @@
lemmas (in mixin7_inherited) less_thm7b = less_def
thm le7.less_thm7b (* after, mixin applied *)
-lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
+lemma \<open>gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y\<close>
by (rule le7.less_thm7b)
text \<open>This locale will be interpreted in later theories.\<close>
-locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le'
+locale mixin_thy_merge = le: reflexive \<open>le\<close> + le': reflexive \<open>le'\<close> for le le'
subsection \<open>Rewrite morphisms in sublocale\<close>
@@ -720,37 +720,37 @@
selection operator.\<close>
axiomatization glob_one and glob_inv
- where glob_lone: "prod(glob_one(prod), x) = x"
- and glob_linv: "prod(glob_inv(prod, x), x) = glob_one(prod)"
+ where glob_lone: \<open>prod(glob_one(prod), x) = x\<close>
+ and glob_linv: \<open>prod(glob_inv(prod, x), x) = glob_one(prod)\<close>
locale dgrp = semi
begin
-definition one where "one = glob_one(prod)"
+definition one where \<open>one = glob_one(prod)\<close>
-lemma lone: "one ** x = x"
+lemma lone: \<open>one ** x = x\<close>
unfolding one_def by (rule glob_lone)
-definition inv where "inv(x) = glob_inv(prod, x)"
+definition inv where \<open>inv(x) = glob_inv(prod, x)\<close>
-lemma linv: "inv(x) ** x = one"
+lemma linv: \<open>inv(x) ** x = one\<close>
unfolding one_def inv_def by (rule glob_linv)
end
sublocale lgrp < def?: dgrp
- rewrites one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
+ rewrites one_equation: \<open>dgrp.one(prod) = one\<close> and inv_equation: \<open>dgrp.inv(prod, x) = inv(x)\<close>
proof -
- show "dgrp(prod)" by unfold_locales
+ show \<open>dgrp(prod)\<close> by unfold_locales
from this interpret d: dgrp .
\<comment> \<open>Unit\<close>
- have "dgrp.one(prod) = glob_one(prod)" by (rule d.one_def)
- also have "... = glob_one(prod) ** one" by (simp add: rone)
- also have "... = one" by (simp add: glob_lone)
- finally show "dgrp.one(prod) = one" .
+ have \<open>dgrp.one(prod) = glob_one(prod)\<close> by (rule d.one_def)
+ also have \<open>... = glob_one(prod) ** one\<close> by (simp add: rone)
+ also have \<open>... = one\<close> by (simp add: glob_lone)
+ finally show \<open>dgrp.one(prod) = one\<close> .
\<comment> \<open>Inverse\<close>
- then have "dgrp.inv(prod, x) ** x = inv(x) ** x" by (simp add: glob_linv d.linv linv)
- then show "dgrp.inv(prod, x) = inv(x)" by (simp add: rcancel)
+ then have \<open>dgrp.inv(prod, x) ** x = inv(x) ** x\<close> by (simp add: glob_linv d.linv linv)
+ then show \<open>dgrp.inv(prod, x) = inv(x)\<close> by (simp add: rcancel)
qed
print_locale! lgrp
@@ -760,35 +760,35 @@
text \<open>Equations stored in target\<close>
-lemma "dgrp.one(prod) = one" by (rule one_equation)
-lemma "dgrp.inv(prod, x) = inv(x)" by (rule inv_equation)
+lemma \<open>dgrp.one(prod) = one\<close> by (rule one_equation)
+lemma \<open>dgrp.inv(prod, x) = inv(x)\<close> by (rule inv_equation)
text \<open>Rewrite morphisms applied\<close>
-lemma "one = glob_one(prod)" by (rule one_def)
-lemma "inv(x) = glob_inv(prod, x)" by (rule inv_def)
+lemma \<open>one = glob_one(prod)\<close> by (rule one_def)
+lemma \<open>inv(x) = glob_inv(prod, x)\<close> by (rule inv_def)
end
text \<open>Interpreted versions\<close>
-lemma "0 = glob_one ((+))" by (rule int.def.one_def)
-lemma "- x = glob_inv((+), x)" by (rule int.def.inv_def)
+lemma \<open>0 = glob_one ((+))\<close> by (rule int.def.one_def)
+lemma \<open>- x = glob_inv((+), x)\<close> by (rule int.def.inv_def)
text \<open>Roundup applies rewrite morphisms at declaration level in DFS tree\<close>
-locale roundup = fixes x assumes true: "x \<longleftrightarrow> True"
+locale roundup = fixes x assumes true: \<open>x \<longleftrightarrow> True\<close>
-sublocale roundup \<subseteq> sub: roundup x rewrites "x \<longleftrightarrow> True \<and> True"
+sublocale roundup \<subseteq> sub: roundup \<open>x\<close> rewrites \<open>x \<longleftrightarrow> True \<and> True\<close>
apply unfold_locales apply (simp add: true) done
-lemma (in roundup) "True \<and> True \<longleftrightarrow> True" by (rule sub.true)
+lemma (in roundup) \<open>True \<and> True \<longleftrightarrow> True\<close> by (rule sub.true)
section \<open>Interpretation in named contexts\<close>
locale container
begin
-interpretation "private": roundup True by unfold_locales rule
+interpretation "private": roundup \<open>True\<close> by unfold_locales rule
lemmas true_copy = private.true
end
@@ -806,39 +806,39 @@
notepad
begin
- interpret "local": lgrp "(+)" "0" "minus"
+ interpret "local": lgrp \<open>(+)\<close> \<open>0\<close> \<open>minus\<close>
by unfold_locales (* subsumed *)
{
- fix zero :: int
- assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
- then interpret local_fixed: lgrp "(+)" zero "minus"
+ fix zero :: \<open>int\<close>
+ assume \<open>!!x. zero + x = x\<close> \<open>!!x. (-x) + x = zero\<close>
+ then interpret local_fixed: lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close>
by unfold_locales
thm local_fixed.lone
- print_dependencies! lgrp "(+)" 0 minus + lgrp "(+)" zero minus
+ print_dependencies! lgrp \<open>(+)\<close> \<open>0\<close> \<open>minus\<close> + lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close>
}
- assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
- then interpret local_free: lgrp "(+)" zero "minus" for zero
+ assume \<open>!!x zero. zero + x = x\<close> \<open>!!x zero. (-x) + x = zero\<close>
+ then interpret local_free: lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close> for zero
by unfold_locales
- thm local_free.lone [where ?zero = 0]
+ thm local_free.lone [where ?zero = \<open>0\<close>]
end
notepad
begin
{
fix pand and pnot and por
- assume passoc: "\<And>x y z. pand(pand(x, y), z) \<longleftrightarrow> pand(x, pand(y, z))"
- and pnotnot: "\<And>x. pnot(pnot(x)) \<longleftrightarrow> x"
- and por_def: "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))"
- interpret loc: logic_o pand pnot
- rewrites por_eq: "\<And>x y. logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)" (* FIXME *)
+ assume passoc: \<open>\<And>x y z. pand(pand(x, y), z) \<longleftrightarrow> pand(x, pand(y, z))\<close>
+ and pnotnot: \<open>\<And>x. pnot(pnot(x)) \<longleftrightarrow> x\<close>
+ and por_def: \<open>\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))\<close>
+ interpret loc: logic_o \<open>pand\<close> \<open>pnot\<close>
+ rewrites por_eq: \<open>\<And>x y. logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)\<close> (* FIXME *)
proof -
- show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
+ show logic_o: \<open>PROP logic_o(pand, pnot)\<close> using passoc pnotnot by unfold_locales
fix x y
- show "logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)"
+ show \<open>logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)\<close>
by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
qed
print_interps logic_o
- have "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
+ have \<open>\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))\<close> by (rule loc.lor_o_def)
}
end