54026
|
1 |
(* Title: HOL/BNF/Tools/coinduction.ML
|
|
2 |
Author: Johannes Hölzl, TU Muenchen
|
|
3 |
Author: Dmitriy Traytel, TU Muenchen
|
|
4 |
Copyright 2013
|
|
5 |
|
|
6 |
Coinduction method that avoids some boilerplate compared to coinduct.
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature COINDUCTION =
|
|
10 |
sig
|
|
11 |
val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
|
|
12 |
val setup: theory -> theory
|
|
13 |
end;
|
|
14 |
|
|
15 |
structure Coinduction : COINDUCTION =
|
|
16 |
struct
|
|
17 |
|
|
18 |
open BNF_Util
|
|
19 |
open BNF_Tactics
|
|
20 |
|
|
21 |
fun filter_in_out _ [] = ([], [])
|
|
22 |
| filter_in_out P (x :: xs) = (let
|
|
23 |
val (ins, outs) = filter_in_out P xs;
|
|
24 |
in
|
|
25 |
if P x then (x :: ins, outs) else (ins, x :: outs)
|
|
26 |
end);
|
|
27 |
|
|
28 |
fun ALLGOALS_SKIP skip tac st =
|
|
29 |
let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
|
|
30 |
in doall (nprems_of st) st end;
|
|
31 |
|
|
32 |
fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st =
|
|
33 |
st |> (tac1 i THEN (fn st' =>
|
|
34 |
Seq.INTERVAL tac2 (i + skip) (i + nprems_of st' - nprems_of st) st'));
|
|
35 |
|
|
36 |
fun DELETE_PREMS_AFTER skip tac i st =
|
|
37 |
let
|
|
38 |
val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
|
|
39 |
in
|
|
40 |
(THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
|
|
41 |
end;
|
|
42 |
|
|
43 |
fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
|
|
44 |
let
|
|
45 |
val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
|
|
46 |
fun find_coinduct t =
|
|
47 |
Induct.find_coinductP ctxt t @
|
|
48 |
(try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
|
|
49 |
val raw_thm = case opt_raw_thm
|
|
50 |
of SOME raw_thm => raw_thm
|
|
51 |
| NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
|
|
52 |
val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
|
|
53 |
val cases = Rule_Cases.get raw_thm |> fst
|
|
54 |
in
|
|
55 |
NO_CASES (HEADGOAL (
|
|
56 |
Object_Logic.rulify_tac THEN'
|
|
57 |
Method.insert_tac prems THEN'
|
|
58 |
Object_Logic.atomize_prems_tac THEN'
|
|
59 |
DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
|
|
60 |
let
|
|
61 |
val vars = raw_vars @ map (term_of o snd) params;
|
|
62 |
val names_ctxt = ctxt
|
|
63 |
|> fold Variable.declare_names vars
|
|
64 |
|> fold Variable.declare_thm (raw_thm :: prems);
|
|
65 |
val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
|
|
66 |
val (rhoTs, rhots) = Thm.match (thm_concl, concl)
|
|
67 |
|>> map (pairself typ_of)
|
|
68 |
||> map (pairself term_of);
|
|
69 |
val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
|
|
70 |
|> map (subst_atomic_types rhoTs);
|
|
71 |
val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
|
|
72 |
val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
|
|
73 |
|>> (fn names => Variable.variant_fixes names names_ctxt) ;
|
|
74 |
val eqs =
|
|
75 |
map3 (fn name => fn T => fn (_, rhs) =>
|
|
76 |
HOLogic.mk_eq (Free (name, T), rhs))
|
|
77 |
names Ts raw_eqs;
|
|
78 |
val phi = map (HOLogic.dest_Trueprop o prop_of) prems @ eqs
|
|
79 |
|> try (Library.foldr1 HOLogic.mk_conj)
|
|
80 |
|> the_default @{term True}
|
|
81 |
|> list_exists_free vars
|
|
82 |
|> Term.map_abs_vars (Variable.revert_fixed ctxt)
|
|
83 |
|> fold_rev Term.absfree (names ~~ Ts)
|
|
84 |
|> certify ctxt;
|
|
85 |
val thm = cterm_instantiate_pos [SOME phi] raw_thm;
|
|
86 |
val e = length eqs;
|
|
87 |
val p = length prems;
|
|
88 |
in
|
|
89 |
HEADGOAL (EVERY' [rtac thm,
|
|
90 |
EVERY' (map (fn var =>
|
|
91 |
rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
|
|
92 |
EVERY' (map (fn prem => rtac conjI THEN' rtac prem) prems),
|
|
93 |
CONJ_WRAP' (K (rtac refl)) eqs,
|
|
94 |
K (ALLGOALS_SKIP skip
|
|
95 |
(REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
|
|
96 |
DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
|
|
97 |
(case prems of
|
|
98 |
[] => all_tac
|
|
99 |
| inv::case_prems =>
|
|
100 |
let
|
|
101 |
val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
|
|
102 |
val inv_thms = init @ [last];
|
|
103 |
val eqs = drop p inv_thms;
|
|
104 |
fun is_local_var t =
|
|
105 |
member (fn (t, (_, t')) => t aconv (term_of t')) params t;
|
|
106 |
val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
|
|
107 |
val assms = assms' @ take p inv_thms
|
|
108 |
in
|
|
109 |
HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
|
|
110 |
unfold_thms_tac ctxt eqs
|
|
111 |
end)) ctxt)))])
|
|
112 |
end) ctxt) THEN'
|
|
113 |
K (prune_params_tac))) st
|
|
114 |
|> Seq.maps (fn (_, st) =>
|
|
115 |
CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
|
|
116 |
end;
|
|
117 |
|
|
118 |
local
|
|
119 |
|
|
120 |
val ruleN = "rule"
|
|
121 |
val arbitraryN = "arbitrary"
|
|
122 |
fun single_rule [rule] = rule
|
|
123 |
| single_rule _ = error "Single rule expected";
|
|
124 |
|
|
125 |
fun named_rule k arg get =
|
|
126 |
Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
|
|
127 |
(fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
|
|
128 |
(case get (Context.proof_of context) name of SOME x => x
|
|
129 |
| NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
|
|
130 |
|
|
131 |
fun rule get_type get_pred =
|
|
132 |
named_rule Induct.typeN (Args.type_name false) get_type ||
|
|
133 |
named_rule Induct.predN (Args.const false) get_pred ||
|
|
134 |
named_rule Induct.setN (Args.const false) get_pred ||
|
|
135 |
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
|
|
136 |
|
|
137 |
val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;
|
|
138 |
|
|
139 |
fun unless_more_args scan = Scan.unless (Scan.lift
|
|
140 |
((Args.$$$ arbitraryN || Args.$$$ Induct.typeN ||
|
|
141 |
Args.$$$ Induct.predN || Args.$$$ Induct.setN || Args.$$$ ruleN) -- Args.colon)) scan;
|
|
142 |
|
|
143 |
val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
|
|
144 |
Scan.repeat1 (unless_more_args Args.term)) [];
|
|
145 |
|
|
146 |
in
|
|
147 |
|
|
148 |
val setup =
|
|
149 |
Method.setup @{binding coinduction}
|
|
150 |
(arbitrary -- Scan.option coinduct_rule >>
|
|
151 |
(fn (arbitrary, opt_rule) => fn ctxt =>
|
|
152 |
RAW_METHOD_CASES (fn facts =>
|
|
153 |
Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts))))
|
|
154 |
"coinduction on types or predicates/sets";
|
|
155 |
|
|
156 |
end;
|
|
157 |
|
|
158 |
end;
|
|
159 |
|