63 not need to have any theorem attributes. A testcase for this function is |
63 not need to have any theorem attributes. A testcase for this function is |
64 *} |
64 *} |
65 |
65 |
66 local_setup %gray {* fn lthy => |
66 local_setup %gray {* fn lthy => |
67 let |
67 let |
68 val arg = ((Binding.name "MyTrue", NoSyn), @{term True}) |
68 val arg = ((@{binding "MyTrue"}, NoSyn), @{term True}) |
69 val (def, lthy') = make_defs arg lthy |
69 val (def, lthy') = make_defs arg lthy |
70 in |
70 in |
71 warning (str_of_thm lthy' def); lthy' |
71 warning (str_of_thm lthy' def); lthy' |
72 end *} |
72 end *} |
73 |
73 |
188 let |
188 let |
189 val rules = [@{prop "even 0"}, |
189 val rules = [@{prop "even 0"}, |
190 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
190 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
191 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
191 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
192 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
192 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
193 val prednames = [Binding.name "even", Binding.name "odd"] |
193 val prednames = [@{binding "even"}, @{binding "odd"}] |
194 val syns = [NoSyn, NoSyn] |
194 val syns = [NoSyn, NoSyn] |
195 val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
195 val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
196 val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy |
196 val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy |
197 in |
197 in |
198 warning (str_of_thms lthy' defs); lthy' |
198 warning (str_of_thms lthy' defs); lthy' |
499 map_index prove_intro rules |
499 map_index prove_intro rules |
500 end*} |
500 end*} |
501 |
501 |
502 text {* main internal function *} |
502 text {* main internal function *} |
503 |
503 |
504 ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy = |
504 ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy = |
505 let |
505 let |
506 val syns = map snd pred_specs |
506 val syns = map snd pred_specs |
507 val pred_specs' = map fst pred_specs |
507 val pred_specs' = map fst pred_specs |
508 val prednames = map fst pred_specs' |
508 val prednames = map fst pred_specs' |
509 val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs' |
509 val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs' |
520 in |
520 in |
521 lthy' |
521 lthy' |
522 |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
522 |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
523 ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) |
523 ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) |
524 |-> (fn intross => LocalTheory.note Thm.theoremK |
524 |-> (fn intross => LocalTheory.note Thm.theoremK |
525 ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) |
525 ((Binding.qualify false mut_name (@{binding "intros"}), []), maps snd intross)) |
526 |>> snd |
526 |>> snd |
527 ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
527 ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
528 ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), |
528 ((Binding.qualify false (Binding.name_of R) (@{binding "induct"}), |
529 [Attrib.internal (K (RuleCases.case_names case_names)), |
529 [Attrib.internal (K (RuleCases.case_names case_names)), |
530 Attrib.internal (K (RuleCases.consumes 1)), |
530 Attrib.internal (K (RuleCases.consumes 1)), |
531 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
531 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
532 (pred_specs ~~ ind_rules)) #>> maps snd) |
532 (pred_specs ~~ ind_rules)) #>> maps snd) |
533 |> snd |
533 |> snd |
534 end*} |
534 end*} |
535 |
535 |
536 ML{*fun add_inductive pred_specs rule_specs lthy = |
536 ML{*fun add_inductive_cmd pred_specs rule_specs lthy = |
537 let |
537 let |
538 val ((pred_specs', rule_specs'), _) = |
538 val ((pred_specs', rule_specs'), _) = |
539 Specification.read_spec pred_specs rule_specs lthy |
539 Specification.read_spec pred_specs rule_specs lthy |
540 in |
540 in |
541 add_inductive_i pred_specs' rule_specs' lthy |
541 add_inductive pred_specs' rule_specs' lthy |
542 end*} |
542 end*} |
543 |
543 |
544 ML{*val spec_parser = |
544 ML{*val spec_parser = |
545 OuterParse.fixes -- |
545 OuterParse.fixes -- |
546 Scan.optional |
546 Scan.optional |
549 (OuterParse.enum1 "|" |
549 (OuterParse.enum1 "|" |
550 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
550 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
551 |
551 |
552 ML{*val specification = |
552 ML{*val specification = |
553 spec_parser >> |
553 spec_parser >> |
554 (fn ((pred_specs), rule_specs) => add_inductive pred_specs rule_specs)*} |
554 (fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*} |
555 |
555 |
556 ML{*val _ = OuterSyntax.local_theory "simple_inductive" |
556 ML{*val _ = OuterSyntax.local_theory "simple_inductive" |
557 "define inductive predicates" |
557 "define inductive predicates" |
558 OuterKeyword.thy_decl specification*} |
558 OuterKeyword.thy_decl specification*} |
559 |
559 |