38 open FundefLib |
38 open FundefLib |
39 open FundefCommon |
39 open FundefCommon |
40 |
40 |
41 val note_theorem = LocalTheory.note Thm.theoremK |
41 val note_theorem = LocalTheory.note Thm.theoremK |
42 |
42 |
|
43 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
|
44 |
43 fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *) |
45 fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *) |
44 let val (xs, ys) = split_list ps |
46 let val (xs, ys) = split_list ps |
45 in xs ~~ f ys end |
47 in xs ~~ f ys end |
46 |
48 |
47 fun restore_spec_structure reps spec = |
49 fun restore_spec_structure reps spec = |
48 (burrow o burrow_snd o burrow o K) reps spec |
50 (burrow o burrow_snd o burrow o K) reps spec |
49 |
51 |
50 fun add_simps label moreatts mutual_info fixes psimps spec lthy = |
52 fun add_simps fixes spec sort label moreatts simps lthy = |
51 let |
53 let |
52 val fnames = map (fst o fst) fixes |
54 val fnames = map (fst o fst) fixes |
53 |
55 |
54 val (saved_spec_psimps, lthy) = |
56 val (saved_spec_simps, lthy) = |
55 fold_map (fold_map note_theorem) (restore_spec_structure psimps spec) lthy |
57 fold_map (fold_map note_theorem) (restore_spec_structure simps spec) lthy |
56 val saved_psimps = flat (map snd (flat saved_spec_psimps)) |
58 val saved_simps = flat (map snd (flat saved_spec_simps)) |
57 |
59 |
58 val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps |
60 val simps_by_f = sort saved_simps |
59 |
61 |
60 fun add_for_f fname psimps = |
62 fun add_for_f fname simps = |
61 note_theorem |
63 note_theorem |
62 ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts), |
64 ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts), |
63 psimps) #> snd |
65 simps) #> snd |
64 in |
66 in |
65 (saved_psimps, |
67 (saved_simps, |
66 fold2 add_for_f fnames psimps_by_f lthy) |
68 fold2 add_for_f fnames simps_by_f lthy) |
67 end |
69 end |
68 |
70 |
69 |
71 |
70 fun fundef_afterqed config fixes spec mutual_info defname data [[result]] lthy = |
72 fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy = |
71 let |
73 let |
72 val FundefConfig { domintros, ...} = config |
74 val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = |
73 val Prep {f, R, ...} = data |
75 cont (Goal.close_result proof) |
74 val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result |
76 |
75 val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data |
|
76 val qualify = NameSpace.qualified defname |
77 val qualify = NameSpace.qualified defname |
|
78 val addsimps = add_simps fixes spec sort_cont |
77 |
79 |
78 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
80 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
79 lthy |
81 lthy |
80 |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec) |
82 |> addsimps "psimps" [] psimps |
81 ||>> PROFILE "adding pinduct" |
83 ||> fold_option (snd oo addsimps "simps" []) trsimps |
82 (note_theorem ((qualify "pinduct", |
84 ||>> note_theorem ((qualify "pinduct", |
83 [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)) |
85 [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts) |
84 ||>> PROFILE "adding termination" |
86 ||>> note_theorem ((qualify "termination", []), [termination]) |
85 (note_theorem ((qualify "termination", []), [termination])) |
87 ||> (snd o note_theorem ((qualify "cases", []), [cases])) |
86 ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases]))) |
88 ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros |
87 ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros))) |
89 |
88 |
90 val cdata = FundefCtxData { add_simps=addsimps, psimps=psimps', |
89 val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps', |
|
90 pinducts=snd pinducts', termination=termination', f=f, R=R } |
91 pinducts=snd pinducts', termination=termination', f=f, R=R } |
91 |
|
92 |
|
93 in |
92 in |
94 lthy (* FIXME proper handling of morphism *) |
93 lthy (* FIXME proper handling of morphism *) |
95 |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *) |
94 |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *) |
96 |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *) |
95 |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *) |
97 end (* FIXME: Add cases for induct and cases thm *) |
96 end (* FIXME: Add cases for induct and cases thm *) |
115 end |
114 end |
116 |
115 |
117 |
116 |
118 fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy = |
117 fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy = |
119 let |
118 let |
120 val FundefConfig {sequential, default, ...} = config |
119 val FundefConfig {sequential, default, tailrec, ...} = config |
121 |
120 |
122 val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy |
121 val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy |
|
122 |
|
123 val defname = mk_defname fixes |
|
124 |
123 val t_eqns = spec |
125 val t_eqns = spec |
124 |> flat |> map snd |> flat (* flatten external structure *) |
126 |> flat |> map snd |> flat (* flatten external structure *) |
125 |
127 |
126 val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = |
128 val ((goalstate, cont, sort_cont), lthy) = |
127 FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy |
129 FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy |
128 |
130 |
129 val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result |
131 val afterqed = fundef_afterqed config fixes spec defname cont sort_cont |
130 in |
132 in |
131 (name, lthy |
133 (defname, lthy |
132 |> Proof.theorem_i NONE afterqed [[(goal, [])]] |
134 |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] |
133 |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd) |
135 |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd) |
134 end |
136 end |
135 |
137 |
136 |
138 |
137 fun total_termination_afterqed defname data [[totality]] lthy = |
139 fun total_termination_afterqed defname data [[totality]] lthy = |
138 let |
140 let |
139 val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data |
141 val FundefCtxData { add_simps, psimps, pinducts, ... } = data |
140 |
142 |
141 val totality = PROFILE "closing" Goal.close_result totality |
143 val totality = Goal.close_result totality |
142 |
144 |
143 val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) |
145 val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) |
144 |
146 |
145 val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps |
147 val tsimps = map remove_domain_condition psimps |
146 val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts |
148 val tinduct = map remove_domain_condition pinducts |
147 |
149 |
148 (* FIXME: How to generate code from (possibly) local contexts*) |
150 (* FIXME: How to generate code from (possibly) local contexts*) |
149 val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps |
151 val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps |
150 val allatts = if has_guards then [] else [Attrib.internal (K (RecfunCodegen.add NONE))] |
152 val allatts = if has_guards then [] else [Attrib.internal (K (RecfunCodegen.add NONE))] |
151 |
153 |
152 val qualify = NameSpace.qualified defname; |
154 val qualify = NameSpace.qualified defname; |
153 in |
155 in |
154 lthy |
156 lthy |
155 |> PROFILE "adding tsimps" (add_simps "simps" allatts mutual fixes tsimps spec) |> snd |
157 |> add_simps "simps" allatts tsimps |> snd |
156 |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd |
158 |> note_theorem ((qualify "induct", []), tinduct) |> snd |
157 end |
159 end |
158 |
160 |
159 |
161 |
160 fun setup_termination_proof name_opt lthy = |
162 fun setup_termination_proof name_opt lthy = |
161 let |
163 let |
162 val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt |
164 val defname = the_default (get_last_fundef (Context.Proof lthy)) name_opt |
163 val data = the (get_fundef_data name (Context.Proof lthy)) |
165 val data = the (get_fundef_data defname (Context.Proof lthy)) |
164 handle Option.Option => raise ERROR ("No such function definition: " ^ name) |
166 handle Option.Option => raise ERROR ("No such function definition: " ^ defname) |
165 |
167 |
166 val FundefCtxData {termination, f, R, ...} = data |
168 val FundefCtxData {termination, R, ...} = data |
167 val goal = FundefTermination.mk_total_termination_goal f R |
169 val goal = FundefTermination.mk_total_termination_goal R |
168 in |
170 in |
169 lthy |
171 lthy |
170 |> ProofContext.note_thmss_i "" |
172 |> ProofContext.note_thmss_i "" |
171 [(("termination", [ContextRules.intro_query NONE]), |
173 [(("termination", [ContextRules.intro_query NONE]), |
172 [([Goal.norm_result termination], [])])] |> snd |
174 [([Goal.norm_result termination], [])])] |> snd |
173 |> set_termination_rule termination |
175 |> set_termination_rule termination |
174 |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]] |
176 |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]] |
175 end |
177 end |
176 |
178 |
177 |
179 |
178 val add_fundef = gen_add_fundef Specification.read_specification |
180 val add_fundef = gen_add_fundef Specification.read_specification |
179 val add_fundef_i = gen_add_fundef Specification.cert_specification |
181 val add_fundef_i = gen_add_fundef Specification.cert_specification |