equal
deleted
inserted
replaced
64 \begin{matharray}{rcl} |
64 \begin{matharray}{rcl} |
65 @{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
65 @{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
66 @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
66 @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
67 @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
67 @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
68 @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
68 @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
|
69 @{command_def "print_inductives"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
69 @{attribute_def (HOL) mono} & : & @{text attribute} \\ |
70 @{attribute_def (HOL) mono} & : & @{text attribute} \\ |
70 \end{matharray} |
71 \end{matharray} |
71 |
72 |
72 An \emph{inductive definition} specifies the least predicate or set |
73 An \emph{inductive definition} specifies the least predicate or set |
73 @{text R} closed under given rules: applying a rule to elements of |
74 @{text R} closed under given rules: applying a rule to elements of |
132 |
133 |
133 \item @{command (HOL) "inductive_set"} and @{command (HOL) |
134 \item @{command (HOL) "inductive_set"} and @{command (HOL) |
134 "coinductive_set"} are wrappers for to the previous commands for |
135 "coinductive_set"} are wrappers for to the previous commands for |
135 native HOL predicates. This allows to define (co)inductive sets, |
136 native HOL predicates. This allows to define (co)inductive sets, |
136 where multiple arguments are simulated via tuples. |
137 where multiple arguments are simulated via tuples. |
|
138 |
|
139 \item @{command "print_inductives"} prints (co)inductive definitions and |
|
140 monotonicity rules. |
137 |
141 |
138 \item @{attribute (HOL) mono} declares monotonicity rules in the |
142 \item @{attribute (HOL) mono} declares monotonicity rules in the |
139 context. These rule are involved in the automated monotonicity |
143 context. These rule are involved in the automated monotonicity |
140 proof of the above inductive and coinductive definitions. |
144 proof of the above inductive and coinductive definitions. |
141 |
145 |