author | wenzelm |
Fri, 09 Aug 2019 17:14:49 +0200 | |
changeset 70494 | 41108e3e9ca5 |
parent 69593 | 3dda49e08b9d |
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 |
64629 | 14 |
val clean_blast_tac: Proof.context -> int -> tactic |
58332 | 15 |
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
|
16 |
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
|
17 |
|
60728 | 18 |
val mk_rotate_eq_tac: Proof.context -> (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> |
19 |
''a list -> int -> tactic |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
20 |
|
64413 | 21 |
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
|
22 |
|
49228 | 23 |
val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm |
24 |
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
|
25 |
|
55756 | 26 |
val mk_map_comp_id_tac: Proof.context -> thm -> tactic |
55197 | 27 |
val mk_map_cong0_tac: Proof.context -> int -> thm -> tactic |
60728 | 28 |
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
|
29 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
structure BNF_Tactics : BNF_TACTICS = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
33 |
|
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
53692
diff
changeset
|
34 |
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
|
35 |
open BNF_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
|
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55197
diff
changeset
|
37 |
(*stolen from Christian Urban's Cookbook (and adapted slightly)*) |
60728 | 38 |
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
|
39 |
let |
59582 | 40 |
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
|
41 |
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
|
42 |
in |
60728 | 43 |
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
|
44 |
end |
60728 | 45 |
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
|
46 |
|
69593 | 47 |
fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of \<^theory_context>\<open>HOL\<close>) ctxt); |
64629 | 48 |
|
58332 | 49 |
(*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*) |
50 |
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
|
51 |
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
|
52 |
|
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
51893
diff
changeset
|
53 |
(*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 | 54 |
fun mk_pointfree2 ctxt thm = thm |
58370
ffc8669e46cf
made 'mk_pointfree' work again in local theories
blanchet
parents:
58352
diff
changeset
|
55 |
|> 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
|
56 |
|> 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
|
57 |
|> mk_Trueprop_eq |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
51893
diff
changeset
|
58 |
|> (fn goal => Goal.prove_sorry ctxt [] [] goal |
64413 | 59 |
(K (rtac ctxt ext 1 THEN |
58370
ffc8669e46cf
made 'mk_pointfree' work again in local theories
blanchet
parents:
58352
diff
changeset
|
60 |
unfold_thms_tac ctxt ([o_apply, unfold_thms ctxt [o_apply] (mk_sym thm)]) THEN |
60728 | 61 |
rtac ctxt refl 1))) |
70494 | 62 |
|> Thm.close_derivation \<^here>; |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
51893
diff
changeset
|
63 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
|
49228 | 65 |
(* 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
|
66 |
|
63399 | 67 |
fun mk_Abs_inj_thm inj = inj OF (replicate 2 @{thm UNIV_I}); |
60728 | 68 |
fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac ctxt surj THEN' etac ctxt exI) 1) |
55067 | 69 |
(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
|
70 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
72 |
(* General tactic generators *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
73 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
74 |
(*applies assoc rule to the lhs of an equation as long as possible*) |
60728 | 75 |
fun mk_flatten_assoc_tac ctxt refl_tac trans assoc cong = rtac ctxt trans 1 THEN |
76 |
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
|
77 |
refl_tac 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
78 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
(*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
|
80 |
from lhs by the given permutation of monoms*) |
60728 | 81 |
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
|
82 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
83 |
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
|
84 |
| 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
|
85 |
| gen_tac (x :: xs) (y :: ys) = if x = y |
60728 | 86 |
then rtac ctxt cong THEN' refl_tac THEN' gen_tac xs ys |
87 |
else rtac ctxt trans THEN' rtac ctxt com THEN' |
|
88 |
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
|
89 |
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
|
90 |
| 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
|
91 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
92 |
gen_tac |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
94 |
|
55756 | 95 |
fun mk_map_comp_id_tac ctxt map_comp0 = |
60728 | 96 |
(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
|
97 |
|
55197 | 98 |
fun mk_map_cong0_tac ctxt m map_cong0 = |
60728 | 99 |
EVERY' [rtac ctxt mp, rtac ctxt map_cong0, |
63399 | 100 |
CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; |
49284 | 101 |
|
60728 | 102 |
fun mk_map_cong0L_tac ctxt passive map_cong0 map_id = |
103 |
(rtac ctxt trans THEN' rtac ctxt map_cong0 THEN' EVERY' (replicate passive (rtac ctxt refl))) 1 THEN |
|
63399 | 104 |
REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt @{thm bspec}, assume_tac ctxt, |
60752 | 105 |
rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN |
60728 | 106 |
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
|
107 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
108 |
end; |