[4b23aa]: thys / PseudoHoops / RightComplementedMonoid.thy  Maximize  Restore  History

Download this file

89 lines (64 with data), 3.4 kB

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
header{* Right Complemented Monoid *}
theory RightComplementedMonoid
imports LeftComplementedMonoid
begin
class left_pordered_monoid_mult = order + monoid_mult +
assumes mult_left_mono: "a \<le> b \<Longrightarrow> c * a \<le> c * b"
class integral_left_pordered_monoid_mult = left_pordered_monoid_mult + one_greatest
class right_residuated = ord + times + right_imp +
assumes right_residual: "(a * x \<le> b) = (x \<le> a r\<rightarrow> b)"
class right_residuated_pordered_monoid = integral_left_pordered_monoid_mult + right_residuated
class right_inf = inf + times + right_imp +
assumes inf_r_def: "(a \<sqinter> b) = a * (a r\<rightarrow> b)"
class right_complemented_monoid = right_residuated_pordered_monoid + right_inf +
assumes left_divisibility: "(a \<le> b) = (\<exists> c . a = b * c)"
sublocale right_complemented_monoid < dual!: left_complemented_monoid "\<lambda> a b . b * a" "op \<sqinter>" "op r\<rightarrow>" 1 "op \<le>" "op <"
apply unfold_locales
apply (simp_all add: inf_r_def mult_assoc mult_left_mono)
apply (simp add: right_residual)
by (simp add: left_divisibility)
context right_complemented_monoid begin
lemma rcm_D: "a r\<rightarrow> a = 1"
by (rule dual.lcm_D)
subclass semilattice_inf_infix
by unfold_locales
lemma right_semilattice_inf: "class.semilattice_inf_infix inf op \<le> op <"
by unfold_locales
lemma right_one_inf [simp]: "1 \<sqinter> a = a"
by (rule dual.left_one_inf)
lemma right_one_impl [simp]: "1 r\<rightarrow> a = a"
by (rule dual.left_one_impl)
lemma rcm_A: "a * (a r\<rightarrow> b) = b * (b r\<rightarrow> a)"
by (rule dual.lcm_A)
lemma rcm_B: "((b * a) r\<rightarrow> c) = (a r\<rightarrow> (b r\<rightarrow> c))"
by (rule dual.lcm_B)
lemma rcm_C: "(a \<le> b) = ((a r\<rightarrow> b) = 1)"
by (rule dual.lcm_C)
end
class right_complemented_monoid_nole_algebra = right_imp + one_times + right_inf + less_def +
assumes right_impl_one [simp]: "a r\<rightarrow> a = 1"
and right_impl_times: "a * (a r\<rightarrow> b) = b * (b r\<rightarrow> a)"
and right_impl_ded: "((a * b) r\<rightarrow> c) = (b r\<rightarrow> (a r\<rightarrow> c))"
class right_complemented_monoid_algebra = right_complemented_monoid_nole_algebra +
assumes right_lesseq: "(a \<le> b) = ((a r\<rightarrow> b) = 1)"
begin
end
sublocale right_complemented_monoid_algebra < dual_algebra!: left_complemented_monoid_algebra "\<lambda> a b . b * a" inf "op r\<rightarrow>" "op \<le>" "op <" 1
apply (unfold_locales, simp_all)
by (rule inf_r_def, rule right_impl_times, rule right_impl_ded, rule right_lesseq)
context right_complemented_monoid_algebra begin
subclass right_complemented_monoid
apply unfold_locales
apply simp_all
apply (simp add: dual_algebra.mult_assoc)
apply (simp add: dual_algebra.mult_right_mono)
apply (simp add: dual_algebra.left_residual)
by (simp add: dual_algebra.right_divisibility)
end
lemma (in right_complemented_monoid) right_complemented_monoid: "class.right_complemented_monoid_algebra (op \<le>) (op <) 1 (op *) inf (op r\<rightarrow>)"
by (unfold_locales, simp_all add: less_le_not_le rcm_A rcm_B rcm_C rcm_D)
(*
sublocale right_complemented_monoid < rcm!: right_complemented_monoid_algebra "op \<le>" "op <" 1 "op *" inf "op r\<rightarrow>"
by (unfold_locales, simp_all add: less_le_not_le rcm_A rcm_B rcm_C rcm_D)
*)
end

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks