Object

definition abbreviation theorem

legend

NoteObject

structure Object.{u_1, u_2} {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value)
  {L : FirstOrder.Language} [L.Structure ↑h.reachable] {I : Interface ↑h.reachable}
  (C : Class (↑h.reachable) L I) : Type

• place : Place

• resides : self.place ∈ Heap.domain Value

• member : ⟨Heap.at_ self.place ⋯, ⋯⟩ ∈ C.State

• behavior : (m : I.Method) → Behavior L ↑h.reachable ↑(I.input m) ↑(I.output m)

• compatible : ∀ (m : I.Method) (pre : Option ↑h.reachable) (i : Option ↑(I.input m)) (post : Option ↑h.reachable)
  (o : Option ↑(I.output m)), Behavior.relation L pre i post o → Behavior.relation L pre i post o

Show details

Outer dependencies: Class, Heap, Heap.reachable, Interface

Inner dependencies: Behavior, Heap.mem_reachable

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

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

Used by: Object.state, doorObject

NoteObject.state

abbrev Object.state.{u_1, u_2} {Place Value : Type} [TopologicalSpace Place] {h : Heap Place Value}
  {L : FirstOrder.Language} [L.Structure ↑h.reachable] {I : Interface ↑h.reachable}
  {C : Class (↑h.reachable) L I} (o : Object h C) : ↑C.State

Show details

| o.state = ⟨⟨Heap.at_ o.place ⋯, ⋯⟩, ⋯⟩

Complexity: 315 (size of the value term)

Outer dependencies: Class, Heap, Heap.reachable, Interface, Object

Inner dependencies: Heap.mem_reachable

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

Used by: (none)

NoteDoorState

inductive DoorState : Type

• opened : DoorState

• closed : DoorState

Show details

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, Nat.ble, PULift, cond, noConfusionEnum, noConfusionTypeEnum

Used by: doorBehavior, doorClass, doorHeap, doorHeap.closedVal, doorHeap.closed_reachable, doorHeap.openedVal, doorHeap.opened_reachable, doorInterface, doorObject, instNonemptyDoorState, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

ImportantinstNonemptyDoorState

instance instNonemptyDoorState : Nonempty DoorState

Show details

Nonempty.intro DoorState.opened

Complexity: 5 (size of the value term)

Outer dependencies: DoorState

Lean core dependencies: Nonempty

Used by: (none)

NotedoorHeap

def doorHeap : Heap Bool DoorState

Show details

| doorHeap =
  { domain := Set.univ,
    at_ := fun p x =>
      match p, x with
      | true, x => DoorState.opened
      | false, x => DoorState.closed }

Complexity: 99 (size of the value term)

Outer dependencies: DoorState, Heap

Mathlib dependencies: Set, Set.univ

Lean core dependencies: Bool

Used by: doorBehavior, doorClass, doorHeap.closedVal, doorHeap.closed_reachable, doorHeap.openedVal, doorHeap.opened_reachable, doorInterface, doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

ImportantdoorHeap.opened_reachable

theorem doorHeap.opened_reachable : DoorState.opened ∈ doorHeap.reachable

Show details

Exists.intro true (Exists.intro trivial rfl)

Complexity: 167 (size of the value term)

Dependencies: DoorState, Heap.reachable, doorHeap

Mathlib dependencies: Set

Lean core dependencies: Bool, Eq, Exists, rfl, trivial

Used by: doorHeap.openedVal

ImportantdoorHeap.closed_reachable

theorem doorHeap.closed_reachable : DoorState.closed ∈ doorHeap.reachable

Show details

Exists.intro false (Exists.intro trivial rfl)

Complexity: 167 (size of the value term)

Dependencies: DoorState, Heap.reachable, doorHeap

Mathlib dependencies: Set

Lean core dependencies: Bool, Eq, Exists, rfl, trivial

Used by: doorHeap.closedVal

NotedoorHeap.openedVal

def doorHeap.openedVal : ↑doorHeap.reachable

Show details

| doorHeap.openedVal = ⟨DoorState.opened, doorHeap.opened_reachable⟩

Complexity: 33 (size of the value term)

Outer dependencies: DoorState, Heap.reachable, doorHeap

Inner dependencies: doorHeap.opened_reachable

Mathlib dependencies: Set, Set.Elem

Lean core dependencies: Bool

Used by: instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass

NotedoorHeap.closedVal

def doorHeap.closedVal : ↑doorHeap.reachable

Show details

| doorHeap.closedVal = ⟨DoorState.closed, doorHeap.closed_reachable⟩

