equal
deleted
inserted
replaced
921 |
921 |
922 (* outer syntax *) |
922 (* outer syntax *) |
923 |
923 |
924 local structure P = OuterParse and K = OuterKeyword in |
924 local structure P = OuterParse and K = OuterKeyword in |
925 |
925 |
|
926 val _ = OuterSyntax.keywords ["monos"]; |
|
927 |
926 (* FIXME tmp *) |
928 (* FIXME tmp *) |
927 fun flatten_specification specs = specs |> maps |
929 fun flatten_specification specs = specs |> maps |
928 (fn (a, (concl, [])) => concl |> map |
930 (fn (a, (concl, [])) => concl |> map |
929 (fn ((b, atts), [B]) => |
931 (fn ((b, atts), [B]) => |
930 if a = "" then ((b, atts), B) |
932 if a = "" then ((b, atts), B) |
943 (fn lthy => lthy |> gen_add_inductive mk_def true coind preds params |
945 (fn lthy => lthy |> gen_add_inductive mk_def true coind preds params |
944 (flatten_specification specs) monos |> snd)); |
946 (flatten_specification specs) monos |> snd)); |
945 |
947 |
946 val ind_decl = gen_ind_decl add_ind_def; |
948 val ind_decl = gen_ind_decl add_ind_def; |
947 |
949 |
948 val inductiveP = |
950 val _ = OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false); |
949 OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false); |
951 val _ = OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true); |
950 |
952 |
951 val coinductiveP = |
953 val _ = |
952 OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true); |
|
953 |
|
954 |
|
955 val inductive_casesP = |
|
956 OuterSyntax.command "inductive_cases" |
954 OuterSyntax.command "inductive_cases" |
957 "create simplified instances of elimination rules (improper)" K.thy_script |
955 "create simplified instances of elimination rules (improper)" K.thy_script |
958 (P.opt_target -- P.and_list1 SpecParse.spec |
956 (P.opt_target -- P.and_list1 SpecParse.spec |
959 >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs))); |
957 >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs))); |
960 |
958 |
961 val _ = OuterSyntax.add_keywords ["monos"]; |
|
962 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; |
|
963 |
|
964 end; |
959 end; |
965 |
960 |
966 end; |
961 end; |