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 
```
```   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
```