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