Specification

definition theorem

legend

NoteBehavior

structure Behavior.{u_1, u_2} (L : FirstOrder.Language) (M : Type) [L.Structure M] (Input Output : Type) :
  Type

• relation : Option M → Option Input → Option M → Option Output → Prop

Show details

Outer dependencies: (none)

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure

Lean core dependencies: Eq, HEq, Option, eq_of_heq

Used by: Class, Creation, Destruction, Internal, NormalBehavior, Object, doorBehavior

NoteNormalBehavior

structure NormalBehavior.{u_1, u_2} (L : FirstOrder.Language) (M : Type) [L.Structure M]
  (Input Output : Type) : Type

• (inherited from Behavior)

  relation : Option M → Option Input → Option M → Option Output → Prop

• all_present : ∀ (pre : Option M) (i : Option Input) (post : Option M) (o : Option Output),
  Behavior.relation L pre i post o →
    pre.isSome = true ∧ i.isSome = true ∧ post.isSome = true ∧ o.isSome = true

Show details

Outer dependencies: (none)

Inner dependencies: Behavior

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure

Lean core dependencies: And, Bool, Eq, HEq, Option, Option.isSome, eq_of_heq

Used by: (none)

NoteCreation

structure Creation.{u_1, u_2} (L : FirstOrder.Language) (M : Type) [L.Structure M] (Input Output : Type) :
  Type

• (inherited from Behavior)

  relation : Option M → Option Input → Option M → Option Output → Prop

• no_initial : ∀ (pre : Option M) (i : Option Input) (post : Option M) (o : Option Output),
  Behavior.relation L pre i post o → pre = none

Show details

Outer dependencies: (none)

Inner dependencies: Behavior

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure

Lean core dependencies: Eq, HEq, Option, eq_of_heq

Used by: (none)

NoteDestruction

structure Destruction.{u_1, u_2} (L : FirstOrder.Language) (M : Type) [L.Structure M] (Input Output : Type) :
  Type

• (inherited from Behavior)

  relation : Option M → Option Input → Option M → Option Output → Prop

• no_final : ∀ (pre : Option M) (i : Option Input) (post : Option M) (o : Option Output),
  Behavior.relation L pre i post o → post = none

Show details

Outer dependencies: (none)

Inner dependencies: Behavior

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure

Lean core dependencies: Eq, HEq, Option, eq_of_heq

Used by: (none)

NoteInternal

structure Internal.{u_1, u_2} (L : FirstOrder.Language) (M : Type) [L.Structure M] (Input Output : Type) :
  Type

• (inherited from Behavior)

  relation : Option M → Option Input → Option M → Option Output → Prop

• no_io : ∀ (pre : Option M) (i : Option Input) (post : Option M) (o : Option Output),
  Behavior.relation L pre i post o → i = none ∧ o = none

Show details

Outer dependencies: (none)

Inner dependencies: Behavior

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure

Lean core dependencies: And, Eq, HEq, Option, eq_of_heq

Used by: (none)

NoteInterface

structure Interface (M : Type) : Type 1

• Method : Type

• input : self.Method → Set M

• output : self.Method → Set M

Show details

Outer dependencies: (none)

Mathlib dependencies: Set

Lean core dependencies: Eq, HEq, Nat, SizeOf, eq_of_heq

Used by: Class, Class.Active, Class.Passive, Class.Reactive, Class.not_reactive_and_active, Class.reachable, Interface.combine, Object, Object.state, doorInterface

NoteInterface.combine

def Interface.combine {M : Type} (I1 I2 : Interface M) : Interface M

Show details

| I1.combine I2 =
  { Method := I1.Method ⊕ I2.Method, input := Sum.elim I1.input I2.input,
    output := Sum.elim I1.output I2.output }

Complexity: 87 (size of the value term)

Outer dependencies: Interface

Mathlib dependencies: Set

Lean core dependencies: Sum, Sum.elim

Used by: (none)

NoteClass

structure Class.{u_1, u_2} (M : Type) (L : FirstOrder.Language) [L.Structure M] (I : Interface M) : Type

• State : Set M

• operation : (m : I.Method) → Behavior L M ↑(I.input m) ↑(I.output m)

• autonomous : ↑self.State → ↑self.State → Prop

Show details

Outer dependencies: Interface

Inner dependencies: Behavior

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure, Set, Set.Elem

Lean core dependencies: Eq, HEq, Nat, SizeOf, eq_of_heq

Used by: Class.Active, Class.Passive, Class.Reactive, Class.not_reactive_and_active, Class.reachable, Object, Object.state, doorClass

NoteClass.Reactive

def Class.Reactive.{u_1, u_2} {M : Type} {L : FirstOrder.Language} [L.Structure M] {I : Interface M}
  (C : Class M L I) : Prop

Show details

| C.Reactive = ∀ (s s' : ↑C.State), ¬C.autonomous s s'

Complexity: 73 (size of the value term)

Outer dependencies: Class, Interface

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure, Set.Elem

Lean core dependencies: Not

Used by: Class.Passive, Class.not_reactive_and_active

NoteClass.Passive

def Class.Passive.{u_1, u_2} {M : Type} {L : FirstOrder.Language} [L.Structure M] {I : Interface M}
  (C : Class M L I) : Prop

Show details

| C.Passive =
  (C.Reactive ∧
    ∀ (m : I.Method) (s s' : ↑C.State) (i : ↑(I.input m)) (o : ↑(I.output m)),
      Behavior.relation L (some ↑s) (some i) (some ↑s') (some o) → s = s')

Complexity: 275 (size of the value term)

Outer dependencies: Class, Interface

Inner dependencies: Class.Reactive

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure, Set, Set.Elem

Lean core dependencies: And, Eq

Used by: (none)

NoteClass.Active

def Class.Active.{u_1, u_2} {M : Type} {L : FirstOrder.Language} [L.Structure M] {I : Interface M}
  (C : Class M L I) : Prop

Show details

| C.Active = ∃ s s', C.autonomous s s'

Complexity: 107 (size of the value term)

Outer dependencies: Class, Interface

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure, Set.Elem

Lean core dependencies: Exists

Used by: Class.not_reactive_and_active

ImportantClass.not_reactive_and_active

theorem Class.not_reactive_and_active.{u_1, u_2} {M : Type} {L : FirstOrder.Language} [L.Structure M]
  {I : Interface M} (C : Class M L I) (h1 : C.Reactive) (h2 : C.Active) : False

Show details

fun {M} {L} [L.Structure M] {I} C h1 h2 =>
  match h2 with
  | Exists.intro s (Exists.intro s' ha) => h1 s s' ha

Complexity: 131 (size of the value term)

Dependencies: Class, Class.Active, Class.Reactive, Interface

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure, Set.Elem

Lean core dependencies: Exists, False

Used by: (none)

NoteClass.reachable

def Class.reachable.{u_1, u_2} {M : Type} {L : FirstOrder.Language} [L.Structure M] {I : Interface M}
  (C : Class M L I) (s s' : ↑C.State) : Prop

Show details

| C.reachable s s' = (C.autonomous s s' ∨ ∃ m i o, Behavior.relation L (some ↑s) i (some ↑s') o)

Complexity: 273 (size of the value term)

Outer dependencies: Class, Interface

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure, Set, Set.Elem

Lean core dependencies: Exists, Option, Or

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitiontheoremdeclared elsewheredependencyproof dependency

legend