37 using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example |
37 using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example |
38 |
38 |
39 @{ML_response [display,gray] |
39 @{ML_response [display,gray] |
40 "@{term \"(a::nat) + b = c\"}" |
40 "@{term \"(a::nat) + b = c\"}" |
41 "Const (\"op =\", \<dots>) $ |
41 "Const (\"op =\", \<dots>) $ |
42 (Const (\"Algebras.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"} |
42 (Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"} |
43 |
43 |
44 constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using |
44 constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using |
45 the internal representation corresponding to the datatype @{ML_type_ind "term"}, |
45 the internal representation corresponding to the datatype @{ML_type_ind "term"}, |
46 which is defined as follows: |
46 which is defined as follows: |
47 *} |
47 *} |
531 (@{text "list"}). Even worse, some constants have a name involving |
531 (@{text "list"}). Even worse, some constants have a name involving |
532 type-classes. Consider for example the constants for @{term "zero"} and |
532 type-classes. Consider for example the constants for @{term "zero"} and |
533 \mbox{@{text "(op *)"}}: |
533 \mbox{@{text "(op *)"}}: |
534 |
534 |
535 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" |
535 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" |
536 "(Const (\"Algebras.zero_class.zero\", \<dots>), |
536 "(Const (\"Groups.zero_class.zero\", \<dots>), |
537 Const (\"Algebras.times_class.times\", \<dots>))"} |
537 Const (\"Groups.times_class.times\", \<dots>))"} |
538 |
538 |
539 While you could use the complete name, for example |
539 While you could use the complete name, for example |
540 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
540 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
541 matching against @{text "Nil"}, this would make the code rather brittle. |
541 matching against @{text "Nil"}, this would make the code rather brittle. |
542 The reason is that the theory and the name of the datatype can easily change. |
542 The reason is that the theory and the name of the datatype can easily change. |
768 say @{text "s1"} and @{text "s2"}, which we attach to the schematic type |
768 say @{text "s1"} and @{text "s2"}, which we attach to the schematic type |
769 variables @{text "?'a"} and @{text "?'b"}. Since we do not make any |
769 variables @{text "?'a"} and @{text "?'b"}. Since we do not make any |
770 assumption about the sorts, they are incomparable. |
770 assumption about the sorts, they are incomparable. |
771 *} |
771 *} |
772 |
772 |
|
773 class s1 |
|
774 class s2 |
|
775 |
773 ML{*val (tyenv, index) = let |
776 ML{*val (tyenv, index) = let |
774 val ty1 = @{typ_pat "?'a::s1"} |
777 val ty1 = @{typ_pat "?'a::s1"} |
775 val ty2 = @{typ_pat "?'b::s2"} |
778 val ty2 = @{typ_pat "?'b::s2"} |
776 in |
779 in |
777 Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) |
780 Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) |
1637 and @{text "\<And>"}, or the other way around. A reason for such a transformation |
1640 and @{text "\<And>"}, or the other way around. A reason for such a transformation |
1638 might be stating a definition. The reason is that definitions can only be |
1641 might be stating a definition. The reason is that definitions can only be |
1639 stated using object logic connectives, while theorems using the connectives |
1642 stated using object logic connectives, while theorems using the connectives |
1640 from the meta logic are more convenient for reasoning. Therefore there are |
1643 from the meta logic are more convenient for reasoning. Therefore there are |
1641 some build in functions which help with these transformations. The function |
1644 some build in functions which help with these transformations. The function |
1642 @{ML_ind rulify in ObjectLogic} |
1645 @{ML_ind rulify in Object_Logic} |
1643 replaces all object connectives by equivalents in the meta logic. For example |
1646 replaces all object connectives by equivalents in the meta logic. For example |
1644 |
1647 |
1645 @{ML_response_fake [display, gray] |
1648 @{ML_response_fake [display, gray] |
1646 "ObjectLogic.rulify @{thm foo_test2}" |
1649 "Object_Logic.rulify @{thm foo_test2}" |
1647 "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"} |
1650 "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"} |
1648 |
1651 |
1649 The transformation in the other direction can be achieved with function |
1652 The transformation in the other direction can be achieved with function |
1650 @{ML_ind atomize in ObjectLogic} and the following code. |
1653 @{ML_ind atomize in Object_Logic} and the following code. |
1651 |
1654 |
1652 @{ML_response_fake [display,gray] |
1655 @{ML_response_fake [display,gray] |
1653 "let |
1656 "let |
1654 val thm = @{thm foo_test1} |
1657 val thm = @{thm foo_test1} |
1655 val meta_eq = ObjectLogic.atomize (cprop_of thm) |
1658 val meta_eq = Object_Logic.atomize (cprop_of thm) |
1656 in |
1659 in |
1657 MetaSimplifier.rewrite_rule [meta_eq] thm |
1660 MetaSimplifier.rewrite_rule [meta_eq] thm |
1658 end" |
1661 end" |
1659 "?A \<longrightarrow> ?B \<longrightarrow> ?C"} |
1662 "?A \<longrightarrow> ?B \<longrightarrow> ?C"} |
1660 |
1663 |
1661 In this code the function @{ML atomize in ObjectLogic} produces |
1664 In this code the function @{ML atomize in Object_Logic} produces |
1662 a meta-equation between the given theorem and the theorem transformed |
1665 a meta-equation between the given theorem and the theorem transformed |
1663 into the object logic. The result is the theorem with object logic |
1666 into the object logic. The result is the theorem with object logic |
1664 connectives. However, in order to completely transform a theorem |
1667 connectives. However, in order to completely transform a theorem |
1665 involving meta variables, such as @{thm [source] list.induct}, which |
1668 involving meta variables, such as @{thm [source] list.induct}, which |
1666 is of the form |
1669 is of the form |
1674 *} |
1677 *} |
1675 |
1678 |
1676 ML{*fun atomize_thm thm = |
1679 ML{*fun atomize_thm thm = |
1677 let |
1680 let |
1678 val thm' = forall_intr_vars thm |
1681 val thm' = forall_intr_vars thm |
1679 val thm'' = ObjectLogic.atomize (cprop_of thm') |
1682 val thm'' = Object_Logic.atomize (cprop_of thm') |
1680 in |
1683 in |
1681 MetaSimplifier.rewrite_rule [thm''] thm' |
1684 MetaSimplifier.rewrite_rule [thm''] thm' |
1682 end*} |
1685 end*} |
1683 |
1686 |
1684 text {* |
1687 text {* |
1685 This function produces for the theorem @{thm [source] list.induct} |
1688 This function produces for the theorem @{thm [source] list.induct} |
1686 |
1689 |
1687 @{ML_response_fake [display, gray] |
1690 @{ML_response_fake [display, gray] |
1688 "atomize_thm @{thm list.induct}" |
1691 "atomize_thm @{thm list.induct}" |
1689 "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"} |
1692 "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"} |
1690 |
|
1691 \footnote{\bf FIXME: say someting about @{ML_ind standard in Drule}.} |
|
1692 |
1693 |
1693 Theorems can also be produced from terms by giving an explicit proof. |
1694 Theorems can also be produced from terms by giving an explicit proof. |
1694 One way to achieve this is by using the function @{ML_ind prove in Goal} |
1695 One way to achieve this is by using the function @{ML_ind prove in Goal} |
1695 in the structure @{ML_struct Goal}. For example below we use this function |
1696 in the structure @{ML_struct Goal}. For example below we use this function |
1696 to prove the term @{term "P \<Longrightarrow> P"}.\footnote{\bf FIXME: What about @{ML_ind prove_internal in Goal}?} |
1697 to prove the term @{term "P \<Longrightarrow> P"}.\footnote{\bf FIXME: What about @{ML_ind prove_internal in Goal}?} |