src/HOL/ex/LocaleTest2.thy
author ballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223 e09c53289830
parent 28823 dcbef866c9e2
child 29226 fcc9606fe141
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
     1 (*  Title:      HOL/ex/LocaleTest2.thy
     2     ID:         $Id$
     3     Author:     Clemens Ballarin
     4     Copyright (c) 2007 by Clemens Ballarin
     5 
     6 More regression tests for locales.
     7 Definitions are less natural in FOL, since there is no selection operator.
     8 Hence we do them here in HOL, not in the main test suite for locales,
     9 which is FOL/ex/LocaleTest.thy
    10 *)
    11 
    12 header {* Test of Locale Interpretation *}
    13 
    14 theory LocaleTest2
    15 imports Main GCD
    16 begin
    17 
    18 section {* Interpretation of Defined Concepts *}
    19 
    20 text {* Naming convention for global objects: prefixes D and d *}
    21 
    22 
    23 subsection {* Lattices *}
    24 
    25 text {* Much of the lattice proofs are from HOL/Lattice. *}
    26 
    27 
    28 subsubsection {* Definitions *}
    29 
    30 locale dpo =
    31   fixes le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>" 50)
    32   assumes refl [intro, simp]: "x \<sqsubseteq> x"
    33     and anti_sym [intro]: "[| x \<sqsubseteq> y; y \<sqsubseteq> x |] ==> x = y"
    34     and trans [trans]: "[| x \<sqsubseteq> y; y \<sqsubseteq> z |] ==> x \<sqsubseteq> z"
    35 
    36 begin
    37 
    38 theorem circular:
    39   "[| x \<sqsubseteq> y; y \<sqsubseteq> z; z \<sqsubseteq> x |] ==> x = y & y = z"
    40   by (blast intro: trans)
    41 
    42 definition
    43   less :: "['a, 'a] => bool" (infixl "\<sqsubset>" 50)
    44   where "(x \<sqsubset> y) = (x \<sqsubseteq> y & x ~= y)"
    45 
    46 theorem abs_test:
    47   "op \<sqsubset> = (%x y. x \<sqsubset> y)"
    48   by simp
    49 
    50 definition
    51   is_inf :: "['a, 'a, 'a] => bool"
    52   where "is_inf x y i = (i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))"
    53 
    54 definition
    55   is_sup :: "['a, 'a, 'a] => bool"
    56   where "is_sup x y s = (x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z))"
    57 
    58 end
    59 
    60 locale dlat = dpo +
    61   assumes ex_inf: "EX inf. dpo.is_inf le x y inf"
    62     and ex_sup: "EX sup. dpo.is_sup le x y sup"
    63 
    64 begin
    65 
    66 definition
    67   meet :: "['a, 'a] => 'a" (infixl "\<sqinter>" 70)
    68   where "x \<sqinter> y = (THE inf. is_inf x y inf)"
    69 
    70 definition
    71   join :: "['a, 'a] => 'a" (infixl "\<squnion>" 65)
    72   where "x \<squnion> y = (THE sup. is_sup x y sup)"
    73 
    74 lemma is_infI [intro?]: "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow>
    75     (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> is_inf x y i"
    76   by (unfold is_inf_def) blast
    77 
    78 lemma is_inf_lower [elim?]:
    79   "is_inf x y i \<Longrightarrow> (i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C"
    80   by (unfold is_inf_def) blast
    81 
    82 lemma is_inf_greatest [elim?]:
    83     "is_inf x y i \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i"
    84   by (unfold is_inf_def) blast
    85 
    86 theorem is_inf_uniq: "is_inf x y i \<Longrightarrow> is_inf x y i' \<Longrightarrow> i = i'"
    87 proof -
    88   assume inf: "is_inf x y i"
    89   assume inf': "is_inf x y i'"
    90   show ?thesis
    91   proof (rule anti_sym)
    92     from inf' show "i \<sqsubseteq> i'"
    93     proof (rule is_inf_greatest)
    94       from inf show "i \<sqsubseteq> x" ..
    95       from inf show "i \<sqsubseteq> y" ..
    96     qed
    97     from inf show "i' \<sqsubseteq> i"
    98     proof (rule is_inf_greatest)
    99       from inf' show "i' \<sqsubseteq> x" ..
   100       from inf' show "i' \<sqsubseteq> y" ..
   101     qed
   102   qed
   103 qed
   104 
   105 theorem is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
   106 proof -
   107   assume "x \<sqsubseteq> y"
   108   show ?thesis
   109   proof
   110     show "x \<sqsubseteq> x" ..
   111     show "x \<sqsubseteq> y" by fact
   112     fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact
   113   qed
   114 qed
   115 
   116 lemma meet_equality [elim?]: "is_inf x y i \<Longrightarrow> x \<sqinter> y = i"
   117 proof (unfold meet_def)
   118   assume "is_inf x y i"
   119   then show "(THE i. is_inf x y i) = i"
   120     by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y i`])
   121 qed
   122 
   123 lemma meetI [intro?]:
   124     "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> x \<sqinter> y = i"
   125   by (rule meet_equality, rule is_infI) blast+
   126 
   127 lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
   128 proof (unfold meet_def)
   129   from ex_inf obtain i where "is_inf x y i" ..
   130   then show "is_inf x y (THE i. is_inf x y i)"
   131     by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y i`])
   132 qed
   133 
   134 lemma meet_left [intro?]:
   135   "x \<sqinter> y \<sqsubseteq> x"
   136   by (rule is_inf_lower) (rule is_inf_meet)
   137 
   138 lemma meet_right [intro?]:
   139   "x \<sqinter> y \<sqsubseteq> y"
   140   by (rule is_inf_lower) (rule is_inf_meet)
   141 
   142 lemma meet_le [intro?]:
   143   "[| z \<sqsubseteq> x; z \<sqsubseteq> y |] ==> z \<sqsubseteq> x \<sqinter> y"
   144   by (rule is_inf_greatest) (rule is_inf_meet)
   145 
   146 lemma is_supI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
   147     (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> is_sup x y s"
   148   by (unfold is_sup_def) blast
   149 
   150 lemma is_sup_least [elim?]:
   151     "is_sup x y s \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z"
   152   by (unfold is_sup_def) blast
   153 
   154 lemma is_sup_upper [elim?]:
   155     "is_sup x y s \<Longrightarrow> (x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> C) \<Longrightarrow> C"
   156   by (unfold is_sup_def) blast
   157 
   158 theorem is_sup_uniq: "is_sup x y s \<Longrightarrow> is_sup x y s' \<Longrightarrow> s = s'"
   159 proof -
   160   assume sup: "is_sup x y s"
   161   assume sup': "is_sup x y s'"
   162   show ?thesis
   163   proof (rule anti_sym)
   164     from sup show "s \<sqsubseteq> s'"
   165     proof (rule is_sup_least)
   166       from sup' show "x \<sqsubseteq> s'" ..
   167       from sup' show "y \<sqsubseteq> s'" ..
   168     qed
   169     from sup' show "s' \<sqsubseteq> s"
   170     proof (rule is_sup_least)
   171       from sup show "x \<sqsubseteq> s" ..
   172       from sup show "y \<sqsubseteq> s" ..
   173     qed
   174   qed
   175 qed
   176 
   177 theorem is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y"
   178 proof -
   179   assume "x \<sqsubseteq> y"
   180   show ?thesis
   181   proof
   182     show "x \<sqsubseteq> y" by fact
   183     show "y \<sqsubseteq> y" ..
   184     fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
   185     show "y \<sqsubseteq> z" by fact
   186   qed
   187 qed
   188 
   189 lemma join_equality [elim?]: "is_sup x y s \<Longrightarrow> x \<squnion> y = s"
   190 proof (unfold join_def)
   191   assume "is_sup x y s"
   192   then show "(THE s. is_sup x y s) = s"
   193     by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y s`])
   194 qed
   195 
   196 lemma joinI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
   197     (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = s"
   198   by (rule join_equality, rule is_supI) blast+
   199 
   200 lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
   201 proof (unfold join_def)
   202   from ex_sup obtain s where "is_sup x y s" ..
   203   then show "is_sup x y (THE s. is_sup x y s)"
   204     by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y s`])
   205 qed
   206 
   207 lemma join_left [intro?]:
   208   "x \<sqsubseteq> x \<squnion> y"
   209   by (rule is_sup_upper) (rule is_sup_join)
   210 
   211 lemma join_right [intro?]:
   212   "y \<sqsubseteq> x \<squnion> y"
   213   by (rule is_sup_upper) (rule is_sup_join)
   214 
   215 lemma join_le [intro?]:
   216   "[| x \<sqsubseteq> z; y \<sqsubseteq> z |] ==> x \<squnion> y \<sqsubseteq> z"
   217   by (rule is_sup_least) (rule is_sup_join)
   218 
   219 theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   220 proof (rule meetI)
   221   show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
   222   proof
   223     show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
   224     show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
   225     proof -
   226       have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
   227       also have "\<dots> \<sqsubseteq> y" ..
   228       finally show ?thesis .
   229     qed
   230   qed
   231   show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
   232   proof -
   233     have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
   234     also have "\<dots> \<sqsubseteq> z" ..
   235     finally show ?thesis .
   236   qed
   237   fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
   238   show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
   239   proof
   240     show "w \<sqsubseteq> x"
   241     proof -
   242       have "w \<sqsubseteq> x \<sqinter> y" by fact
   243       also have "\<dots> \<sqsubseteq> x" ..
   244       finally show ?thesis .
   245     qed
   246     show "w \<sqsubseteq> y \<sqinter> z"
   247     proof
   248       show "w \<sqsubseteq> y"
   249       proof -
   250         have "w \<sqsubseteq> x \<sqinter> y" by fact
   251         also have "\<dots> \<sqsubseteq> y" ..
   252         finally show ?thesis .
   253       qed
   254       show "w \<sqsubseteq> z" by fact
   255     qed
   256   qed
   257 qed
   258 
   259 theorem meet_commute: "x \<sqinter> y = y \<sqinter> x"
   260 proof (rule meetI)
   261   show "y \<sqinter> x \<sqsubseteq> x" ..
   262   show "y \<sqinter> x \<sqsubseteq> y" ..
   263   fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
   264   then show "z \<sqsubseteq> y \<sqinter> x" ..
   265 qed
   266 
   267 theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
   268 proof (rule meetI)
   269   show "x \<sqsubseteq> x" ..
   270   show "x \<sqsubseteq> x \<squnion> y" ..
   271   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
   272   show "z \<sqsubseteq> x" by fact
   273 qed
   274 
   275 theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   276 proof (rule joinI)
   277   show "x \<squnion> y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
   278   proof
   279     show "x \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
   280     show "y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
   281     proof -
   282       have "y \<sqsubseteq> y \<squnion> z" ..
   283       also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
   284       finally show ?thesis .
   285     qed
   286   qed
   287   show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)"
   288   proof -
   289     have "z \<sqsubseteq> y \<squnion> z"  ..
   290     also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
   291     finally show ?thesis .
   292   qed
   293   fix w assume "x \<squnion> y \<sqsubseteq> w" and "z \<sqsubseteq> w"
   294   show "x \<squnion> (y \<squnion> z) \<sqsubseteq> w"
   295   proof
   296     show "x \<sqsubseteq> w"
   297     proof -
   298       have "x \<sqsubseteq> x \<squnion> y" ..
   299       also have "\<dots> \<sqsubseteq> w" by fact
   300       finally show ?thesis .
   301     qed
   302     show "y \<squnion> z \<sqsubseteq> w"
   303     proof
   304       show "y \<sqsubseteq> w"
   305       proof -
   306 	have "y \<sqsubseteq> x \<squnion> y" ..
   307 	also have "... \<sqsubseteq> w" by fact
   308         finally show ?thesis .
   309       qed
   310       show "z \<sqsubseteq> w" by fact
   311     qed
   312   qed
   313 qed
   314 
   315 theorem join_commute: "x \<squnion> y = y \<squnion> x"
   316 proof (rule joinI)
   317   show "x \<sqsubseteq> y \<squnion> x" ..
   318   show "y \<sqsubseteq> y \<squnion> x" ..
   319   fix z assume "y \<sqsubseteq> z" and "x \<sqsubseteq> z"
   320   then show "y \<squnion> x \<sqsubseteq> z" ..
   321 qed
   322 
   323 theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
   324 proof (rule joinI)
   325   show "x \<sqsubseteq> x" ..
   326   show "x \<sqinter> y \<sqsubseteq> x" ..
   327   fix z assume "x \<sqsubseteq> z" and "x \<sqinter> y \<sqsubseteq> z"
   328   show "x \<sqsubseteq> z" by fact
   329 qed
   330 
   331 theorem meet_idem: "x \<sqinter> x = x"
   332 proof -
   333   have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
   334   also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
   335   finally show ?thesis .
   336 qed
   337 
   338 theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   339 proof (rule meetI)
   340   assume "x \<sqsubseteq> y"
   341   show "x \<sqsubseteq> x" ..
   342   show "x \<sqsubseteq> y" by fact
   343   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
   344   show "z \<sqsubseteq> x" by fact
   345 qed
   346 
   347 theorem meet_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   348   by (drule meet_related) (simp add: meet_commute)
   349 
   350 theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   351 proof (rule joinI)
   352   assume "x \<sqsubseteq> y"
   353   show "y \<sqsubseteq> y" ..
   354   show "x \<sqsubseteq> y" by fact
   355   fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
   356   show "y \<sqsubseteq> z" by fact
   357 qed
   358 
   359 theorem join_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   360   by (drule join_related) (simp add: join_commute)
   361 
   362 
   363 text {* Additional theorems *}
   364 
   365 theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
   366 proof
   367   assume "x \<sqsubseteq> y"
   368   then have "is_inf x y x" ..
   369   then show "x \<sqinter> y = x" ..
   370 next
   371   have "x \<sqinter> y \<sqsubseteq> y" ..
   372   also assume "x \<sqinter> y = x"
   373   finally show "x \<sqsubseteq> y" .
   374 qed
   375 
   376 theorem meet_connection2: "(x \<sqsubseteq> y) = (y \<sqinter> x = x)"
   377   using meet_commute meet_connection by simp
   378 
   379 theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
   380 proof
   381   assume "x \<sqsubseteq> y"
   382   then have "is_sup x y y" ..
   383   then show "x \<squnion> y = y" ..
   384 next
   385   have "x \<sqsubseteq> x \<squnion> y" ..
   386   also assume "x \<squnion> y = y"
   387   finally show "x \<sqsubseteq> y" .
   388 qed
   389 
   390 theorem join_connection2: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
   391   using join_commute join_connection by simp
   392 
   393 
   394 text {* Naming according to Jacobson I, p.\ 459. *}
   395 
   396 lemmas L1 = join_commute meet_commute
   397 lemmas L2 = join_assoc meet_assoc
   398 (*lemmas L3 = join_idem meet_idem*)
   399 lemmas L4 = join_meet_absorb meet_join_absorb
   400 
   401 end
   402 
   403 locale ddlat = dlat +
   404   assumes meet_distr:
   405     "dlat.meet le x (dlat.join le y z) =
   406     dlat.join le (dlat.meet le x y) (dlat.meet le x z)"
   407 
   408 begin
   409 
   410 lemma join_distr:
   411   "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   412   txt {* Jacobson I, p.\ 462 *}
   413 proof -
   414   have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by (simp add: L4)
   415   also have "... = x \<squnion> ((x \<sqinter> z) \<squnion> (y \<sqinter> z))" by (simp add: L2)
   416   also have "... = x \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 meet_distr)
   417   also have "... = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 L4)
   418   also have "... = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by (simp add: meet_distr)
   419   finally show ?thesis .
   420 qed
   421 
   422 end
   423 
   424 locale dlo = dpo +
   425   assumes total: "x \<sqsubseteq> y | y \<sqsubseteq> x"
   426 
   427 begin
   428 
   429 lemma less_total: "x \<sqsubset> y | x = y | y \<sqsubset> x"
   430   using total
   431   by (unfold less_def) blast
   432 
   433 end
   434 
   435 
   436 sublocale dlo < dlat
   437 proof
   438   fix x y
   439   from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
   440   then show "EX inf. is_inf x y inf" by blast
   441 next
   442   fix x y
   443   from total have "is_sup x y (if x \<sqsubseteq> y then y else x)" by (auto simp: is_sup_def)
   444   then show "EX sup. is_sup x y sup" by blast
   445 qed
   446 
   447 sublocale dlo < ddlat
   448 proof
   449   fix x y z
   450   show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
   451     txt {* Jacobson I, p.\ 462 *}
   452   proof -
   453     { assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x"
   454       from c have "?l = y \<squnion> z"
   455 	by (metis c (*join_commute*) join_connection2 join_related2 (*meet_commute*) meet_connection meet_related2 total)
   456       also from c have "... = ?r" by (metis (*c*) (*join_commute*) meet_related2)
   457       finally have "?l = ?r" . }
   458     moreover
   459     { assume c: "x \<sqsubseteq> y | x \<sqsubseteq> z"
   460       from c have "?l = x"
   461 	by (metis (*anti_sym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans)
   462       also from c have "... = ?r"
   463 	by (metis join_commute join_related2 meet_connection meet_related2 total)
   464       finally have "?l = ?r" . }
   465     moreover note total
   466     ultimately show ?thesis by blast
   467   qed
   468 qed
   469 
   470 subsubsection {* Total order @{text "<="} on @{typ int} *}
   471 
   472 interpretation int: dpo ["op <= :: [int, int] => bool"]
   473   where "(dpo.less (op <=) (x::int) y) = (x < y)"
   474   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
   475 proof -
   476   show "dpo (op <= :: [int, int] => bool)"
   477     proof qed auto
   478   then interpret int: dpo ["op <= :: [int, int] => bool"] .
   479     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   480   show "(dpo.less (op <=) (x::int) y) = (x < y)"
   481     by (unfold int.less_def) auto
   482 qed
   483 
   484 thm int.circular
   485 lemma "\<lbrakk> (x::int) \<le> y; y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> x = y \<and> y = z"
   486   apply (rule int.circular) apply assumption apply assumption apply assumption done
   487 thm int.abs_test
   488 lemma "(op < :: [int, int] => bool) = op <"
   489   apply (rule int.abs_test) done
   490 
   491 interpretation int: dlat ["op <= :: [int, int] => bool"]
   492   where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
   493     and join_eq: "dlat.join (op <=) (x::int) y = max x y"
   494 proof -
   495   show "dlat (op <= :: [int, int] => bool)"
   496     apply unfold_locales
   497     apply (unfold int.is_inf_def int.is_sup_def)
   498     apply arith+
   499     done
   500   then interpret int: dlat ["op <= :: [int, int] => bool"] .
   501   txt {* Interpretation to ease use of definitions, which are
   502     conditional in general but unconditional after interpretation. *}
   503   show "dlat.meet (op <=) (x::int) y = min x y"
   504     apply (unfold int.meet_def)
   505     apply (rule the_equality)
   506     apply (unfold int.is_inf_def)
   507     by auto
   508   show "dlat.join (op <=) (x::int) y = max x y"
   509     apply (unfold int.join_def)
   510     apply (rule the_equality)
   511     apply (unfold int.is_sup_def)
   512     by auto
   513 qed
   514 
   515 interpretation int: dlo ["op <= :: [int, int] => bool"]
   516   proof qed arith
   517 
   518 text {* Interpreted theorems from the locales, involving defined terms. *}
   519 
   520 thm int.less_def text {* from dpo *}
   521 thm int.meet_left text {* from dlat *}
   522 thm int.meet_distr text {* from ddlat *}
   523 thm int.less_total text {* from dlo *}
   524 
   525 
   526 subsubsection {* Total order @{text "<="} on @{typ nat} *}
   527 
   528 interpretation nat: dpo ["op <= :: [nat, nat] => bool"]
   529   where "dpo.less (op <=) (x::nat) y = (x < y)"
   530   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
   531 proof -
   532   show "dpo (op <= :: [nat, nat] => bool)"
   533     proof qed auto
   534   then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
   535     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   536   show "dpo.less (op <=) (x::nat) y = (x < y)"
   537     apply (unfold nat.less_def)
   538     apply auto
   539     done
   540 qed
   541 
   542 interpretation nat: dlat ["op <= :: [nat, nat] => bool"]
   543   where "dlat.meet (op <=) (x::nat) y = min x y"
   544     and "dlat.join (op <=) (x::nat) y = max x y"
   545 proof -
   546   show "dlat (op <= :: [nat, nat] => bool)"
   547     apply unfold_locales
   548     apply (unfold nat.is_inf_def nat.is_sup_def)
   549     apply arith+
   550     done
   551   then interpret nat: dlat ["op <= :: [nat, nat] => bool"] .
   552   txt {* Interpretation to ease use of definitions, which are
   553     conditional in general but unconditional after interpretation. *}
   554   show "dlat.meet (op <=) (x::nat) y = min x y"
   555     apply (unfold nat.meet_def)
   556     apply (rule the_equality)
   557     apply (unfold nat.is_inf_def)
   558     by auto
   559   show "dlat.join (op <=) (x::nat) y = max x y"
   560     apply (unfold nat.join_def)
   561     apply (rule the_equality)
   562     apply (unfold nat.is_sup_def)
   563     by auto
   564 qed
   565 
   566 interpretation nat: dlo ["op <= :: [nat, nat] => bool"]
   567   proof qed arith
   568 
   569 text {* Interpreted theorems from the locales, involving defined terms. *}
   570 
   571 thm nat.less_def text {* from dpo *}
   572 thm nat.meet_left text {* from dlat *}
   573 thm nat.meet_distr text {* from ddlat *}
   574 thm nat.less_total text {* from ldo *}
   575 
   576 
   577 subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
   578 
   579 interpretation nat_dvd: dpo ["op dvd :: [nat, nat] => bool"]
   580   where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
   581   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
   582 proof -
   583   show "dpo (op dvd :: [nat, nat] => bool)"
   584     proof qed (auto simp: dvd_def)
   585   then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
   586     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   587   show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
   588     apply (unfold nat_dvd.less_def)
   589     apply auto
   590     done
   591 qed
   592 
   593 interpretation nat_dvd: dlat ["op dvd :: [nat, nat] => bool"]
   594   where "dlat.meet (op dvd) (x::nat) y = gcd x y"
   595     and "dlat.join (op dvd) (x::nat) y = lcm x y"
   596 proof -
   597   show "dlat (op dvd :: [nat, nat] => bool)"
   598     apply unfold_locales
   599     apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
   600     apply (rule_tac x = "gcd x y" in exI)
   601     apply auto [1]
   602     apply (rule_tac x = "lcm x y" in exI)
   603     apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
   604     done
   605   then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] .
   606   txt {* Interpretation to ease use of definitions, which are
   607     conditional in general but unconditional after interpretation. *}
   608   show "dlat.meet (op dvd) (x::nat) y = gcd x y"
   609     apply (unfold nat_dvd.meet_def)
   610     apply (rule the_equality)
   611     apply (unfold nat_dvd.is_inf_def)
   612     by auto
   613   show "dlat.join (op dvd) (x::nat) y = lcm x y"
   614     apply (unfold nat_dvd.join_def)
   615     apply (rule the_equality)
   616     apply (unfold nat_dvd.is_sup_def)
   617     by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
   618 qed
   619 
   620 text {* Interpreted theorems from the locales, involving defined terms. *}
   621 
   622 thm nat_dvd.less_def text {* from dpo *}
   623 lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)"
   624   apply (rule nat_dvd.less_def) done
   625 thm nat_dvd.meet_left text {* from dlat *}
   626 lemma "gcd x y dvd x"
   627   apply (rule nat_dvd.meet_left) done
   628 
   629 print_interps dpo
   630 print_interps dlat
   631 
   632 
   633 subsection {* Group example with defined operations @{text inv} and @{text unit} *}
   634 
   635 subsubsection {* Locale declarations and lemmas *}
   636 
   637 locale Dsemi =
   638   fixes prod (infixl "**" 65)
   639   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
   640 
   641 locale Dmonoid = Dsemi +
   642   fixes one
   643   assumes l_one [simp]: "one ** x = x"
   644     and r_one [simp]: "x ** one = x"
   645 
   646 begin
   647 
   648 definition
   649   inv where "inv x = (THE y. x ** y = one & y ** x = one)"
   650 definition
   651   unit where "unit x = (EX y. x ** y = one  & y ** x = one)"
   652 
   653 lemma inv_unique:
   654   assumes eq: "y ** x = one" "x ** y' = one"
   655   shows "y = y'"
   656 proof -
   657   from eq have "y = y ** (x ** y')" by (simp add: r_one)
   658   also have "... = (y ** x) ** y'" by (simp add: assoc)
   659   also from eq have "... = y'" by (simp add: l_one)
   660   finally show ?thesis .
   661 qed
   662 
   663 lemma unit_one [intro, simp]:
   664   "unit one"
   665   by (unfold unit_def) auto
   666 
   667 lemma unit_l_inv_ex:
   668   "unit x ==> \<exists>y. y ** x = one"
   669   by (unfold unit_def) auto
   670 
   671 lemma unit_r_inv_ex:
   672   "unit x ==> \<exists>y. x ** y = one"
   673   by (unfold unit_def) auto
   674 
   675 lemma unit_l_inv:
   676   "unit x ==> inv x ** x = one"
   677   apply (simp add: unit_def inv_def) apply (erule exE)
   678   apply (rule theI2, fast)
   679   apply (rule inv_unique)
   680   apply fast+
   681   done
   682 
   683 lemma unit_r_inv:
   684   "unit x ==> x ** inv x = one"
   685   apply (simp add: unit_def inv_def) apply (erule exE)
   686   apply (rule theI2, fast)
   687   apply (rule inv_unique)
   688   apply fast+
   689   done
   690 
   691 lemma unit_inv_unit [intro, simp]:
   692   "unit x ==> unit (inv x)"
   693 proof -
   694   assume x: "unit x"
   695   show "unit (inv x)"
   696     by (auto simp add: unit_def
   697       intro: unit_l_inv unit_r_inv x)
   698 qed
   699 
   700 lemma unit_l_cancel [simp]:
   701   "unit x ==> (x ** y = x ** z) = (y = z)"
   702 proof
   703   assume eq: "x ** y = x ** z"
   704     and G: "unit x"
   705   then have "(inv x ** x) ** y = (inv x ** x) ** z"
   706     by (simp add: assoc)
   707   with G show "y = z" by (simp add: unit_l_inv)
   708 next
   709   assume eq: "y = z"
   710     and G: "unit x"
   711   then show "x ** y = x ** z" by simp
   712 qed
   713 
   714 lemma unit_inv_inv [simp]:
   715   "unit x ==> inv (inv x) = x"
   716 proof -
   717   assume x: "unit x"
   718   then have "inv x ** inv (inv x) = inv x ** x"
   719     by (simp add: unit_l_inv unit_r_inv)
   720   with x show ?thesis by simp
   721 qed
   722 
   723 lemma inv_inj_on_unit:
   724   "inj_on inv {x. unit x}"
   725 proof (rule inj_onI, simp)
   726   fix x y
   727   assume G: "unit x"  "unit y" and eq: "inv x = inv y"
   728   then have "inv (inv x) = inv (inv y)" by simp
   729   with G show "x = y" by simp
   730 qed
   731 
   732 lemma unit_inv_comm:
   733   assumes inv: "x ** y = one"
   734     and G: "unit x"  "unit y"
   735   shows "y ** x = one"
   736 proof -
   737   from G have "x ** y ** x = x ** one" by (auto simp add: inv)
   738   with G show ?thesis by (simp del: r_one add: assoc)
   739 qed
   740 
   741 end
   742 
   743 
   744 locale Dgrp = Dmonoid +
   745   assumes unit [intro, simp]: "Dmonoid.unit (op **) one x"
   746 
   747 begin
   748 
   749 lemma l_inv_ex [simp]:
   750   "\<exists>y. y ** x = one"
   751   using unit_l_inv_ex by simp
   752 
   753 lemma r_inv_ex [simp]:
   754   "\<exists>y. x ** y = one"
   755   using unit_r_inv_ex by simp
   756 
   757 lemma l_inv [simp]:
   758   "inv x ** x = one"
   759   using unit_l_inv by simp
   760 
   761 lemma l_cancel [simp]:
   762   "(x ** y = x ** z) = (y = z)"
   763   using unit_l_inv by simp
   764 
   765 lemma r_inv [simp]:
   766   "x ** inv x = one"
   767 proof -
   768   have "inv x ** (x ** inv x) = inv x ** one"
   769     by (simp add: assoc [symmetric] l_inv)
   770   then show ?thesis by (simp del: r_one)
   771 qed
   772 
   773 lemma r_cancel [simp]:
   774   "(y ** x = z ** x) = (y = z)"
   775 proof
   776   assume eq: "y ** x = z ** x"
   777   then have "y ** (x ** inv x) = z ** (x ** inv x)"
   778     by (simp add: assoc [symmetric] del: r_inv)
   779   then show "y = z" by simp
   780 qed simp
   781 
   782 lemma inv_one [simp]:
   783   "inv one = one"
   784 proof -
   785   have "inv one = one ** (inv one)" by (simp del: r_inv)
   786   moreover have "... = one" by simp
   787   finally show ?thesis .
   788 qed
   789 
   790 lemma inv_inv [simp]:
   791   "inv (inv x) = x"
   792   using unit_inv_inv by simp
   793 
   794 lemma inv_inj:
   795   "inj_on inv UNIV"
   796   using inv_inj_on_unit by simp
   797 
   798 lemma inv_mult_group:
   799   "inv (x ** y) = inv y ** inv x"
   800 proof -
   801   have "inv (x ** y) ** (x ** y) = (inv y ** inv x) ** (x ** y)"
   802     by (simp add: assoc l_inv) (simp add: assoc [symmetric])
   803   then show ?thesis by (simp del: l_inv)
   804 qed
   805 
   806 lemma inv_comm:
   807   "x ** y = one ==> y ** x = one"
   808   by (rule unit_inv_comm) auto
   809 
   810 lemma inv_equality:
   811      "y ** x = one ==> inv x = y"
   812   apply (simp add: inv_def)
   813   apply (rule the_equality)
   814    apply (simp add: inv_comm [of y x])
   815   apply (rule r_cancel [THEN iffD1], auto)
   816   done
   817 
   818 end
   819 
   820 
   821 locale Dhom = Dgrp prod (infixl "**" 65) one + Dgrp sum (infixl "+++" 60) zero +
   822   fixes hom
   823   assumes hom_mult [simp]: "hom (x ** y) = hom x +++ hom y"
   824 
   825 begin
   826 
   827 lemma hom_one [simp]:
   828   "hom one = zero"
   829 proof -
   830   have "hom one +++ zero = hom one +++ hom one"
   831     by (simp add: hom_mult [symmetric] del: hom_mult)
   832   then show ?thesis by (simp del: r_one)
   833 qed
   834 
   835 end
   836 
   837 
   838 subsubsection {* Interpretation of Functions *}
   839 
   840 interpretation Dfun: Dmonoid ["op o" "id :: 'a => 'a"]
   841   where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
   842 (*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
   843 proof -
   844   show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc)
   845   note Dmonoid = this
   846 (*
   847   from this interpret Dmonoid ["op o" "id :: 'a => 'a"] .
   848 *)
   849   show "Dmonoid.unit (op o) (id :: 'a => 'a) f = bij f"
   850     apply (unfold Dmonoid.unit_def [OF Dmonoid])
   851     apply rule apply clarify
   852   proof -
   853     fix f g
   854     assume id1: "f o g = id" and id2: "g o f = id"
   855     show "bij f"
   856     proof (rule bijI)
   857       show "inj f"
   858       proof (rule inj_onI)
   859         fix x y
   860         assume "f x = f y"
   861 	then have "(g o f) x = (g o f) y" by simp
   862 	with id2 show "x = y" by simp
   863       qed
   864     next
   865       show "surj f"
   866       proof (rule surjI)
   867 	fix x
   868         from id1 have "(f o g) x = x" by simp
   869 	then show "f (g x) = x" by simp
   870       qed
   871     qed
   872   next
   873     fix f
   874     assume bij: "bij f"
   875     then
   876     have inv: "f o Hilbert_Choice.inv f = id & Hilbert_Choice.inv f o f = id"
   877       by (simp add: bij_def surj_iff inj_iff)
   878     show "EX g. f o g = id & g o f = id" by rule (rule inv)
   879   qed
   880 qed
   881 
   882 thm Dmonoid.unit_def Dfun.unit_def
   883 
   884 thm Dmonoid.inv_inj_on_unit Dfun.inv_inj_on_unit
   885 
   886 lemma unit_id:
   887   "(f :: unit => unit) = id"
   888   by rule simp
   889 
   890 interpretation Dfun: Dgrp ["op o" "id :: unit => unit"]
   891   where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
   892 proof -
   893   have "Dmonoid op o (id :: 'a => 'a)" ..
   894   note Dmonoid = this
   895 
   896   show "Dgrp (op o) (id :: unit => unit)"
   897 apply unfold_locales
   898 apply (unfold Dmonoid.unit_def [OF Dmonoid])
   899 apply (insert unit_id)
   900 apply simp
   901 done
   902   show "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
   903 apply (unfold Dmonoid.inv_def [OF Dmonoid] inv_def)
   904 apply (insert unit_id)
   905 apply simp
   906 apply (rule the_equality)
   907 apply rule
   908 apply rule
   909 apply simp
   910 done
   911 qed
   912 
   913 thm Dfun.unit_l_inv Dfun.l_inv
   914 
   915 thm Dfun.inv_equality
   916 thm Dfun.inv_equality
   917 
   918 end