80 function @{ML_ind declare_const in Sign} from the structure @{ML_struct |
72 function @{ML_ind declare_const in Sign} from the structure @{ML_struct |
81 Sign}. To see how \isacommand{setup} works, consider the following code: |
73 Sign}. To see how \isacommand{setup} works, consider the following code: |
82 |
74 |
83 *} |
75 *} |
84 |
76 |
85 ML{*let |
77 ML %grayML{*let |
86 val thy = @{theory} |
78 val thy = @{theory} |
87 val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn) |
79 val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn) |
88 in |
80 in |
89 Sign.declare_const @{context} bar_const thy |
81 Sign.declare_const @{context} bar_const thy |
90 end*} |
82 end*} |
254 @{text z} and @{text w} are not anymore in the scope of the context. |
246 @{text z} and @{text w} are not anymore in the scope of the context. |
255 This means the curly-braces act on the Isabelle level as opening and closing statements |
247 This means the curly-braces act on the Isabelle level as opening and closing statements |
256 for a context. The above proof fragment corresponds roughly to the following ML-code |
248 for a context. The above proof fragment corresponds roughly to the following ML-code |
257 *} |
249 *} |
258 |
250 |
259 ML{*val ctxt0 = @{context}; |
251 ML %grayML{*val ctxt0 = @{context}; |
260 val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0; |
252 val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0; |
261 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*} |
253 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*} |
262 |
254 |
263 text {* |
255 text {* |
264 where the function @{ML_ind add_fixes in Variable} fixes a list of variables |
256 where the function @{ML_ind add_fixes in Variable} fixes a list of variables |
598 \end{isabelle} |
590 \end{isabelle} |
599 |
591 |
600 The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as |
592 The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as |
601 *} |
593 *} |
602 |
594 |
603 ML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*} |
595 ML %grayML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*} |
604 |
596 |
605 text {* |
597 text {* |
606 Morphisms can be composed with the function @{ML_ind "$>" in Morphism} |
598 Morphisms can be composed with the function @{ML_ind "$>" in Morphism} |
607 *} |
599 *} |
608 |
600 |
609 ML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T) |
601 ML %grayML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T) |
610 | trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t) |
602 | trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t) |
611 | trm_phi (t $ s) = (trm_phi t) $ (trm_phi s) |
603 | trm_phi (t $ s) = (trm_phi t) $ (trm_phi s) |
612 | trm_phi t = t*} |
604 | trm_phi t = t*} |
613 |
605 |
614 ML{*val phi = Morphism.term_morphism trm_phi*} |
606 ML %grayML{*val phi = Morphism.term_morphism trm_phi*} |
615 |
607 |
616 ML{*Morphism.term phi @{term "P x y"}*} |
608 ML %grayML{*Morphism.term phi @{term "P x y"}*} |
617 |
609 |
618 text {* |
610 text {* |
619 @{ML_ind term_morphism in Morphism} |
611 @{ML_ind term_morphism in Morphism} |
620 |
612 |
621 @{ML_ind term in Morphism}, |
613 @{ML_ind term in Morphism}, |