Commit e01ca943 authored by Florian Rabe's avatar Florian Rabe

no message

parent 83acccfb
......@@ -9,6 +9,7 @@ import info.kwarc.mmt.lf._
object Tutorial {
val path = DPath(URI("http","cds.omdoc.org")) / "examples" / "tutorial"
val under = List(info.kwarc.mmt.lf.Apply.path)
}
object FOL {
......@@ -28,17 +29,10 @@ object Nat {
object NatLiterals extends RepresentedRealizedType(Nat.nattp,StandardNat)
object Succ extends RealizedOperator(Nat.succ, SynOpType(List(Nat.nattp), Nat.nattp),
Arithmetic.Succ, SemOpType(List(StandardNat), StandardNat))
object Succ extends RealizedOperator(Nat.succ, SynOpType(Tutorial.under, List(Nat.nattp), Nat.nattp),
Arithmetic.Succ, SemOpType(List(StandardNat), StandardPositive))
object Plus extends RealizedOperator(Nat.plus, SynOpType(List(Nat.nattp, Nat.nattp), Nat.nattp),
object Plus extends RealizedOperator(Nat.plus, SynOpType(Tutorial.under, List(Nat.nattp, Nat.nattp), Nat.nattp),
Arithmetic.Plus, SemOpType(List(StandardNat,StandardNat), StandardNat))
object SuccInverse extends InverseOperator(Nat.succ) {
def unapply(l: OMLIT): Option[List[OMLIT]] = l match {
case NatLiterals(u : BigInt) if u>0 => Some(List(NatLiterals(u-1)))
case _ => None
}
}
namespace http://cds.omdoc.org/examples❚
/T regular bands❚
theory Regular : ?FOLEQNatDed =
include ?Band ❙
regular: {x,y,z} ⊦ z∘x∘z∘y∘z ≐ z∘x∘y∘z ❙
theory LeftRegular1 : ?FOLEQNatDed =
include ?Band ❙
leftregular1: {x,y,z} ⊦ z∘x∘z∘y ≐ z∘x∘y ❙
theory LeftRegular : ?FOLEQNatDed =
include ?Band ❙
leftregular: {x,z} ⊦ z∘x∘z ≐ z∘x ❙
theory RightRegular1 : ?FOLEQNatDed =
include ?Band ❙
rightregular1: {x,y,z} ⊦ x∘z∘y∘z ≐ x∘y∘z ❙
theory RightRegular : ?FOLEQNatDed =
include ?Band ❙
rightregular: {y,z} ⊦ z∘y∘z ≐ y∘z ❙
/T views for the three stages of regular band theories ❚
implicit view Regular2LeftRegular1 : ?Regular -> ?LeftRegular1 =
include ?Band = ?Band❙
regular = [x,y,z] congT ([u] u∘z) leftregular1❙
implicit view LeftRegular12LeftRegular : ?LeftRegular1 -> ?LeftRegular =
include ?Band = ?Band❙
leftregular1 = [x,y,z] congT ([u] u∘y) leftregular❙
implicit view Regular2RightRegular1 : ?Regular -> ?RightRegular1 =
include ?Band = ?Band❙
regular = [x,y,z] congT ([u] z∘u) rightregular1❙
implicit view RightRegular12RightRegular : ?RightRegular1 -> ?RightRegular =
include ?Band = ?Band❙
rightregular1 = [x,y,z] congT ([u] x∘u) rightregular❙
/T normal bands ❚
theory Normal : ?FOLEQNatDed =
include ?Band ❙
normal: {x,y,z} ⊦ z∘(x∘y)∘z ≐ z∘(y∘x)∘z ❙
theory LeftNormal : ?FOLEQNatDed =
include ?Band ❙
leftnormal: {x,y,z} ⊦ z∘(x∘y) ≐ z∘(y∘x) ❙
theory RightNormal : ?FOLEQNatDed =
include ?Band ❙
rightnormal: {x,y,z} ⊦ (x∘y)∘z ≐ (y∘x)∘z ❙
/T views for the diamond of normal band theories (with semilattices at the bottom) ❚
implicit view Normal2LeftNormal : ?Normal -> ?LeftNormal =
include ?Band = ?Band❙
normal = [x,y,z] congT ([u] u∘z) leftnormal❙
implicit view Normal2RightNormal : ?Normal -> ?RightNormal =
include ?Band = ?Band❙
normal = [x,y,z] congT ([u] z∘u) rightnormal❙
implicit view LeftNormal2Semilattice : ?LeftNormal -> ?Semilattice =
include ?Band = ?Band❙
leftnormal = [x,y,z] congT ([u] z∘u) comm❙
implicit view RightNormal2Semilattice : ?RightNormal -> ?Semilattice =
include ?Band = ?Band❙
rightnormal = [x,y,z] congT ([u] u∘z) comm❙
/T views from regular to normal band theories ❚
implicit view LeftRegular12Normal : ?LeftRegular1 -> ?Normal =
include ?Band = ?Band❙
leftregular1 = [x,y,z] _❙
implicit view LeftRegular2LeftNormal : ?LeftRegular -> ?LeftNormal =
include ?Band = ?Band❙
leftregular = [x,y,z] _❙
implicit view RightRegular12Normal : ?RightRegular1 -> ?Normal =
include ?Band = ?Band❙
rightregular1 = [x,y,z] _❙
implicit view RightRegular2RightNormal : ?RightRegular -> ?RightNormal =
include ?Band = ?Band❙
rightregular = [x,y,z] _❙
......@@ -28,8 +28,8 @@ theory FOLEQNatDed : http://cds.omdoc.org/urtheories?LF =
include ?FOLEQ❙
include ?FOLNatDed ❙
refl : {x} ⊦ x ≐ x❙
congT : {T}{x,y} ⊦ x ≐ y ⟶ ⊦ (T x) ≐ (T y)
congF : {F}{x,y} ⊦ x ≐ y ⟶ ⊦ (F x) ⟶ ⊦ (F y)
congT : {x,y}{T: term ⟶ term} ⊦ x ≐ y ⟶ ⊦ (T x) ≐ (T y) ❘# congT 3 4
congF : {x,y}{F: term ⟶ prop} ⊦ x ≐ y ⟶ ⊦ (F x) ⟶ ⊦ (F y)❘# congF 3 4 5
sym : {x,y} ⊦ x ≐ y ⟶ ⊦ y ≐ x❙
trans : {x,y,z} ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ x ≐ z❙
\ No newline at end of file
namespace http://cds.omdoc.org/examples❚
theory Magma : ?FOLEQNatDed =
op : term ⟶ term ⟶ term ❘# 1 ∘ 2 prec 50❙
theory Semigroup : ?FOLEQNatDed =
include ?Magma❙
assoc: {x,y,z} ⊦ (x∘y)∘z ≐ x∘(y∘z)❙
theory Commutative : ?FOLEQNatDed =
include ?Magma❙
comm: {x,y} ⊦ x∘y ≐ y∘x❙
theory Neutral : ?FOLEQNatDed =
include ?Magma❙
e : term ❙
neutLeft: {x} ⊦ x∘e ≐ x❙
neutRight: {x} ⊦ x∘e ≐ x❙
theory Idempotent : ?FOLEQNatDed =
include ?Magma❙
idempotent: {x} ⊦ x∘x ≐ x❙
theory Monoid : ?FOLEQNatDed =
include ?Semigroup❙
include ?Neutral❙
theory Band : ?FOLEQNatDed =
include ?Semigroup❙
include ?Idempotent❙
theory Semilattice : ?FOLEQNatDed =
include ?Band❙
include ?Commutative❙
\ No newline at end of file
......@@ -40,8 +40,8 @@ theory NatRules : http://cds.omdoc.org/urtheories?LF =
plus_comm : {X,Y} ⊦ X + Y = Y + X ❙
plus_assoc : {X,Y,Z} ⊦ (X + Y) + Z = X + (Y + Z) ❙
plus_neut_Ex : {X} ⊦ X + O = X ❘ # %%prefix 0 1❙
plus_neut_L : {X} ⊦ O + X = X❘ = [X] trans plus_comm (plus_neut_Ex X)❘ role Simplify ❙
plus_neut : {X} ⊦ X + O = X ❘ = [X] plus_neut_Ex X ❘role Simplify ❙
plus_neut_L : {X} ⊦ O + X = X❘ = [X] trans plus_comm plus_neut❘ role Simplify ❙
plus_succ_R : {X,Y} ⊦ X + Y' = (X+Y)'❘role Simplify ❙
plus_succ_L : {X,Y} ⊦ X' + Y = (X+Y)'❘role Simplify ❙
......
......@@ -2,6 +2,7 @@ namespace http://cds.omdoc.org/examples ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚
// temporary experiment by Colin ❚
theory LFEq =
include ur:?LF
rule rules?EquivalenceRelation 
......
......@@ -81,19 +81,6 @@ theory FOL : http://cds.omdoc.org/urtheories?PLF =
forall : {s} (tm s ⟶ prop) ⟶ prop❘# ∀ 2❙
exists : {s} (tm s ⟶ prop) ⟶ prop❘# ∃ 2❙
nat : sort❙
N = tm nat❙
zero : N❙
plus: N ⟶ N ⟶ N ❘ # 1 + 2 prec 100❙
leq: N ⟶ N ⟶ prop ❘ # 1 ≤ 2 prec 100❙
prod : type ⟶ type ⟶ type ❘ # 1 * 2❙
pair : {A,B} A ⟶ B ⟶ A * B ❘ # 3 ∙ 4 prec 50❙
bigplus : {s} (tm s ⟶ prop * N) ⟶ N ❘ # Σ 2 prec 40❙
test : N ⟶ N ❘ = [x] Σ [i] i ≤ x ∙ i❙
/T Finally, we need to be able to talk about the truth of propositions.
For that, we introduce a Curry-Howard style judgment: The LF-type '⊢ P' is the type of proofs of the proposition 'P'.
......@@ -102,11 +89,6 @@ theory FOL : http://cds.omdoc.org/urtheories?PLF =
❘ role Judgment❙
/T It's practical to give ⊢ a very low precedence to avoid brackets later on.❙
test2 : {R,S,F} ⊢ (Σ [x:N] R x ∙ Σ [y:N] S x y ∙ F x y) =
(Σ [y:N] S y y ∙ Σ [x:N] R x ∙ F x y)❙
/T The 'role Judgment' is an attribute introduced by the LF plugin (which tells MMT to be loaded automatically whenever LF is used).
By annotation the symbol 'proof' in this way, the plugin can add some LF-specific language support, in particular, it can generate appropriate default notations.
......
......@@ -24,8 +24,7 @@ theory Nat : ?NatDed =
S : ℕ ⟶ ℕ ❙
rule rules?Succ ❙
/T Furthermore, we can add an InverseRule, which MMT will use for unification, when working with terms that contain both literals and variables: ❙
rule rules?SuccInverse ❙
/T Succ is implemented in such a way that it can be inverted, which MMT will use for unification, when working with terms that contain both literals and variables: ❙
/T MMT will now simplify every instance of S being applied to literals to the actual
computation result. We can test this, by proving that the successor
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment