author | wenzelm |
Sun, 13 Dec 2015 21:56:15 +0100 | |
changeset 61841 | 4d3527b94f2a |
parent 61340 | ce74c00de6b7 |
child 67149 | e61557884799 |
permissions | -rw-r--r-- |
33471 | 1 |
(* Title: HOL/Tools/Function/induction_schema.ML |
2 |
Author: Alexander Krauss, TU Muenchen |
|
3 |
||
4 |
A method to prove induction schemas. |
|
5 |
*) |
|
6 |
||
7 |
signature INDUCTION_SCHEMA = |
|
8 |
sig |
|
9 |
val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic) |
|
10 |
-> Proof.context -> thm list -> tactic |
|
11 |
val induction_schema_tac : Proof.context -> thm list -> tactic |
|
12 |
end |
|
13 |
||
14 |
structure Induction_Schema : INDUCTION_SCHEMA = |
|
15 |
struct |
|
16 |
||
17 |
open Function_Lib |
|
18 |
||
19 |
type rec_call_info = int * (string * typ) list * term list * term list |
|
20 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
21 |
datatype scheme_case = SchemeCase of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
22 |
{bidx : int, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
23 |
qs: (string * typ) list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
24 |
oqnames: string list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
25 |
gs: term list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
26 |
lhs: term list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
27 |
rs: rec_call_info list} |
33471 | 28 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
29 |
datatype scheme_branch = SchemeBranch of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
30 |
{P : term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
31 |
xs: (string * typ) list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
32 |
ws: (string * typ) list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
33 |
Cs: term list} |
33471 | 34 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
35 |
datatype ind_scheme = IndScheme of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
36 |
{T: typ, (* sum of products *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
37 |
branches: scheme_branch list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
38 |
cases: scheme_case list} |
33471 | 39 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52467
diff
changeset
|
40 |
fun ind_atomize ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_atomize} |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52467
diff
changeset
|
41 |
fun ind_rulify ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_rulify} |
33471 | 42 |
|
43 |
fun meta thm = thm RS eq_reflection |
|
44 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52467
diff
changeset
|
45 |
fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true |
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
54742
diff
changeset
|
46 |
(map meta (@{thm split_conv} :: @{thms sum.case})) |
33471 | 47 |
|
59627 | 48 |
fun term_conv ctxt cv t = |
49 |
cv (Thm.cterm_of ctxt t) |
|
59582 | 50 |
|> Thm.prop_of |> Logic.dest_equals |> snd |
33471 | 51 |
|
52 |
fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)) |
|
53 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
54 |
fun dest_hhf ctxt t = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
55 |
let |
60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
59970
diff
changeset
|
56 |
val ((params, imp), ctxt') = Variable.focus NONE t ctxt |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
57 |
in |
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
wenzelm
parents:
42361
diff
changeset
|
58 |
(ctxt', map #2 params, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
59 |
end |
33471 | 60 |
|
61 |
fun mk_scheme' ctxt cases concl = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
62 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
63 |
fun mk_branch concl = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
64 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
65 |
val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
66 |
val (P, xs) = strip_comb Pxs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
67 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
68 |
SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs } |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
69 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
70 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
71 |
val (branches, cases') = (* correction *) |
41418 | 72 |
case Logic.dest_conjunctions concl of |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
73 |
[conc] => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
74 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
75 |
val _ $ Pxs = Logic.strip_assums_concl conc |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
76 |
val (P, _) = strip_comb Pxs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
77 |
val (cases', conds) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
78 |
take_prefix (Term.exists_subterm (curry op aconv P)) cases |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
79 |
val concl' = fold_rev (curry Logic.mk_implies) conds conc |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
80 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
81 |
([mk_branch concl'], cases') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
82 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
83 |
| concls => (map mk_branch concls, cases) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
84 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
85 |
fun mk_case premise = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
86 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
87 |
val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
88 |
val (P, lhs) = strip_comb Plhs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
89 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
90 |
fun bidx Q = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
91 |
find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
92 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
93 |
fun mk_rcinfo pr = |
33471 | 94 |
let |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
95 |
val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
96 |
val (P', rcs) = strip_comb Phyp |
33471 | 97 |
in |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
98 |
(bidx P', Gvs, Gas, rcs) |
33471 | 99 |
end |
100 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
101 |
fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches |
33471 | 102 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
103 |
val (gs, rcprs) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
104 |
take_prefix (not o Term.exists_subterm is_pred) prems |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
105 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
106 |
SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
107 |
gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
108 |
end |
33471 | 109 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
110 |
fun PT_of (SchemeBranch { xs, ...}) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
111 |
foldr1 HOLogic.mk_prodT (map snd xs) |
33471 | 112 |
|
55968 | 113 |
val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) (map PT_of branches) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
114 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
115 |
IndScheme {T=ST, cases=map mk_case cases', branches=branches } |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
116 |
end |
33471 | 117 |
|
118 |
fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
119 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
120 |
val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
121 |
val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
122 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
123 |
val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
124 |
val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) |
42361 | 125 |
val Cs' = map (Pattern.rewrite_term (Proof_Context.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs |
33471 | 126 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
127 |
fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = |
33471 | 128 |
HOLogic.mk_Trueprop Pbool |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
129 |
|> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
130 |
(xs' ~~ lhs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
131 |
|> fold_rev (curry Logic.mk_implies) gs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
132 |
|> fold_rev mk_forall_rename (oqnames ~~ map Free qs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
133 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
134 |
HOLogic.mk_Trueprop Pbool |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
135 |
|> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
136 |
|> fold_rev (curry Logic.mk_implies) Cs' |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
137 |
|> fold_rev (Logic.all o Free) ws |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
138 |
|> fold_rev mk_forall_rename (map fst xs ~~ xs') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
139 |
|> mk_forall_rename ("P", Pbool) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
140 |
end |
33471 | 141 |
|
33855
cd8acf137c9c
eliminated dead code and some unused bindings, reported by polyml
krauss
parents:
33697
diff
changeset
|
142 |
fun mk_wf R (IndScheme {T, ...}) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
143 |
HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R) |
33471 | 144 |
|
61340 | 145 |
fun mk_ineqs R thesisn (IndScheme {T, cases, branches}) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
146 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
147 |
fun inject i ts = |
55968 | 148 |
Sum_Tree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts) |
33471 | 149 |
|
61340 | 150 |
val thesis = Free (thesisn, HOLogic.boolT) |
33471 | 151 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
152 |
fun mk_pres bdx args = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
153 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
154 |
val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
155 |
fun replace (x, v) t = betapply (lambda (Free x) t, v) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
156 |
val Cs' = map (fold replace (xs ~~ args)) Cs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
157 |
val cse = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
158 |
HOLogic.mk_Trueprop thesis |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
159 |
|> fold_rev (curry Logic.mk_implies) Cs' |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
160 |
|> fold_rev (Logic.all o Free) ws |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
161 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
162 |
Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
163 |
end |
33471 | 164 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
165 |
fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
166 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
167 |
fun g (bidx', Gvs, Gas, rcarg) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
168 |
let val export = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
169 |
fold_rev (curry Logic.mk_implies) Gas |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
170 |
#> fold_rev (curry Logic.mk_implies) gs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
171 |
#> fold_rev (Logic.all o Free) Gvs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
172 |
#> fold_rev mk_forall_rename (oqnames ~~ map Free qs) |
33471 | 173 |
in |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
174 |
(HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
175 |
|> HOLogic.mk_Trueprop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
176 |
|> export, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
177 |
mk_pres bidx' rcarg |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
178 |
|> export |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
179 |
|> Logic.all thesis) |
33471 | 180 |
end |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
181 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
182 |
map g rs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
183 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
184 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
185 |
map f cases |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
186 |
end |
33471 | 187 |
|
188 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52467
diff
changeset
|
189 |
fun mk_ind_goal ctxt branches = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
190 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
191 |
fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
192 |
HOLogic.mk_Trueprop (list_comb (P, map Free xs)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
193 |
|> fold_rev (curry Logic.mk_implies) Cs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
194 |
|> fold_rev (Logic.all o Free) ws |
59627 | 195 |
|> term_conv ctxt (ind_atomize ctxt) |
59970 | 196 |
|> Object_Logic.drop_judgment ctxt |
39756
6c8e83d94536
consolidated tupled_lambda; moved to structure HOLogic
krauss
parents:
37677
diff
changeset
|
197 |
|> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
198 |
in |
55968 | 199 |
Sum_Tree.mk_sumcases HOLogic.boolT (map brnch branches) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
200 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
201 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
202 |
fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
203 |
(IndScheme {T, cases=scases, branches}) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
204 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
205 |
val n = length branches |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
206 |
val scases_idx = map_index I scases |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
207 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
208 |
fun inject i ts = |
55968 | 209 |
Sum_Tree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
210 |
val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
211 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52467
diff
changeset
|
212 |
val P_comp = mk_ind_goal ctxt branches |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
213 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
214 |
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
46217
7b19666f0e3d
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
wenzelm
parents:
42495
diff
changeset
|
215 |
val ihyp = Logic.all_const T $ Abs ("z", T, |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
216 |
Logic.mk_implies |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
217 |
(HOLogic.mk_Trueprop ( |
37677 | 218 |
Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
219 |
$ (HOLogic.pair_const T T $ Bound 0 $ x) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
220 |
$ R), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
221 |
HOLogic.mk_Trueprop (P_comp $ Bound 0))) |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
222 |
|> Thm.cterm_of ctxt |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
223 |
|
36945 | 224 |
val aihyp = Thm.assume ihyp |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
225 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
226 |
(* Rule for case splitting along the sum types *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
227 |
val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
228 |
val pats = map_index (uncurry inject) xss |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
229 |
val sum_split_rule = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
230 |
Pat_Completeness.prove_completeness ctxt [x] (P_comp $ x) xss (map single pats) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
231 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
232 |
fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
233 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
234 |
val fxs = map Free xs |
59618 | 235 |
val branch_hyp = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
236 |
Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
237 |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
238 |
val C_hyps = map (Thm.cterm_of ctxt #> Thm.assume) Cs |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
239 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
240 |
val (relevant_cases, ineqss') = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
241 |
(scases_idx ~~ ineqss) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
242 |
|> filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
243 |
|> split_list |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
244 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
245 |
fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
246 |
let |
36945 | 247 |
val case_hyps = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
248 |
map (Thm.assume o Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) |
59618 | 249 |
(fxs ~~ lhs) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
250 |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
251 |
val cqs = map (Thm.cterm_of ctxt o Free) qs |
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
252 |
val ags = map (Thm.assume o Thm.cterm_of ctxt) gs |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
253 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
254 |
val replace_x_simpset = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
255 |
put_simpset HOL_basic_ss ctxt addsimps (branch_hyp :: case_hyps) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
256 |
val sih = full_simplify replace_x_simpset aihyp |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
257 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
258 |
fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
259 |
let |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
260 |
val cGas = map (Thm.assume o Thm.cterm_of ctxt) Gas |
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
261 |
val cGvs = map (Thm.cterm_of ctxt o Free) Gvs |
36945 | 262 |
val import = fold Thm.forall_elim (cqs @ cGvs) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
263 |
#> fold Thm.elim_implies (ags @ cGas) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
264 |
val ipres = pres |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
265 |
|> Thm.forall_elim (Thm.cterm_of ctxt (list_comb (P_of idx, rcargs))) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
266 |
|> import |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
267 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
268 |
sih |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
269 |
|> Thm.forall_elim (Thm.cterm_of ctxt (inject idx rcargs)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
270 |
|> Thm.elim_implies (import ineq) (* Psum rcargs *) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52467
diff
changeset
|
271 |
|> Conv.fconv_rule (sum_prod_conv ctxt) |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52467
diff
changeset
|
272 |
|> Conv.fconv_rule (ind_rulify ctxt) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
273 |
|> (fn th => th COMP ipres) (* P rs *) |
59582 | 274 |
|> fold_rev (Thm.implies_intr o Thm.cprop_of) cGas |
36945 | 275 |
|> fold_rev Thm.forall_intr cGvs |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
276 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
277 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
278 |
val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
279 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
280 |
val step = HOLogic.mk_Trueprop (list_comb (P, lhs)) |
59582 | 281 |
|> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
282 |
|> fold_rev (curry Logic.mk_implies) gs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
283 |
|> fold_rev (Logic.all o Free) qs |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
284 |
|> Thm.cterm_of ctxt |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
285 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
286 |
val Plhs_to_Pxs_conv = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
287 |
foldl1 (uncurry Conv.combination_conv) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
288 |
(Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
289 |
|
36945 | 290 |
val res = Thm.assume step |
291 |
|> fold Thm.forall_elim cqs |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
292 |
|> fold Thm.elim_implies ags |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
293 |
|> fold Thm.elim_implies P_recs (* P lhs *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
294 |
|> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *) |
59582 | 295 |
|> fold_rev (Thm.implies_intr o Thm.cprop_of) (ags @ case_hyps) |
36945 | 296 |
|> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
297 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
298 |
(res, (cidx, step)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
299 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
300 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
301 |
val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
302 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
303 |
val bstep = complete_thm |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
304 |
|> Thm.forall_elim (Thm.cterm_of ctxt (list_comb (P, fxs))) |
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
305 |
|> fold (Thm.forall_elim o Thm.cterm_of ctxt) (fxs @ map Free ws) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
306 |
|> fold Thm.elim_implies C_hyps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
307 |
|> fold Thm.elim_implies cases (* P xs *) |
59582 | 308 |
|> fold_rev (Thm.implies_intr o Thm.cprop_of) C_hyps |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
309 |
|> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) ws |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
310 |
|
59618 | 311 |
val Pxs = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
312 |
Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P_comp $ x)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
313 |
|> Goal.init |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52467
diff
changeset
|
314 |
|> (Simplifier.rewrite_goals_tac ctxt |
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
54742
diff
changeset
|
315 |
(map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.case})) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52467
diff
changeset
|
316 |
THEN CONVERSION (ind_rulify ctxt) 1) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
317 |
|> Seq.hd |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
318 |
|> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
319 |
|> Goal.finish ctxt |
59582 | 320 |
|> Thm.implies_intr (Thm.cprop_of branch_hyp) |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
321 |
|> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) fxs |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
322 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
323 |
(Pxs, steps) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
324 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
325 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
326 |
val (branches, steps) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
327 |
map_index prove_branch (branches ~~ (complete_thms ~~ pats)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
328 |
|> split_list |> apsnd flat |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
329 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
330 |
val istep = sum_split_rule |
52467 | 331 |
|> fold (fn b => fn th => Drule.compose (b, 1, th)) branches |
36945 | 332 |
|> Thm.implies_intr ihyp |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
333 |
|> Thm.forall_intr (Thm.cterm_of ctxt x) (* "!!x. (!!y<x. P y) ==> P x" *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
334 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
335 |
val induct_rule = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
336 |
@{thm "wf_induct_rule"} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
337 |
|> (curry op COMP) wf_thm |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
338 |
|> (curry op COMP) istep |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
339 |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58963
diff
changeset
|
340 |
val steps_sorted = map snd (sort (int_ord o apply2 fst) steps) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
341 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
342 |
(steps_sorted, induct_rule) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
343 |
end |
33471 | 344 |
|
345 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
346 |
fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = |
46467 | 347 |
(* FIXME proper use of facts!? *) |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61340
diff
changeset
|
348 |
(ALLGOALS (Method.insert_tac ctxt facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) => |
33471 | 349 |
let |
350 |
val (ctxt', _, cases, concl) = dest_hhf ctxt t |
|
351 |
val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl |
|
61340 | 352 |
val ([Rn, xn, thesisn], ctxt'') = Variable.variant_fixes ["R", "x", "thesis"] ctxt' |
33471 | 353 |
val R = Free (Rn, mk_relT ST) |
354 |
val x = Free (xn, ST) |
|
355 |
||
59618 | 356 |
val ineqss = |
61340 | 357 |
mk_ineqs R thesisn scheme |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
358 |
|> map (map (apply2 (Thm.assume o Thm.cterm_of ctxt''))) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
359 |
val complete = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
360 |
map_range (mk_completeness ctxt'' scheme #> Thm.cterm_of ctxt'' #> Thm.assume) |
59618 | 361 |
(length branches) |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
362 |
val wf_thm = mk_wf R scheme |> Thm.cterm_of ctxt'' |> Thm.assume |
33471 | 363 |
|
364 |
val (descent, pres) = split_list (flat ineqss) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
365 |
val newgoals = complete @ pres @ wf_thm :: descent |
33471 | 366 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
367 |
val (steps, indthm) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
368 |
mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme |
33471 | 369 |
|
370 |
fun project (i, SchemeBranch {xs, ...}) = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
371 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
372 |
val inst = (foldr1 HOLogic.mk_prod (map Free xs)) |
55968 | 373 |
|> Sum_Tree.mk_inj ST (length branches) (i + 1) |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
374 |
|> Thm.cterm_of ctxt'' |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
375 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
376 |
indthm |
60801 | 377 |
|> Thm.instantiate' [] [SOME inst] |
55968 | 378 |
|> simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt'') |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52467
diff
changeset
|
379 |
|> Conv.fconv_rule (ind_rulify ctxt'') |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
380 |
end |
33471 | 381 |
|
382 |
val res = Conjunction.intr_balanced (map_index project branches) |
|
59582 | 383 |
|> fold_rev Thm.implies_intr (map Thm.cprop_of newgoals @ steps) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
384 |
|> Drule.generalize ([], [Rn]) |
33471 | 385 |
|
386 |
val nbranches = length branches |
|
387 |
val npres = length pres |
|
388 |
in |
|
59618 | 389 |
Thm.bicompose (SOME ctxt'') {flatten = false, match = false, incremented = false} |
52223
5bb6ae8acb87
tuned signature -- more explicit flags for low-level Thm.bicompose;
wenzelm
parents:
51717
diff
changeset
|
390 |
(false, res, length newgoals) i |
33471 | 391 |
THEN term_tac (i + nbranches + npres) |
392 |
THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches)))) |
|
393 |
THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i))) |
|
394 |
end)) |
|
395 |
||
396 |
||
397 |
fun induction_schema_tac ctxt = |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58950
diff
changeset
|
398 |
mk_ind_tac (K all_tac) (assume_tac ctxt APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; |
33471 | 399 |
|
400 |
end |