Specification

definition theorem
legend
Behavior.{u_1, u_2} (L : FirstOrder.Language) (M : Type) [L.Structure M] (Input Output : Type) :
  Type
Show details 
| Behavior.mk : {L : FirstOrder.Language} →
  {M : Type} →
    [inst : L.Structure M] →
      {Input Output : Type} →
        (Option M → Option Input → Option M → Option Output → Prop) → Behavior L M Input Output

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

NormalBehavior.{u_1, u_2} (L : FirstOrder.Language) (M : Type) [L.Structure M]
  (Input Output : Type) : Type
Show details 
| NormalBehavior.mk : {L : FirstOrder.Language} →
  {M : Type} →
    [inst : L.Structure M] →
      {Input Output : Type} →
        [toBehavior : Behavior L M Input Output] →
          (∀ (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) →
            NormalBehavior L M Input Output

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)

Creation.{u_1, u_2} (L : FirstOrder.Language) (M : Type) [L.Structure M] (Input Output : Type) :
  Type
Show details 
| Creation.mk : {L : FirstOrder.Language} →
  {M : Type} →
    [inst : L.Structure M] →
      {Input Output : Type} →
        [toBehavior : Behavior L M Input Output] →
          (∀ (pre : Option M) (i : Option Input) (post : Option M) (o : Option Output),
              Behavior.relation L pre i post o → pre = none) →
            Creation L M Input Output

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)

Destruction.{u_1, u_2} (L : FirstOrder.Language) (M : Type) [L.Structure M] (Input Output : Type) :
  Type
Show details 
| Destruction.mk : {L : FirstOrder.Language} →
  {M : Type} →
    [inst : L.Structure M] →
      {Input Output : Type} →
        [toBehavior : Behavior L M Input Output] →
          (∀ (pre : Option M) (i : Option Input) (post : Option M) (o : Option Output),
              Behavior.relation L pre i post o → post = none) →
            Destruction L M Input Output

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)

Internal.{u_1, u_2} (L : FirstOrder.Language) (M : Type) [L.Structure M] (Input Output : Type) :
  Type
Show details 
| Internal.mk : {L : FirstOrder.Language} →
  {M : Type} →
    [inst : L.Structure M] →
      {Input Output : Type} →
        [toBehavior : Behavior L M Input Output] →
          (∀ (pre : Option M) (i : Option Input) (post : Option M) (o : Option Output),
              Behavior.relation L pre i post o → i = none ∧ o = none) →
            Internal L M Input Output

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)

Interface (M : Type) : Type 1
Show details 
| Interface.mk : {M : Type} → (Method : Type) → (Method → Set M) → (Method → Set M) → Interface M

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

Interface.combine {M : Type} (I1 I2 : Interface M) : Interface M
Show details 
fun {M} I1 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)

Class.{u_1, u_2} (M : Type) (L : FirstOrder.Language) [L.Structure M] (I : Interface M) : Type
Show details 
| Class.mk : {M : Type} →
  {L : FirstOrder.Language} →
    [inst : L.Structure M] →
      {I : Interface M} →
        (State : Set M) →
          ((m : I.Method) → Behavior L M ↑(I.input m) ↑(I.output m)) →
            (↑State → ↑State → Prop) → Class M L I

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

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 
fun {M} {L} [L.Structure M] {I} C => ∀ (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

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 
fun {M} {L} [L.Structure M] {I} C =>
  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)

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 
fun {M} {L} [L.Structure M] {I} C => ∃ 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

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)

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 
fun {M} {L} [L.Structure M] {I} C 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