author | blanchet |
Wed, 26 Oct 2016 22:40:28 +0200 | |
changeset 64413 | c0d5e78eb647 |
parent 63399 | d1742d1b7f0f |
child 64629 | a331208010b6 |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_tactics.ML |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
General tactics for bounded natural functors. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
signature BNF_TACTICS = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
sig |
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
53692
diff
changeset
|
11 |
include CTR_SUGAR_GENERAL_TACTICS |
49213 | 12 |
|
60728 | 13 |
val fo_rtac: Proof.context -> thm -> int -> tactic |
58332 | 14 |
val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic |
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
58332
diff
changeset
|
15 |
val subst_asm_tac: Proof.context -> int list option -> thm list -> int -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
|
60728 | 17 |
val mk_rotate_eq_tac: Proof.context -> (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> |
18 |
''a list -> int -> tactic |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
|
64413 | 20 |
val mk_pointfree2: Proof.context -> thm -> thm |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
51893
diff
changeset
|
21 |
|
49228 | 22 |
val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm |
23 |
val mk_Abs_inj_thm: thm -> thm |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
|
55756 | 25 |
val mk_map_comp_id_tac: Proof.context -> thm -> tactic |
55197 | 26 |
val mk_map_cong0_tac: Proof.context -> int -> thm -> tactic |
60728 | 27 |
val mk_map_cong0L_tac: Proof.context -> int -> thm -> thm -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
structure BNF_Tactics : BNF_TACTICS = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
|
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
53692
diff
changeset
|
33 |
open Ctr_Sugar_General_Tactics |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
open BNF_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
35 |
|
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55197
diff
changeset
|
36 |
(*stolen from Christian Urban's Cookbook (and adapted slightly)*) |
60728 | 37 |
fun fo_rtac ctxt thm = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
let |
59582 | 39 |
val concl_pat = Drule.strip_imp_concl (Thm.cprop_of thm) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
40 |
val insts = Thm.first_order_match (concl_pat, concl) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
in |
60728 | 42 |
rtac ctxt (Drule.instantiate_normalize insts thm) 1 |
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55197
diff
changeset
|
43 |
end |
60728 | 44 |
handle Pattern.MATCH => no_tac) ctxt; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
|
58332 | 46 |
(*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*) |
47 |
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0]; |
|
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
58332
diff
changeset
|
48 |
fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt o the_default [0]; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
58332
diff
changeset
|
49 |
|
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
51893
diff
changeset
|
50 |
(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) |
64413 | 51 |
fun mk_pointfree2 ctxt thm = thm |
58370
ffc8669e46cf
made 'mk_pointfree' work again in local theories
blanchet
parents:
58352
diff
changeset
|
52 |
|> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58370
diff
changeset
|
53 |
|> apply2 (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp) |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
51893
diff
changeset
|
54 |
|> mk_Trueprop_eq |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
51893
diff
changeset
|
55 |
|> (fn goal => Goal.prove_sorry ctxt [] [] goal |
64413 | 56 |
(K (rtac ctxt ext 1 THEN |
58370
ffc8669e46cf
made 'mk_pointfree' work again in local theories
blanchet
parents:
58352
diff
changeset
|
57 |
unfold_thms_tac ctxt ([o_apply, unfold_thms ctxt [o_apply] (mk_sym thm)]) THEN |
60728 | 58 |
rtac ctxt refl 1))) |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
51893
diff
changeset
|
59 |
|> Thm.close_derivation; |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
51893
diff
changeset
|
60 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
61 |
|
49228 | 62 |
(* Theorems for open typedefs with UNIV as representing set *) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
63 |
|
63399 | 64 |
fun mk_Abs_inj_thm inj = inj OF (replicate 2 @{thm UNIV_I}); |
60728 | 65 |
fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac ctxt surj THEN' etac ctxt exI) 1) |
55067 | 66 |
(Abs_inj_thm RS @{thm bijI'}); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
67 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
69 |
(* General tactic generators *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
70 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
(*applies assoc rule to the lhs of an equation as long as possible*) |
60728 | 72 |
fun mk_flatten_assoc_tac ctxt refl_tac trans assoc cong = rtac ctxt trans 1 THEN |
73 |
REPEAT_DETERM (CHANGED ((FIRST' [rtac ctxt trans THEN' rtac ctxt assoc, rtac ctxt cong THEN' refl_tac]) 1)) THEN |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
74 |
refl_tac 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
75 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
76 |
(*proves two sides of an equation to be equal assuming both are flattened and rhs can be obtained |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
77 |
from lhs by the given permutation of monoms*) |
60728 | 78 |
fun mk_rotate_eq_tac ctxt refl_tac trans assoc com cong = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
80 |
fun gen_tac [] [] = K all_tac |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
81 |
| gen_tac [x] [y] = if x = y then refl_tac else error "mk_rotate_eq_tac: different lists" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
| gen_tac (x :: xs) (y :: ys) = if x = y |
60728 | 83 |
then rtac ctxt cong THEN' refl_tac THEN' gen_tac xs ys |
84 |
else rtac ctxt trans THEN' rtac ctxt com THEN' |
|
85 |
K (mk_flatten_assoc_tac ctxt refl_tac trans assoc cong) THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
gen_tac (xs @ [x]) (y :: ys) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
| gen_tac _ _ = error "mk_rotate_eq_tac: different lists"; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
88 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
gen_tac |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
91 |
|
55756 | 92 |
fun mk_map_comp_id_tac ctxt map_comp0 = |
60728 | 93 |
(rtac ctxt trans THEN' rtac ctxt map_comp0 THEN' K (unfold_thms_tac ctxt @{thms comp_id}) THEN' rtac ctxt refl) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
94 |
|
55197 | 95 |
fun mk_map_cong0_tac ctxt m map_cong0 = |
60728 | 96 |
EVERY' [rtac ctxt mp, rtac ctxt map_cong0, |
63399 | 97 |
CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; |
49284 | 98 |
|
60728 | 99 |
fun mk_map_cong0L_tac ctxt passive map_cong0 map_id = |
100 |
(rtac ctxt trans THEN' rtac ctxt map_cong0 THEN' EVERY' (replicate passive (rtac ctxt refl))) 1 THEN |
|
63399 | 101 |
REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt @{thm bspec}, assume_tac ctxt, |
60752 | 102 |
rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN |
60728 | 103 |
rtac ctxt map_id 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
104 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
end; |