Complexity: 33 (size of the value term)

Outer dependencies: DoorState, Heap.reachable, doorHeap

Inner dependencies: doorHeap.closed_reachable

Mathlib dependencies: Set, Set.Elem

Lean core dependencies: Bool

Used by: (none)

NotedoorLanguage

The language of a single unary relation, “is open”.

def doorLanguage : FirstOrder.Language

Show details

| doorLanguage =
  { Functions := fun x => Empty,
    Relations := fun x =>
      match x with
      | 1 => Unit
      | x => Empty }

Complexity: 23 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: FirstOrder.Language

Lean core dependencies: Empty, Eq, Eq.ndrec_symm, Nat, Not, Unit, Unit.unit, dite

Used by: doorBehavior, doorClass, doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

ImportantinstStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

instance instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap :
  doorLanguage.Structure ↑doorHeap.reachable

Show details

| instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap =
  { funMap := fun {x} f x_1 => Empty.elim f,
    RelMap := fun {n} r x =>
      match n, r, x with
      | 1, x, x_1 => ↑(x_1 0) = DoorState.opened
      | 0, r, x => Empty.elim r
      | n.succ.succ, r, x => Empty.elim r }

Complexity: 359 (size of the value term)

Outer dependencies: DoorState, Heap.reachable, doorHeap, doorLanguage

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

Lean core dependencies: Bool, Empty.elim, Eq, Fin, Nat

Used by: doorBehavior, doorClass, doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass

NotedoorInterface

def doorInterface : Interface ↑doorHeap.reachable

Show details

| doorInterface =
  { Method := Unit, input := fun x => {v | ↑v = DoorState.opened},
    output := fun x => {v | ↑v = DoorState.opened} }

Complexity: 157 (size of the value term)

Outer dependencies: DoorState, Heap.reachable, Interface, doorHeap

Mathlib dependencies: Set, Set.Elem, setOf

Lean core dependencies: Bool, Eq, Unit

Used by: doorClass, doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass

NotedoorBehavior

def doorBehavior :
  Behavior doorLanguage ↑doorHeap.reachable ↑{v | ↑v = DoorState.opened}
    ↑{v | ↑v = DoorState.opened}

Show details

| doorBehavior =
  {
    relation := fun pre x post x_1 =>
      ∃ ps po,
        pre = some ps ∧
          post = some po ∧
            (↑ps = DoorState.opened ∧ ↑po = DoorState.closed ∨
              ↑ps = DoorState.closed ∧ ↑po = DoorState.opened) }

Complexity: 689 (size of the value term)

Outer dependencies: Behavior, DoorState, Heap.reachable, doorHeap, doorLanguage, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

Mathlib dependencies: Set, Set.Elem, setOf

Lean core dependencies: And, Bool, Eq, Exists, Option, Or

Used by: doorClass, doorObject

NotedoorClass

def doorClass : Class (↑doorHeap.reachable) doorLanguage doorInterface

Show details

| doorClass =
  { State := Set.univ, operation := fun x => doorBehavior, autonomous := fun x x_1 => False }

Complexity: 123 (size of the value term)

Outer dependencies: Class, DoorState, Heap.reachable, doorHeap, doorInterface, doorLanguage, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

Inner dependencies: doorBehavior

Mathlib dependencies: Set.Elem, Set.univ

Lean core dependencies: Bool, False

Used by: doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass

ImportantinstNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass

instance instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass : Nonempty ↑doorClass.State

Show details

Nonempty.intro ⟨doorHeap.openedVal, trivial⟩

Complexity: 149 (size of the value term)

Outer dependencies: DoorState, Heap.reachable, doorClass, doorHeap, doorInterface, doorLanguage, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

Inner dependencies: doorHeap.openedVal

Mathlib dependencies: Set, Set.Elem

Lean core dependencies: Bool, Nonempty, trivial

Used by: (none)

NotedoorObject

def doorObject : Object doorHeap doorClass

Show details

| doorObject =
  { place := true, resides := trivial, member := trivial, behavior := fun x => doorBehavior,
    compatible := ⋯ }

Complexity: 273 (size of the value term)

Outer dependencies: DoorState, Object, doorClass, doorHeap, doorInterface, doorLanguage, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

Inner dependencies: Heap.reachable, doorBehavior

Mathlib dependencies: Set.Elem

Lean core dependencies: Bool, Option, trivial

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.

definitionabbreviationtheoremexampledeclared elsewheredependencyproof dependency

legend