author | wenzelm |
Fri, 19 Dec 2014 22:53:43 +0100 | |
changeset 59158 | 05cb83f083b9 |
parent 59058 | a78612c67ec0 |
child 59498 | 50b60f501b05 |
permissions | -rw-r--r-- |
54540 | 1 |
(* Title: HOL/Tools/coinduction.ML |
54026 | 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 |
end; |
|
13 |
||
14 |
structure Coinduction : COINDUCTION = |
|
15 |
struct |
|
16 |
||
17 |
fun filter_in_out _ [] = ([], []) |
|
58814 | 18 |
| filter_in_out P (x :: xs) = |
19 |
let |
|
20 |
val (ins, outs) = filter_in_out P xs; |
|
21 |
in |
|
22 |
if P x then (x :: ins, outs) else (ins, x :: outs) |
|
23 |
end; |
|
54026 | 24 |
|
25 |
fun ALLGOALS_SKIP skip tac st = |
|
26 |
let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1) |
|
27 |
in doall (nprems_of st) st end; |
|
28 |
||
29 |
fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st = |
|
30 |
st |> (tac1 i THEN (fn st' => |
|
31 |
Seq.INTERVAL tac2 (i + skip) (i + nprems_of st' - nprems_of st) st')); |
|
32 |
||
33 |
fun DELETE_PREMS_AFTER skip tac i st = |
|
34 |
let |
|
35 |
val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length; |
|
36 |
in |
|
58839 | 37 |
(THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve_tac [thin_rl])) i st |
54026 | 38 |
end; |
39 |
||
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55954
diff
changeset
|
40 |
fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) => |
54026 | 41 |
let |
42 |
val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst; |
|
58814 | 43 |
fun find_coinduct t = |
54026 | 44 |
Induct.find_coinductP ctxt t @ |
45 |
(try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default []) |
|
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55954
diff
changeset
|
46 |
val raw_thm = |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55954
diff
changeset
|
47 |
(case opt_raw_thm of |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55954
diff
changeset
|
48 |
SOME raw_thm => raw_thm |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55954
diff
changeset
|
49 |
| NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd); |
54026 | 50 |
val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1 |
51 |
val cases = Rule_Cases.get raw_thm |> fst |
|
52 |
in |
|
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55954
diff
changeset
|
53 |
HEADGOAL ( |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54540
diff
changeset
|
54 |
Object_Logic.rulify_tac ctxt THEN' |
54026 | 55 |
Method.insert_tac prems THEN' |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54540
diff
changeset
|
56 |
Object_Logic.atomize_prems_tac ctxt THEN' |
54026 | 57 |
DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} => |
58 |
let |
|
59 |
val vars = raw_vars @ map (term_of o snd) params; |
|
60 |
val names_ctxt = ctxt |
|
61 |
|> fold Variable.declare_names vars |
|
62 |
|> fold Variable.declare_thm (raw_thm :: prems); |
|
63 |
val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl; |
|
64 |
val (rhoTs, rhots) = Thm.match (thm_concl, concl) |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58839
diff
changeset
|
65 |
|>> map (apply2 typ_of) |
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58839
diff
changeset
|
66 |
||> map (apply2 term_of); |
54026 | 67 |
val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd |
68 |
|> map (subst_atomic_types rhoTs); |
|
69 |
val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs; |
|
70 |
val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs |
|
71 |
|>> (fn names => Variable.variant_fixes names names_ctxt) ; |
|
72 |
val eqs = |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58002
diff
changeset
|
73 |
@{map 3} (fn name => fn T => fn (_, rhs) => |
54026 | 74 |
HOLogic.mk_eq (Free (name, T), rhs)) |
75 |
names Ts raw_eqs; |
|
54366
13bfdbcfbbfb
swap equations and premises in the coinductive step for better proof automation
Andreas Lochbihler
parents:
54026
diff
changeset
|
76 |
val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems |
54026 | 77 |
|> try (Library.foldr1 HOLogic.mk_conj) |
78 |
|> the_default @{term True} |
|
59158 | 79 |
|> Ctr_Sugar_Util.list_exists_free vars |
54026 | 80 |
|> Term.map_abs_vars (Variable.revert_fixed ctxt) |
81 |
|> fold_rev Term.absfree (names ~~ Ts) |
|
59158 | 82 |
|> Ctr_Sugar_Util.certify ctxt; |
83 |
val thm = Ctr_Sugar_Util.cterm_instantiate_pos [SOME phi] raw_thm; |
|
54026 | 84 |
val e = length eqs; |
85 |
val p = length prems; |
|
86 |
in |
|
58839 | 87 |
HEADGOAL (EVERY' [resolve_tac [thm], |
54026 | 88 |
EVERY' (map (fn var => |
59158 | 89 |
resolve_tac |
90 |
[Ctr_Sugar_Util.cterm_instantiate_pos |
|
91 |
[NONE, SOME (Ctr_Sugar_Util.certify ctxt var)] exI]) vars), |
|
92 |
if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac [refl])) eqs |
|
58839 | 93 |
else |
94 |
REPEAT_DETERM_N e o (resolve_tac [conjI] THEN' resolve_tac [refl]) THEN' |
|
59158 | 95 |
Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac o single) prems, |
54026 | 96 |
K (ALLGOALS_SKIP skip |
58839 | 97 |
(REPEAT_DETERM_N (length vars) o (eresolve_tac [exE] THEN' rotate_tac ~1) THEN' |
54026 | 98 |
DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} => |
99 |
(case prems of |
|
100 |
[] => all_tac |
|
101 |
| inv::case_prems => |
|
102 |
let |
|
103 |
val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv; |
|
104 |
val inv_thms = init @ [last]; |
|
54366
13bfdbcfbbfb
swap equations and premises in the coinductive step for better proof automation
Andreas Lochbihler
parents:
54026
diff
changeset
|
105 |
val eqs = take e inv_thms; |
58814 | 106 |
fun is_local_var t = |
54026 | 107 |
member (fn (t, (_, t')) => t aconv (term_of t')) params t; |
108 |
val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs; |
|
54366
13bfdbcfbbfb
swap equations and premises in the coinductive step for better proof automation
Andreas Lochbihler
parents:
54026
diff
changeset
|
109 |
val assms = assms' @ drop e inv_thms |
54026 | 110 |
in |
111 |
HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN |
|
59158 | 112 |
Ctr_Sugar_General_Tactics.unfold_thms_tac ctxt eqs |
54026 | 113 |
end)) ctxt)))]) |
114 |
end) ctxt) THEN' |
|
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55954
diff
changeset
|
115 |
K (prune_params_tac ctxt)) |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55954
diff
changeset
|
116 |
#> Seq.maps (fn st => |
54026 | 117 |
CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st) |
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55954
diff
changeset
|
118 |
end)); |
54026 | 119 |
|
120 |
local |
|
121 |
||
122 |
val ruleN = "rule" |
|
123 |
val arbitraryN = "arbitrary" |
|
124 |
fun single_rule [rule] = rule |
|
125 |
| single_rule _ = error "Single rule expected"; |
|
126 |
||
127 |
fun named_rule k arg get = |
|
128 |
Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|-- |
|
129 |
(fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name => |
|
130 |
(case get (Context.proof_of context) name of SOME x => x |
|
131 |
| NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))); |
|
132 |
||
133 |
fun rule get_type get_pred = |
|
55951
c07d184aebe9
tuned signature -- more uniform check_type_name/read_type_name;
wenzelm
parents:
54742
diff
changeset
|
134 |
named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type || |
55954 | 135 |
named_rule Induct.predN (Args.const {proper = false, strict = false}) get_pred || |
136 |
named_rule Induct.setN (Args.const {proper = false, strict = false}) get_pred || |
|
54026 | 137 |
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms; |
138 |
||
59158 | 139 |
val coinduct_rule = |
140 |
rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule; |
|
54026 | 141 |
|
142 |
fun unless_more_args scan = Scan.unless (Scan.lift |
|
143 |
((Args.$$$ arbitraryN || Args.$$$ Induct.typeN || |
|
144 |
Args.$$$ Induct.predN || Args.$$$ Induct.setN || Args.$$$ ruleN) -- Args.colon)) scan; |
|
145 |
||
146 |
val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |-- |
|
147 |
Scan.repeat1 (unless_more_args Args.term)) []; |
|
148 |
||
149 |
in |
|
150 |
||
58814 | 151 |
val _ = |
152 |
Theory.setup |
|
153 |
(Method.setup @{binding coinduction} |
|
154 |
(arbitrary -- Scan.option coinduct_rule >> |
|
155 |
(fn (arbitrary, opt_rule) => fn ctxt => fn facts => |
|
156 |
Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts))) |
|
157 |
"coinduction on types or predicates/sets"); |
|
54026 | 158 |
|
159 |
end; |
|
160 |
||
161 |
end; |
|
162 |