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