716 "collect_duplicates xs ys (z#zs) = (if z \<in> set xs |
715 "collect_duplicates xs ys (z#zs) = (if z \<in> set xs |
717 then if z \<in> set ys |
716 then if z \<in> set ys |
718 then collect_duplicates xs ys zs |
717 then collect_duplicates xs ys zs |
719 else collect_duplicates xs (z#ys) zs |
718 else collect_duplicates xs (z#ys) zs |
720 else collect_duplicates (z#xs) (z#ys) zs)" |
719 else collect_duplicates (z#xs) (z#ys) zs)" |
721 termination by (auto_term "measure (length o snd o snd)") |
|
722 (*<*) |
720 (*<*) |
723 lemmas [code func] = collect_duplicates.simps |
721 lemmas [code func] = collect_duplicates.simps |
724 (*>*) |
722 (*>*) |
725 |
723 |
726 text {* |
724 text {* |
1113 |
1110 |
1114 fun |
1111 fun |
1115 dummy_option :: "'a list \<Rightarrow> 'a option" where |
1112 dummy_option :: "'a list \<Rightarrow> 'a option" where |
1116 "dummy_option (x#xs) = Some x" |
1113 "dummy_option (x#xs) = Some x" |
1117 "dummy_option [] = arbitrary" |
1114 "dummy_option [] = arbitrary" |
1118 termination by (auto_term "{}") |
|
1119 (*<*) |
1115 (*<*) |
1120 declare dummy_option.simps [code func] |
1116 declare dummy_option.simps [code func] |
1121 (*>*) |
1117 (*>*) |
1122 |
1118 |
1123 code_gen dummy_option (SML "examples/arbitrary.ML") |
1119 code_gen dummy_option (SML "examples/arbitrary.ML") |
1199 |
1195 |
1200 text %mlref {* |
1196 text %mlref {* |
1201 \begin{mldecls} |
1197 \begin{mldecls} |
1202 @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\ |
1198 @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\ |
1203 @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\ |
1199 @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\ |
1204 @{index_ML CodegenData.add_funcl: "CodegenConsts.const * CodegenData.lthms -> theory -> theory"} \\ |
1200 @{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\ |
1205 @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\ |
1201 @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\ |
1206 @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\ |
1202 @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\ |
1207 @{index_ML CodegenData.add_inline_proc: "(theory -> cterm list -> thm list) |
1203 @{index_ML CodegenData.add_inline_proc: "(theory -> cterm list -> thm list) |
1208 -> theory -> theory"} \\ |
1204 -> theory -> theory"} \\ |
1209 @{index_ML CodegenData.add_preproc: "(theory -> thm list -> thm list) |
1205 @{index_ML CodegenData.add_preproc: "(theory -> thm list -> thm list) |
1210 -> theory -> theory"} \\ |
1206 -> theory -> theory"} \\ |
1211 @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list) |
1207 @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list) |
1212 * CodegenData.lthms) -> theory -> theory"} \\ |
1208 * thm list Susp.T) -> theory -> theory"} \\ |
1213 @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\ |
1209 @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\ |
1214 @{index_ML CodegenData.get_datatype: "theory -> string |
1210 @{index_ML CodegenData.get_datatype: "theory -> string |
1215 -> ((string * sort) list * (string * typ list) list) option"} \\ |
1211 -> ((string * sort) list * (string * typ list) list) option"} \\ |
1216 @{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"} |
1212 @{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"} |
1217 \end{mldecls} |
1213 \end{mldecls} |