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