theory Termin8 imports Main begin section \Typedef\ typedef 'a ne = "{xs :: 'a list . xs \ []}" by (rule exI[where x = "[undefined]"]) simp definition singleton :: "'a \ 'a ne" where "singleton x = Abs_ne [x]" definition append :: "'a ne \ 'a list \ 'a ne" where "append l1 l2 = Abs_ne (Rep_ne l1 @ l2)" definition head :: "'a ne \ 'a" where "head x = hd (Rep_ne x)" definition tail :: "'a ne \ 'a ne" where "tail x = Abs_ne (tl (Rep_ne x))" lemma "head (append l1 l2) = head l1" unfolding head_def append_def by (simp add: Abs_ne_inverse Rep_ne[simplified]) definition tail' :: "'a ne \ 'a list" where "tail' x = tl (Rep_ne x)" lemma "append (singleton (head l)) (tail' l) = l" unfolding head_def append_def tail'_def singleton_def by (simp add: Abs_ne_inverse Rep_ne_inverse Rep_ne[simplified]) section \Locales\ locale Magma = fixes M :: "'a set" fixes bop :: "'a \ 'a \ 'a" (infixl "\" 60) assumes closed: "a \ M \ b \ M \ a \ b \ M" begin lemma closed3: "a \ M \ a \ a \ a \ M" by (intro closed) thm closed3 end locale Semigroup = Magma + assumes assoc: "a \ M \ b \ M \ c \ M \ (a \ b) \ c = a \ (b \ c)" locale Monoid = Semigroup + fixes \ :: 'a assumes \_in_M: "\ \ M" assumes neutral: "a \ M \ \ \ a = a" "a \ M \ a \ \ = a" begin lemma neutral_unique: assumes e_neutral: "\a \ M. a \ e = a" and e_in_M: "e \ M" shows "e = \" using \_in_M e_in_M e_neutral neutral(1) by auto end interpretation Mod3: Magma "{0::nat, 1, 2}" "\ a b. (a + b) mod 3" by unfold_locales auto interpretation Mod3: Monoid "{0::nat, 1, 2}" "\ a b. (a + b) mod 3" 0 by unfold_locales auto locale Group = Monoid + assumes ex_inv: "a \ M \ \ b \ M. a \ b = \ \ b \ a = \" begin definition inv :: "'a \ 'a" where "inv a = (SOME b. b \ M \ a \ b = \ \ b \ a = \)" lemma inv_left: "a \ M \ a \ inv a = \" unfolding inv_def apply (rule someI2_ex) using ex_inv apply blast apply auto done lemma inv_right: "a \ M \ inv a \ a= \" unfolding inv_def apply (rule someI2_ex) using ex_inv apply blast apply auto done lemma inv_in_M: "a \ M \ inv a \ M" unfolding inv_def apply (rule someI2_ex) using ex_inv apply blast apply auto done end interpretation Mod3: Group "{0::nat, 1, 2}" "\ a b. (a + b) mod 3" 0 by unfold_locales (auto; presburger) locale AbelianGroup = Group + assumes commutative: "a \ M \ b \ M \ a \ b = b \ a" interpretation Mod3: AbelianGroup "{0::nat, 1, 2}" "\ a b. (a + b) mod 3" 0 by unfold_locales auto locale Ring = add: AbelianGroup M add zero + mul: Semigroup M mul for M :: "'a set" and add :: "'a \ 'a \ 'a" (infixl "\" 64) and zero :: "'a" ("\") and mul :: "'a \ 'a \ 'a" (infixl "\" 64) + assumes distrib: "a \ M \ b \ M \ c \ M \ (a \ b) \ c = (a \ c) \ (b \ c)" assumes distrib2: "a \ M \ b \ M \ c \ M \ c \ (a \ b) = (c \ a) \ (c \ b)" begin thm add.closed mul.closed end interpretation Mod3_mul: Magma "{0::nat, 1, 2}" "\ a b. (a * b) mod 3" by unfold_locales auto interpretation Mod3_mul: Semigroup "{0::nat, 1, 2}" "\ a b. (a * b) mod 3" by unfold_locales auto interpretation Mod3: Ring "{0::nat, 1, 2}" "\ a b. (a + b) mod 3" 0 "\ a b. (a * b) mod 3" by unfold_locales auto lemma (in Ring) zero_left_mult: assumes "a \ M" shows "\ \ a = \" (* Sledgehammer-Proof 1: *) by (smt add.\_in_M add.ex_inv add.neutral(1) assms local.add.assoc local.distrib mul.closed) (* Sledgehammer-Proof 2: proof - have f1: "\ \ a \ M" using add.\_in_M assms mul.closed by presburger then have "\ \ (\ \ a) = \ \ a" by (meson add.neutral(1)) then show ?thesis using f1 by (metis (no_types) add.\_in_M add.ex_inv add.neutral(1) assms local.add.assoc local.distrib) qed Manueller Proof: proof- have "\ \ a = (\ \ a) \ \" by (simp add: add.\_in_M add.neutral(2) assms mul.closed) also have "\ = (\ \ a) \ ((\ \ a) \ add.inv ((\ \ a)))" by (simp add: add.\_in_M add.inv_left assms mul.closed) also have "\ = ((\ \ a) \ (\ \ a)) \ add.inv ((\ \ a))" by (simp add: add.\_in_M add.inv_in_M assms local.add.assoc mul.closed) also have "\ = ((\ \ \) \ a) \ add.inv (\ \ a)" by (simp add: add.\_in_M assms local.distrib) also have "\ = (\ \ a) \ add.inv (\ \ a)" by (simp add: add.\_in_M add.neutral(1)) also have "\ = \" by (simp add: add.\_in_M add.inv_left assms mul.closed) finally show ?thesis. qed *) thm Mod3.zero_left_mult end