theory week12A_demo imports Main begin

-- --------------------------------------------------------------

section "Type classes and instantiations"

class semigroup =
  fixes mult :: "'a => 'a => 'a" (infixr "\<otimes>" 70)
  assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"

definition
  sq :: "'a :: semigroup => 'a" where
  "sq x = x \<otimes> x"

lemma sq2: "sq x \<otimes> sq x = x \<otimes> x \<otimes> x \<otimes> x"
  by (simp add: sq_def assoc)

lemma "sq x \<otimes> sq x + (y::nat) = x \<otimes> x \<otimes> x \<otimes> x + y"
  -- "error"

instantiation nat :: semigroup
begin
  definition mult_nat_def: "(x::nat) \<otimes> y = x * y"
  instance
    apply intro_classes
    apply (simp add: mult_nat_def)
    done
end

lemma "sq x \<otimes> sq x + (y::nat)  = x \<otimes> x \<otimes> x \<otimes> x + y"
  by (simp add: sq2)  

-- "type variables can have multiple class constraints"
-- "the set of constraints is called 'sort'"
notepad begin
  note [[show_sorts]]
  term "(x + 0) * -10"
end

-- --------------------------------------------------------------

section "More instantiation and subclasses"

instantiation int :: semigroup
begin
  definition "(x::int) \<otimes> y = x * y"
  -- "default name: operation_type_def"
  instance by intro_classes (simp add: mult_int_def)
end

-- "the prod type constuctor (_ \<times> _) produces a 
    semigroup if both arguments are semigroups:"
instantiation prod :: (semigroup, semigroup) semigroup
begin
  definition "x \<otimes> y = (fst x \<otimes> fst y, snd x \<otimes> snd y)"
  instance
    apply intro_classes
    apply (simp add: mult_prod_def)
    apply (simp add: assoc)
    done
end

lemma "sq (x::nat, -2::int) \<otimes> (1,1) = (x * x, 4)"
  by (simp add: sq_def mult_prod_def mult_nat_def
                mult_int_def)


class rmonoid = semigroup +
  fixes one :: 'a
  assumes rone: "x \<otimes> one = x"

class monoid = rmonoid +
  assumes lone: "one \<otimes> x = x"

class com_monoid = rmonoid +
  assumes mult_com: "x \<otimes> y = y \<otimes> x"

lemma "one \<otimes> (x :: 'a :: com_monoid) = x"
  apply (rule lone) 
  -- "we haven't told Isabelle that a com_monoid 
      is also a monoid"
  oops

subclass (in com_monoid) monoid
  apply default
  apply (subst mult_com)
  apply (rule rone)
  done

-- "now it works:"
lemma "one \<otimes> (x :: 'a :: com_monoid) = x"
  by (rule lone) 
  

-- --------------------------------------------------------------

section {* Locales, example 1 *}

locale semi =
  fixes prod :: "'a => 'a => 'a" (infixl "\<cdot>" 70)
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"

locale group = semi +
  fixes one ("\<one>") and inv ("_\<^sup>-" [100] 100)
  assumes l_one: "\<one> \<cdot> x = x"
  assumes l_inv: "x\<^sup>-\<cdot> x = \<one>"

lemma (in group) r_inv: "x \<cdot> x\<^sup>- = \<one>"
proof -
  have "x \<cdot> x\<^sup>- = \<one> \<cdot> (x \<cdot> x\<^sup>-)" by (simp only: l_one)
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<^sup>-" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> x\<^sup>- \<cdot> x \<cdot> x\<^sup>-" by (simp only: l_inv)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> (x\<^sup>- \<cdot> x) \<cdot> x\<^sup>-" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> \<one> \<cdot> x\<^sup>-" by (simp only: l_inv)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> (\<one> \<cdot> x\<^sup>-)" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> x\<^sup>-" by (simp only: l_one)
  also have "\<dots> = \<one>" by (simp only: l_inv)
  finally show ?thesis .
qed

-- "group multiple (in locale) lemmas by explicit 
    context:"
context group 
begin

lemma r_one: "x \<cdot> \<one> = x"
proof -
  have "x \<cdot> \<one> = x \<cdot> (x\<^sup>- \<cdot> x)" by (simp only: l_inv)
  also have "\<dots> = (x \<cdot> x\<^sup>-) \<cdot> x" by (simp only: assoc)
  also have "\<dots> = \<one> \<cdot> x" by (simp only: r_inv)
  also have "\<dots> = x" by (simp only: l_one)
  finally show "x \<cdot> \<one> = x" .
qed

lemma l_cancel [simp]: "(x \<cdot> y = x \<cdot> z) = (y = z)"
proof
  assume "x \<cdot> y = x \<cdot> z"
  then have "(x\<^sup>- \<cdot> x) \<cdot> y = (x\<^sup>- \<cdot> x) \<cdot> z" by (simp add: assoc)
  then show "y = z" by (simp add: l_inv l_one)
next
  assume "y = z"
  then show "x \<cdot> y = x \<cdot> z" by simp
qed

end


-- "classes are locales as well:"

locale foo = monoid + 
  constrains mult :: "'a => 'a => ('a::monoid)"
  fixes bar :: "'a => 'b => 'a"
  assumes "bar (x \<otimes> y) z = (x \<otimes> y)"

print_locale foo



subsection {* Export *}

thm semi.assoc group.l_cancel


subsection {* Definitions *}

locale semi2 = semi +
  fixes rprod (infixl "\<odot>" 70)
  defines rprod_def: "rprod x y \<equiv> y \<cdot> x "
begin -- "can directly open context"

lemma r_assoc:
  "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
  by (simp only: rprod_def assoc)

end

thm semi2.r_assoc



-- -----------------------------------------------------------------


section {* Example 2 *}


locale group_hom = a: group add zero minus + b: group 
  for add zero minus +
  fixes hom
  assumes hom_mult: "hom (add x y) = hom x \<cdot> hom y"
begin

lemma hom_one: "hom zero = \<one>"
proof -
  have "hom zero \<cdot> \<one> = hom zero \<cdot> hom zero" 
    by (simp add: hom_mult [symmetric] a.l_one b.r_one)
  then show ?thesis by simp 
qed

end


locale simple =
  fixes a and b 
  assumes A: "a + b = x"

print_theorems

locale not_so_simple = simple +
  fixes c and d
  defines "c \<equiv> a + b"
  assumes B: "a + c = d"

print_theorems


-- ---------------------------------------------------------------

section {* Example 3 *}

lemma int_semi:
  "semi (op +::int => int =>int)"
  apply (unfold_locales) 
  apply auto
  done

lemma int_group:
  "group (op +) (0::int) uminus"
  apply (unfold_locales) 
  apply auto
  done

text {*
  Manual instantiation possible with the OF attribute.
*}

thm semi.assoc [OF int_semi]
thm group.l_cancel [OF int_group]


text {* Automatic instantiation *}

lemma bla: True
proof -
  interpret my: group "op +" "0::int" "uminus"
    by unfold_locales auto
  print_theorems
  thm my.assoc my.l_cancel
oops

interpretation int_grp: group "op +" "0::int" "uminus"
  by unfold_locales auto

print_theorems

end