author | wenzelm |
Tue, 04 Jun 2019 20:01:02 +0200 | |
changeset 70325 | 9bf04a8f211f |
parent 70324 | 005c1cdbfd3f |
child 71179 | 592e2afdd50c |
permissions | -rw-r--r-- |
40107 | 1 |
(* Title: HOL/Tools/Function/partial_function.ML |
2 |
Author: Alexander Krauss, TU Muenchen |
|
3 |
||
4 |
Partial function definitions based on least fixed points in ccpos. |
|
5 |
*) |
|
6 |
||
7 |
signature PARTIAL_FUNCTION = |
|
8 |
sig |
|
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
9 |
val init: string -> term -> term -> thm -> thm -> thm option -> declaration |
52727 | 10 |
val mono_tac: Proof.context -> int -> tactic |
40107 | 11 |
val add_partial_function: string -> (binding * typ option * mixfix) list -> |
66653 | 12 |
Attrib.binding * term -> local_theory -> (term * thm) * local_theory |
40107 | 13 |
val add_partial_function_cmd: string -> (binding * string option * mixfix) list -> |
66653 | 14 |
Attrib.binding * string -> local_theory -> (term * thm) * local_theory |
69829 | 15 |
val transform_result: morphism -> term * thm -> term * thm |
40107 | 16 |
end; |
17 |
||
18 |
structure Partial_Function: PARTIAL_FUNCTION = |
|
19 |
struct |
|
20 |
||
63005 | 21 |
open Function_Lib |
22 |
||
23 |
||
40107 | 24 |
(*** Context Data ***) |
25 |
||
61113 | 26 |
datatype setup_data = Setup_Data of |
43080 | 27 |
{fixp: term, |
28 |
mono: term, |
|
29 |
fixp_eq: thm, |
|
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
30 |
fixp_induct: thm, |
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
31 |
fixp_induct_user: thm option}; |
43080 | 32 |
|
61113 | 33 |
fun transform_setup_data phi (Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user}) = |
34 |
let |
|
35 |
val term = Morphism.term phi; |
|
36 |
val thm = Morphism.thm phi; |
|
37 |
in |
|
38 |
Setup_Data |
|
39 |
{fixp = term fixp, mono = term mono, fixp_eq = thm fixp_eq, |
|
40 |
fixp_induct = thm fixp_induct, fixp_induct_user = Option.map thm fixp_induct_user} |
|
41 |
end; |
|
42 |
||
40107 | 43 |
structure Modes = Generic_Data |
44 |
( |
|
43080 | 45 |
type T = setup_data Symtab.table; |
40107 | 46 |
val empty = Symtab.empty; |
47 |
val extend = I; |
|
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41117
diff
changeset
|
48 |
fun merge data = Symtab.merge (K true) data; |
40107 | 49 |
) |
50 |
||
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
51 |
fun init mode fixp mono fixp_eq fixp_induct fixp_induct_user phi = |
40107 | 52 |
let |
61113 | 53 |
val data' = |
54 |
Setup_Data |
|
55 |
{fixp = fixp, mono = mono, fixp_eq = fixp_eq, |
|
56 |
fixp_induct = fixp_induct, fixp_induct_user = fixp_induct_user} |
|
57 |
|> transform_setup_data (phi $> Morphism.trim_context_morphism); |
|
58 |
in Modes.map (Symtab.update (mode, data')) end; |
|
40107 | 59 |
|
60 |
val known_modes = Symtab.keys o Modes.get o Context.Proof; |
|
61113 | 61 |
|
62 |
fun lookup_mode ctxt = |
|
63 |
Symtab.lookup (Modes.get (Context.Proof ctxt)) |
|
67664 | 64 |
#> Option.map (transform_setup_data (Morphism.transfer_morphism' ctxt)); |
40107 | 65 |
|
66 |
||
67 |
(*** Automated monotonicity proofs ***) |
|
68 |
||
69 |
(*rewrite conclusion with k-th assumtion*) |
|
70 |
fun rewrite_with_asm_tac ctxt k = |
|
45403 | 71 |
Subgoal.FOCUS (fn {context = ctxt', prems, ...} => |
63170 | 72 |
Local_Defs.unfold0_tac ctxt' [nth prems k]) ctxt; |
40107 | 73 |
|
54405
88f6d5b1422f
ported 'partial_function' to 'Ctr_Sugar' abstraction
blanchet
parents:
52728
diff
changeset
|
74 |
fun dest_case ctxt t = |
40107 | 75 |
case strip_comb t of |
76 |
(Const (case_comb, _), args) => |
|
54405
88f6d5b1422f
ported 'partial_function' to 'Ctr_Sugar' abstraction
blanchet
parents:
52728
diff
changeset
|
77 |
(case Ctr_Sugar.ctr_sugar_of_case ctxt case_comb of |
40107 | 78 |
NONE => NONE |
54405
88f6d5b1422f
ported 'partial_function' to 'Ctr_Sugar' abstraction
blanchet
parents:
52728
diff
changeset
|
79 |
| SOME {case_thms, ...} => |
40107 | 80 |
let |
59582 | 81 |
val lhs = Thm.prop_of (hd case_thms) |
40107 | 82 |
|> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst; |
83 |
val arity = length (snd (strip_comb lhs)); |
|
84 |
val conv = funpow (length args - arity) Conv.fun_conv |
|
54405
88f6d5b1422f
ported 'partial_function' to 'Ctr_Sugar' abstraction
blanchet
parents:
52728
diff
changeset
|
85 |
(Conv.rewrs_conv (map mk_meta_eq case_thms)); |
40107 | 86 |
in |
87 |
SOME (nth args (arity - 1), conv) |
|
88 |
end) |
|
89 |
| _ => NONE; |
|
90 |
||
91 |
(*split on case expressions*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58839
diff
changeset
|
92 |
val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} => |
40107 | 93 |
SUBGOAL (fn (t, i) => case t of |
94 |
_ $ (_ $ Abs (_, _, body)) => |
|
54405
88f6d5b1422f
ported 'partial_function' to 'Ctr_Sugar' abstraction
blanchet
parents:
52728
diff
changeset
|
95 |
(case dest_case ctxt body of |
40107 | 96 |
NONE => no_tac |
97 |
| SOME (arg, conv) => |
|
98 |
let open Conv in |
|
42083
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
41472
diff
changeset
|
99 |
if Term.is_open arg then no_tac |
61844 | 100 |
else ((DETERM o Induct.cases_tac ctxt false [[SOME arg]] NONE []) |
40107 | 101 |
THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58839
diff
changeset
|
102 |
THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl} |
40107 | 103 |
THEN_ALL_NEW (CONVERSION |
104 |
(params_conv ~1 (fn ctxt' => |
|
105 |
arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i |
|
106 |
end) |
|
107 |
| _ => no_tac) 1); |
|
108 |
||
109 |
(*monotonicity proof: apply rules + split case expressions*) |
|
110 |
fun mono_tac ctxt = |
|
63170 | 111 |
K (Local_Defs.unfold0_tac ctxt [@{thm curry_def}]) |
40107 | 112 |
THEN' (TRY o REPEAT_ALL_NEW |
67149 | 113 |
(resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>partial_function_mono\<close>)) |
40107 | 114 |
ORELSE' split_cases_tac ctxt)); |
115 |
||
116 |
||
117 |
(*** Auxiliary functions ***) |
|
118 |
||
119 |
(*Returns t $ u, but instantiates the type of t to make the |
|
120 |
application type correct*) |
|
121 |
fun apply_inst ctxt t u = |
|
122 |
let |
|
42361 | 123 |
val thy = Proof_Context.theory_of ctxt; |
40107 | 124 |
val T = domain_type (fastype_of t); |
125 |
val T' = fastype_of u; |
|
42388 | 126 |
val subst = Sign.typ_match thy (T, T') Vartab.empty |
40107 | 127 |
handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u]) |
128 |
in |
|
129 |
map_types (Envir.norm_type subst) t $ u |
|
130 |
end; |
|
131 |
||
132 |
fun head_conv cv ct = |
|
133 |
if can Thm.dest_comb ct then Conv.fun_conv (head_conv cv) ct else cv ct; |
|
134 |
||
135 |
||
136 |
(*** currying transformation ***) |
|
137 |
||
138 |
fun curry_const (A, B, C) = |
|
67149 | 139 |
Const (\<^const_name>\<open>Product_Type.curry\<close>, |
40107 | 140 |
[HOLogic.mk_prodT (A, B) --> C, A, B] ---> C); |
141 |
||
142 |
fun mk_curry f = |
|
143 |
case fastype_of f of |
|
144 |
Type ("fun", [Type (_, [S, T]), U]) => |
|
145 |
curry_const (S, T, U) $ f |
|
146 |
| T => raise TYPE ("mk_curry", [T], [f]); |
|
147 |
||
148 |
(* iterated versions. Nonstandard left-nested tuples arise naturally |
|
149 |
from "split o split o split"*) |
|
150 |
fun curry_n arity = funpow (arity - 1) mk_curry; |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61121
diff
changeset
|
151 |
fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_case_prod; |
40107 | 152 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
153 |
val curry_uncurry_ss = |
69593 | 154 |
simpset_of (put_simpset HOL_basic_ss \<^context> |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61121
diff
changeset
|
155 |
addsimps [@{thm Product_Type.curry_case_prod}, @{thm Product_Type.case_prod_curry}]) |
40107 | 156 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
157 |
val split_conv_ss = |
69593 | 158 |
simpset_of (put_simpset HOL_basic_ss \<^context> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
159 |
addsimps [@{thm Product_Type.split_conv}]); |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
160 |
|
54630
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
54405
diff
changeset
|
161 |
val curry_K_ss = |
69593 | 162 |
simpset_of (put_simpset HOL_basic_ss \<^context> |
54630
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
54405
diff
changeset
|
163 |
addsimps [@{thm Product_Type.curry_K}]); |
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
164 |
|
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
165 |
(* instantiate generic fixpoint induction and eliminate the canonical assumptions; |
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
166 |
curry induction predicate *) |
70325 | 167 |
fun specialize_fixp_induct ctxt fT fT_uc curry uncurry mono_thm f_def rule = |
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
168 |
let |
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
169 |
val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt |
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
170 |
val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0)) |
61113 | 171 |
in |
70324
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
172 |
(* FIXME ctxt vs. ctxt' (!?) *) |
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
173 |
rule |
70324
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
174 |
|> infer_instantiate' ctxt |
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
175 |
((map o Option.map) (Thm.cterm_of ctxt) [SOME uncurry, NONE, SOME curry, NONE, SOME P_inst]) |
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
176 |
|> Tactic.rule_by_tactic ctxt |
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
177 |
(Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 (* discharge U (C f) = f *) |
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
178 |
THEN Simplifier.simp_tac (put_simpset curry_K_ss ctxt) 4 (* simplify bot case *) |
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
179 |
THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *) |
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
180 |
|> (fn thm => thm OF [mono_thm, f_def]) |
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
181 |
|> Conv.fconv_rule (Conv.concl_conv ~1 (* simplify conclusion *) |
70324
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
182 |
(Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}])) |
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
183 |
|> singleton (Variable.export ctxt' ctxt) |
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
184 |
end |
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
185 |
|
52727 | 186 |
fun mk_curried_induct args ctxt inst_rule = |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
187 |
let |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59582
diff
changeset
|
188 |
val cert = Thm.cterm_of ctxt |
70325 | 189 |
(* FIXME ctxt vs. ctxt' (!?) *) |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
190 |
val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
191 |
|
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
192 |
val split_paired_all_conv = |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
193 |
Conv.every_conv (replicate (length args - 1) (Conv.rewr_conv @{thm split_paired_all})) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
194 |
|
61113 | 195 |
val split_params_conv = |
70325 | 196 |
Conv.params_conv ~1 (fn _ => Conv.implies_conv split_paired_all_conv Conv.all_conv) |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
197 |
|
52521
a1c4f586e372
more robust instantiation: extract vars from conclusion instead of relying on fixed overall ordering
krauss
parents:
52087
diff
changeset
|
198 |
val (P_var, x_var) = |
51484
49eb8d73ae10
allow induction predicates with arbitrary arity (not just binary)
krauss
parents:
46961
diff
changeset
|
199 |
Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |
52521
a1c4f586e372
more robust instantiation: extract vars from conclusion instead of relying on fixed overall ordering
krauss
parents:
52087
diff
changeset
|
200 |
|> strip_comb |> apsnd hd |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59936
diff
changeset
|
201 |
|> apply2 dest_Var |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59936
diff
changeset
|
202 |
val P_rangeT = range_type (snd P_var) |
51484
49eb8d73ae10
allow induction predicates with arbitrary arity (not just binary)
krauss
parents:
46961
diff
changeset
|
203 |
val PT = map (snd o dest_Free) args ---> P_rangeT |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
204 |
val x_inst = cert (foldl1 HOLogic.mk_prod args) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
205 |
val P_inst = cert (uncurry_n (length args) (Free (P, PT))) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
206 |
|
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
207 |
val inst_rule' = inst_rule |
70324
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
208 |
|> Tactic.rule_by_tactic ctxt |
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
209 |
(Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 4 |
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
210 |
THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 |
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
211 |
THEN CONVERSION (split_params_conv ctxt |
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
212 |
then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3) |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59936
diff
changeset
|
213 |
|> Thm.instantiate ([], [(P_var, P_inst), (x_var, x_inst)]) |
70324
005c1cdbfd3f
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
wenzelm
parents:
70319
diff
changeset
|
214 |
|> Simplifier.full_simplify (put_simpset split_conv_ss ctxt) |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
215 |
|> singleton (Variable.export ctxt' ctxt) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
216 |
in |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
217 |
inst_rule' |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
218 |
end; |
61113 | 219 |
|
40107 | 220 |
|
221 |
(*** partial_function definition ***) |
|
222 |
||
69829 | 223 |
fun transform_result phi (t, thm) = (Morphism.term phi t, Morphism.thm phi thm); |
224 |
||
40107 | 225 |
fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy = |
226 |
let |
|
43080 | 227 |
val setup_data = the (lookup_mode lthy mode) |
40107 | 228 |
handle Option.Option => error (cat_lines ["Unknown mode " ^ quote mode ^ ".", |
229 |
"Known modes are " ^ commas_quote (known_modes lthy) ^ "."]); |
|
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
230 |
val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data; |
40107 | 231 |
|
63182 | 232 |
val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [], [])] lthy; |
60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset
|
233 |
val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy; |
40107 | 234 |
|
235 |
val ((f_binding, fT), mixfix) = the_single fixes; |
|
62997 | 236 |
val f_bname = Binding.name_of f_binding; |
40107 | 237 |
|
62998 | 238 |
fun note_qualified (name, thms) = |
63005 | 239 |
Local_Theory.note ((derived_name f_binding name, []), thms) #> snd |
62998 | 240 |
|
40107 | 241 |
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn); |
242 |
val (head, args) = strip_comb lhs; |
|
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
243 |
val argnames = map (fst o dest_Free) args; |
40107 | 244 |
val F = fold_rev lambda (head :: args) rhs; |
245 |
||
246 |
val arity = length args; |
|
247 |
val (aTs, bTs) = chop arity (binder_types fT); |
|
248 |
||
249 |
val tupleT = foldl1 HOLogic.mk_prodT aTs; |
|
250 |
val fT_uc = tupleT :: bTs ---> body_type fT; |
|
62997 | 251 |
val f_uc = Var ((f_bname, 0), fT_uc); |
63008 | 252 |
val x_uc = Var (("x", 1), tupleT); |
40107 | 253 |
val uncurry = lambda head (uncurry_n arity head); |
254 |
val curry = lambda f_uc (curry_n arity f_uc); |
|
255 |
||
256 |
val F_uc = |
|
257 |
lambda f_uc (uncurry_n arity (F $ curry_n arity f_uc)); |
|
258 |
||
259 |
val mono_goal = apply_inst lthy mono (lambda f_uc (F_uc $ f_uc $ x_uc)) |
|
260 |
|> HOLogic.mk_Trueprop |
|
261 |
|> Logic.all x_uc; |
|
262 |
||
60784 | 263 |
val mono_thm = Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal) |
40107 | 264 |
(K (mono_tac lthy 1)) |
60784 | 265 |
val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm |
40107 | 266 |
|
267 |
val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc); |
|
61121
efe8b18306b7
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61113
diff
changeset
|
268 |
val f_def_binding = |
62997 | 269 |
Thm.make_def_binding (Config.get lthy Function_Lib.function_internals) f_binding |
270 |
val ((f, (_, f_def)), lthy') = |
|
271 |
Local_Theory.define ((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy; |
|
40107 | 272 |
|
273 |
val eqn = HOLogic.mk_eq (list_comb (f, args), |
|
274 |
Term.betapplys (F, f :: args)) |
|
275 |
|> HOLogic.mk_Trueprop; |
|
276 |
||
277 |
val unfold = |
|
60784 | 278 |
(infer_instantiate' lthy' (map (SOME o Thm.cterm_of lthy') [uncurry, F, curry]) fixp_eq |
52727 | 279 |
OF [inst_mono_thm, f_def]) |
52087
f3075fc4f5f6
more precise treatment of theory vs. Proof.context;
wenzelm
parents:
51717
diff
changeset
|
280 |
|> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1); |
40107 | 281 |
|
61113 | 282 |
val specialized_fixp_induct = |
70325 | 283 |
specialize_fixp_induct lthy' fT fT_uc curry uncurry inst_mono_thm f_def fixp_induct |
62997 | 284 |
|> Drule.rename_bvars' (map SOME (f_bname :: f_bname :: argnames)); |
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
285 |
|
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
286 |
val mk_raw_induct = |
60784 | 287 |
infer_instantiate' args_ctxt |
288 |
((map o Option.map) (Thm.cterm_of args_ctxt) [SOME uncurry, NONE, SOME curry]) |
|
52727 | 289 |
#> mk_curried_induct args args_ctxt |
52087
f3075fc4f5f6
more precise treatment of theory vs. Proof.context;
wenzelm
parents:
51717
diff
changeset
|
290 |
#> singleton (Variable.export args_ctxt lthy') |
60784 | 291 |
#> (fn thm => infer_instantiate' lthy' |
292 |
[SOME (Thm.cterm_of lthy' F)] thm OF [inst_mono_thm, f_def]) |
|
62997 | 293 |
#> Drule.rename_bvars' (map SOME (f_bname :: argnames @ argnames)) |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
294 |
|
52728
470b579f35d2
derive specialized version of full fixpoint induction (with admissibility)
krauss
parents:
52727
diff
changeset
|
295 |
val raw_induct = Option.map mk_raw_induct fixp_induct_user |
62997 | 296 |
val rec_rule = |
297 |
let open Conv in |
|
298 |
Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ => |
|
299 |
CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1 |
|
300 |
THEN resolve_tac lthy' @{thms refl} 1) |
|
301 |
end; |
|
66653 | 302 |
val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule]) |
40107 | 303 |
in |
66653 | 304 |
lthy'' |
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69829
diff
changeset
|
305 |
|> Spec_Rules.add Spec_Rules.equational_recdef ([f], [rec_rule']) |
66653 | 306 |
|> note_qualified ("simps", [rec_rule']) |
62998 | 307 |
|> note_qualified ("mono", [mono_thm]) |
308 |
|> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm])) |
|
309 |
|> note_qualified ("fixp_induct", [specialized_fixp_induct]) |
|
66653 | 310 |
|> pair (f, rec_rule') |
40107 | 311 |
end; |
312 |
||
63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63008
diff
changeset
|
313 |
val add_partial_function = gen_add_partial_function Specification.check_multi_specs; |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63008
diff
changeset
|
314 |
val add_partial_function_cmd = gen_add_partial_function Specification.read_multi_specs; |
40107 | 315 |
|
67149 | 316 |
val mode = \<^keyword>\<open>(\<close> |-- Parse.name --| \<^keyword>\<open>)\<close>; |
40107 | 317 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
318 |
val _ = |
67149 | 319 |
Outer_Syntax.local_theory \<^command_keyword>\<open>partial_function\<close> "define partial function" |
63285 | 320 |
((mode -- (Parse.vars -- (Parse.where_ |-- Parse_Spec.simple_spec))) |
66653 | 321 |
>> (fn (mode, (vars, spec)) => add_partial_function_cmd mode vars spec #> #2)); |
40107 | 322 |
|
61113 | 323 |
end; |