equal
deleted
inserted
replaced
9 |
9 |
10 signature NOMINAL_FUNCTION_TERMINATION = |
10 signature NOMINAL_FUNCTION_TERMINATION = |
11 sig |
11 sig |
12 include NOMINAL_FUNCTION_DATA |
12 include NOMINAL_FUNCTION_DATA |
13 |
13 |
14 val termination : term option -> local_theory -> Proof.state |
14 val termination : bool -> term option -> local_theory -> Proof.state |
15 val termination_cmd : string option -> local_theory -> Proof.state |
15 val termination_cmd : bool -> string option -> local_theory -> Proof.state |
16 |
16 |
17 end |
17 end |
18 |
18 |
19 structure Nominal_Function_Termination : NOMINAL_FUNCTION_TERMINATION = |
19 structure Nominal_Function_Termination : NOMINAL_FUNCTION_TERMINATION = |
20 struct |
20 struct |
28 Code.add_default_eqn_attribute, |
28 Code.add_default_eqn_attribute, |
29 Nitpick_Simps.add] |
29 Nitpick_Simps.add] |
30 |
30 |
31 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
31 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
32 |
32 |
33 fun prepare_termination_proof prep_term raw_term_opt lthy = |
33 fun prepare_termination_proof prep_term is_eqvt raw_term_opt lthy = |
34 let |
34 let |
35 val term_opt = Option.map (prep_term lthy) raw_term_opt |
35 val term_opt = Option.map (prep_term lthy) raw_term_opt |
36 val info = the (case term_opt of |
36 val info = the (case term_opt of |
37 SOME t => (import_function_data t lthy |
37 SOME t => (import_function_data t lthy |
38 handle Option.Option => |
38 handle Option.Option => |
57 fun qualify n = Binding.name n |
57 fun qualify n = Binding.name n |
58 |> Binding.qualify true defname |
58 |> Binding.qualify true defname |
59 in |
59 in |
60 lthy |
60 lthy |
61 |> add_simps I "simps" I simp_attribs tsimps |
61 |> add_simps I "simps" I simp_attribs tsimps |
62 ||>> Local_Theory.note ((qualify "eqvt", [eqvt_attrib]), teqvts) |
62 ||>> Local_Theory.note ((qualify "eqvt", if is_eqvt then [eqvt_attrib] else []), teqvts) |
63 ||>> Local_Theory.note |
63 ||>> Local_Theory.note |
64 ((qualify "induct", |
64 ((qualify "induct", |
65 [Attrib.internal (K (Rule_Cases.case_names case_names))]), |
65 [Attrib.internal (K (Rule_Cases.case_names case_names))]), |
66 tinducts) |
66 tinducts) |
67 |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy => |
67 |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy => |
78 end |
78 end |
79 in |
79 in |
80 (goal, afterqed, termination) |
80 (goal, afterqed, termination) |
81 end |
81 end |
82 |
82 |
83 fun gen_termination prep_term raw_term_opt lthy = |
83 fun gen_termination prep_term is_eqvt raw_term_opt lthy = |
84 let |
84 let |
85 val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy |
85 val (goal, afterqed, termination) = prepare_termination_proof prep_term is_eqvt raw_term_opt lthy |
86 in |
86 in |
87 lthy |
87 lthy |
88 |> Proof_Context.note_thmss "" |
88 |> Proof_Context.note_thmss "" |
89 [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd |
89 [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd |
90 |> Proof_Context.note_thmss "" |
90 |> Proof_Context.note_thmss "" |
100 |
100 |
101 (* outer syntax *) |
101 (* outer syntax *) |
102 |
102 |
103 val option_parser = |
103 val option_parser = |
104 (Scan.optional (Parse.$$$ "(" |-- Parse.!!! |
104 (Scan.optional (Parse.$$$ "(" |-- Parse.!!! |
105 (Parse.reserved "eqvt" >> K true) --| Parse.$$$ ")") false) |
105 ((Parse.reserved "eqvt" >> K (true, true)) || |
|
106 (Parse.reserved "no_eqvt" >> K (true, false))) --| Parse.$$$ ")") (false, false)) |
106 |
107 |
107 val _ = |
108 val _ = |
108 Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function" |
109 Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function" |
109 Keyword.thy_goal |
110 Keyword.thy_goal |
110 (option_parser -- Scan.option Parse.term >> |
111 (option_parser -- Scan.option Parse.term >> |
111 (fn (is_eqvt, trm) => |
112 (fn ((is_nominal, is_eqvt), opt_trm) => |
112 if is_eqvt then termination_cmd trm else Function.termination_cmd trm)) |
113 if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm)) |
113 |
114 |
114 end |
115 end |