author | wenzelm |
Tue, 17 Nov 2009 14:51:57 +0100 | |
changeset 33726 | 0878aecbf119 |
parent 33671 | 4b0f2599ed48 |
child 34230 | b0d21ae2528e |
permissions | -rw-r--r-- |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Function/fundef.ML |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
3 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
4 |
A package for general recursive function definitions. |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
5 |
Isar commands. |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
6 |
*) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
7 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
8 |
signature FUNCTION = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
9 |
sig |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
10 |
val add_function : (binding * typ option * mixfix) list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
11 |
-> (Attrib.binding * term) list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
12 |
-> Function_Common.function_config |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
13 |
-> local_theory |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
14 |
-> Proof.state |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
15 |
val add_function_cmd : (binding * string option * mixfix) list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
16 |
-> (Attrib.binding * string) list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
17 |
-> Function_Common.function_config |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
18 |
-> local_theory |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
19 |
-> Proof.state |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
20 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
21 |
val termination_proof : term option -> local_theory -> Proof.state |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
22 |
val termination_proof_cmd : string option -> local_theory -> Proof.state |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
23 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
24 |
val setup : theory -> theory |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
25 |
val get_congs : Proof.context -> thm list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
26 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
27 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
28 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
29 |
structure Function : FUNCTION = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
30 |
struct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
31 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
32 |
open Function_Lib |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
33 |
open Function_Common |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
34 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
35 |
val simp_attribs = map (Attrib.internal o K) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
36 |
[Simplifier.simp_add, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
37 |
Code.add_default_eqn_attribute, |
33552 | 38 |
Nitpick_Simps.add] |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
39 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
40 |
val psimp_attribs = map (Attrib.internal o K) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
41 |
[Simplifier.simp_add, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
42 |
Nitpick_Psimps.add] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
43 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
44 |
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
45 |
|
33395
62571cb54811
conceal partial rules depending on config flag (i.e. when called via "fun")
krauss
parents:
33394
diff
changeset
|
46 |
fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy = |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
47 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
48 |
val spec = post simps |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
49 |
|> map (apfst (apsnd (fn ats => moreatts @ ats))) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
50 |
|> map (apfst (apfst extra_qualify)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
51 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
52 |
val (saved_spec_simps, lthy) = |
33671 | 53 |
fold_map Local_Theory.note spec lthy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
54 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
55 |
val saved_simps = maps snd saved_spec_simps |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
56 |
val simps_by_f = sort saved_simps |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
57 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
58 |
fun add_for_f fname simps = |
33671 | 59 |
Local_Theory.note |
60 |
((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) |
|
33394
9c6980f2eb39
conceal "termination" rule, used only by special tools
krauss
parents:
33369
diff
changeset
|
61 |
#> snd |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
62 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
63 |
(saved_simps, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
64 |
fold2 add_for_f fnames simps_by_f lthy) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
65 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
66 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
67 |
fun gen_add_function is_external prep default_constraint fixspec eqns config lthy = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
68 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
69 |
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
70 |
val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
71 |
val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
72 |
val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
73 |
val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
74 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
75 |
val defname = mk_defname fixes |
33101 | 76 |
val FunctionConfig {partials, ...} = config |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
77 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
78 |
val ((goalstate, cont), lthy) = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
79 |
Function_Mutual.prepare_function_mutual config defname fixes eqs lthy |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
80 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
81 |
fun afterqed [[proof]] lthy = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
82 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
83 |
val FunctionResult {fs, R, psimps, trsimps, simple_pinducts, termination, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
84 |
domintros, cases, ...} = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
85 |
cont (Thm.close_derivation proof) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
86 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
87 |
val fnames = map (fst o fst) fixes |
33394
9c6980f2eb39
conceal "termination" rule, used only by special tools
krauss
parents:
33369
diff
changeset
|
88 |
fun qualify n = Binding.name n |
9c6980f2eb39
conceal "termination" rule, used only by special tools
krauss
parents:
33369
diff
changeset
|
89 |
|> Binding.qualify true defname |
33395
62571cb54811
conceal partial rules depending on config flag (i.e. when called via "fun")
krauss
parents:
33394
diff
changeset
|
90 |
val conceal_partial = if partials then I else Binding.conceal |
33394
9c6980f2eb39
conceal "termination" rule, used only by special tools
krauss
parents:
33369
diff
changeset
|
91 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
92 |
val addsmps = add_simps fnames post sort_cont |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
93 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
94 |
val (((psimps', pinducts'), (_, [termination'])), lthy) = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
95 |
lthy |
33395
62571cb54811
conceal partial rules depending on config flag (i.e. when called via "fun")
krauss
parents:
33394
diff
changeset
|
96 |
|> addsmps (conceal_partial o Binding.qualify false "partial") |
62571cb54811
conceal partial rules depending on config flag (i.e. when called via "fun")
krauss
parents:
33394
diff
changeset
|
97 |
"psimps" conceal_partial psimp_attribs psimps |
62571cb54811
conceal partial rules depending on config flag (i.e. when called via "fun")
krauss
parents:
33394
diff
changeset
|
98 |
||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps |
33671 | 99 |
||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), |
33368 | 100 |
[Attrib.internal (K (Rule_Cases.case_names cnames)), |
101 |
Attrib.internal (K (Rule_Cases.consumes 1)), |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
102 |
Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
33671 | 103 |
||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) |
104 |
||> (snd o Local_Theory.note ((qualify "cases", |
|
33368 | 105 |
[Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) |
33671 | 106 |
||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
107 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
108 |
val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
109 |
pinducts=snd pinducts', termination=termination', |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
110 |
fs=fs, R=R, defname=defname } |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
111 |
val _ = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
112 |
if not is_external then () |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
113 |
else Specification.print_consts lthy (K false) (map fst fixes) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
114 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
115 |
lthy |
33671 | 116 |
|> Local_Theory.declaration false (add_function_data o morph_function_data cdata) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
117 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
118 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
119 |
lthy |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
120 |
|> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
121 |
|> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
122 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
123 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
124 |
val add_function = gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
125 |
val add_function_cmd = gen_add_function true Specification.read_spec "_::type" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
126 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
127 |
fun gen_termination_proof prep_term raw_term_opt lthy = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
128 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
129 |
val term_opt = Option.map (prep_term lthy) raw_term_opt |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
130 |
val data = the (case term_opt of |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
131 |
SOME t => (import_function_data t lthy |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
132 |
handle Option.Option => |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
133 |
error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
134 |
| NONE => (import_last_function lthy handle Option.Option => error "Not a function")) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
135 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
136 |
val FunctionCtxData { termination, R, add_simps, case_names, psimps, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
137 |
pinducts, defname, ...} = data |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
138 |
val domT = domain_type (fastype_of R) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
139 |
val goal = HOLogic.mk_Trueprop |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
140 |
(HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
141 |
fun afterqed [[totality]] lthy = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
142 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
143 |
val totality = Thm.close_derivation totality |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
144 |
val remove_domain_condition = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
145 |
full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
146 |
val tsimps = map remove_domain_condition psimps |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
147 |
val tinduct = map remove_domain_condition pinducts |
33394
9c6980f2eb39
conceal "termination" rule, used only by special tools
krauss
parents:
33369
diff
changeset
|
148 |
fun qualify n = Binding.name n |
9c6980f2eb39
conceal "termination" rule, used only by special tools
krauss
parents:
33369
diff
changeset
|
149 |
|> Binding.qualify true defname |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
150 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
151 |
lthy |
33395
62571cb54811
conceal partial rules depending on config flag (i.e. when called via "fun")
krauss
parents:
33394
diff
changeset
|
152 |
|> add_simps I "simps" I simp_attribs tsimps |> snd |
33671 | 153 |
|> Local_Theory.note |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
154 |
((qualify "induct", |
33368 | 155 |
[Attrib.internal (K (Rule_Cases.case_names case_names))]), |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
156 |
tinduct) |> snd |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
157 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
158 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
159 |
lthy |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
160 |
|> ProofContext.note_thmss "" |
33369 | 161 |
[((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
162 |
|> ProofContext.note_thmss "" |
33369 | 163 |
[((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
164 |
|> ProofContext.note_thmss "" |
33369 | 165 |
[((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
166 |
[([Goal.norm_result termination], [])])] |> snd |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
167 |
|> Proof.theorem_i NONE afterqed [[(goal, [])]] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
168 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
169 |
|
33726
0878aecbf119
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset
|
170 |
val termination_proof = gen_termination_proof Syntax.check_term |
0878aecbf119
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset
|
171 |
val termination_proof_cmd = gen_termination_proof Syntax.read_term |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
172 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
173 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
174 |
(* Datatype hook to declare datatype congs as "function_congs" *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
175 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
176 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
177 |
fun add_case_cong n thy = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
178 |
Context.theory_map (Function_Ctx_Tree.map_function_congs (Thm.add_thm |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
179 |
(Datatype.the_info thy n |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
180 |
|> #case_cong |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
181 |
|> safe_mk_meta_eq))) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
182 |
thy |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
183 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
184 |
val setup_case_cong = Datatype.interpretation (K (fold add_case_cong)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
185 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
186 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
187 |
(* setup *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
188 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
189 |
val setup = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
190 |
Attrib.setup @{binding fundef_cong} |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
191 |
(Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
192 |
"declaration of congruence rule for function definitions" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
193 |
#> setup_case_cong |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
194 |
#> Function_Relation.setup |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
195 |
#> Function_Common.Termination_Simps.setup |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
196 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
197 |
val get_congs = Function_Ctx_Tree.get_function_congs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
198 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
199 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
200 |
(* outer syntax *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
201 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
202 |
local structure P = OuterParse and K = OuterKeyword in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
203 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
204 |
val _ = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
205 |
OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
206 |
(function_parser default_config |
33726
0878aecbf119
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset
|
207 |
>> (fn ((config, fixes), statements) => add_function_cmd fixes statements config)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
208 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
209 |
val _ = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
210 |
OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal |
33726
0878aecbf119
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset
|
211 |
(Scan.option P.term >> termination_proof_cmd) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
212 |
|
33726
0878aecbf119
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset
|
213 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
214 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
215 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
216 |
end |