544 \end{isabelle} |
544 \end{isabelle} |
545 |
545 |
546 The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as |
546 The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as |
547 *} |
547 *} |
548 |
548 |
549 ML %grayML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*} |
549 ML %grayML{*val identity = Morphism.morphism "" {binding = [], typ = [], term = [], fact = []}*} |
550 |
550 |
551 text {* |
551 text {* |
552 Morphisms can be composed with the function @{ML_ind "$>" in Morphism} |
552 Morphisms can be composed with the function @{ML_ind "$>" in Morphism} |
553 *} |
553 *} |
554 |
554 |
555 ML %grayML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T) |
555 ML %grayML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T) |
556 | trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t) |
556 | trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t) |
557 | trm_phi (t $ s) = (trm_phi t) $ (trm_phi s) |
557 | trm_phi (t $ s) = (trm_phi t) $ (trm_phi s) |
558 | trm_phi t = t*} |
558 | trm_phi t = t*} |
559 |
559 |
560 ML %grayML{*val phi = Morphism.term_morphism trm_phi*} |
560 ML %grayML{*val phi = Morphism.term_morphism "foo" trm_phi*} |
561 |
561 |
562 ML %grayML{*Morphism.term phi @{term "P x y"}*} |
562 ML %grayML{*Morphism.term phi @{term "P x y"}*} |
563 |
563 |
564 text {* |
564 text {* |
565 @{ML_ind term_morphism in Morphism} |
565 @{ML_ind term_morphism in Morphism} |