author  blanchet 
Tue, 01 Oct 2013 23:36:02 +0200  
changeset 54018  bd2e127389f2 
parent 53961  16d9ecdf519a 
child 54024  07ab4fd922c2 
permissions  rwrr 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

1 
(* Title: HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

2 
Author: Jasmin Blanchette, TU Muenchen 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

3 
Copyright 2013 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

4 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

5 
Tactics for recursor and corecursor sugar. 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

6 
*) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

7 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

8 
signature BNF_FP_REC_SUGAR_TACTICS = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

9 
sig 
53903  10 
val mk_primcorec_assumption_tac: Proof.context > thm list > tactic 
11 
val mk_primcorec_code_of_ctr_tac: Proof.context > thm list > thm list > thm list > thm list > 

53921  12 
int list > thm list > tactic 
13 
val mk_primcorec_code_of_raw_tac: thm list > thm list > thm > tactic 

53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

14 
val mk_primcorec_ctr_of_dtr_tac: Proof.context > int > thm > thm option > thm list > tactic 
53693  15 
val mk_primcorec_disc_tac: Proof.context > thm list > thm > int > int > thm list list list > 
16 
tactic 

53910  17 
val mk_primcorec_sel_tac: Proof.context > thm list > thm list > thm list > thm list > 
18 
thm list > thm list > thm list > thm > int > int > thm list list list > tactic 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

19 
val mk_primrec_tac: Proof.context > int > thm list > thm list > thm list > thm > tactic 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

20 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

21 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

22 
structure BNF_FP_Rec_Sugar_Tactics : BNF_FP_REC_SUGAR_TACTICS = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

23 
struct 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

24 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

25 
open BNF_Util 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

26 
open BNF_Tactics 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

27 

53905  28 
val falseEs = @{thms not_TrueE FalseE}; 
53910  29 
val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict}; 
53902
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset

30 
val split_if = @{thm split_if}; 
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset

31 
val split_if_asm = @{thm split_if_asm}; 
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset

32 
val split_connectI = @{thms allI impI conjI}; 
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset

33 

53329  34 
fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

35 
unfold_thms_tac ctxt fun_defs THEN 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

36 
HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN 
53329  37 
unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

38 
HEADGOAL (rtac refl); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

39 

53903  40 
fun mk_primcorec_assumption_tac ctxt discIs = 
41 
HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt 

42 
@{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN 

53926  43 
SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE' 
53903  44 
resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE' 
53929  45 
dresolve_tac discIs THEN' atac ORELSE' 
46 
etac notE THEN' atac ORELSE' 

47 
etac disjE))))); 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

48 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

49 
fun mk_primcorec_same_case_tac m = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

50 
HEADGOAL (if m = 0 then rtac TrueI 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

51 
else REPEAT_DETERM_N (m  1) o (rtac conjI THEN' atac) THEN' atac); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

52 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

53 
fun mk_primcorec_different_case_tac ctxt excl = 
53922  54 
unfold_thms_tac ctxt @{thms not_not not_False_eq_True not_True_eq_False} THEN 
53903  55 
HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_assumption_tac ctxt [])); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

56 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

57 
fun mk_primcorec_cases_tac ctxt k m exclsss = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

58 
let val n = length exclsss in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

59 
EVERY (map (fn [] => if k = n then all_tac else mk_primcorec_same_case_tac m 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

60 
 [excl] => mk_primcorec_different_case_tac ctxt excl) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

61 
(take k (nth exclsss (k  1)))) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

62 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

63 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

64 
fun mk_primcorec_prelude ctxt defs thm = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

65 
unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt @{thms split}; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

66 

53706  67 
fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss = 
68 
mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss; 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

69 

53910  70 
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms maps map_idents map_comps f_sel k m 
71 
exclsss = 

53901  72 
mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN 
53693  73 
mk_primcorec_cases_tac ctxt k m exclsss THEN 
54018
bd2e127389f2
strengthened tactic for righthand sides involving lambdas
blanchet
parents:
53961
diff
changeset

74 
unfold_thms_tac ctxt (@{thms id_apply o_def split_def} @ maps @ map_comps @ map_idents) THEN 
bd2e127389f2
strengthened tactic for righthand sides involving lambdas
blanchet
parents:
53961
diff
changeset

75 
HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE' 
53905  76 
eresolve_tac falseEs ORELSE' 
53902
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset

77 
resolve_tac split_connectI ORELSE' 
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset

78 
Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' 
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset

79 
Splitter.split_tac (split_if :: splits) ORELSE' 
53910  80 
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' 
54018
bd2e127389f2
strengthened tactic for righthand sides involving lambdas
blanchet
parents:
53961
diff
changeset

81 
(CHANGED o SELECT_GOAL (unfold_tac @{thms sum.cases} ctxt)) ORELSE' 
53900
527ece7edc51
made tactic more flexible w.r.t. case expressions and such
blanchet
parents:
53865
diff
changeset

82 
etac notE THEN' atac)); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

83 

53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

84 
fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs = 
53720  85 
HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN' 
53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

86 
(the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN 
53706  87 
unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl); 
88 

53908  89 
(* TODO: reduce code duplication with selector tactic above *) 
53921  90 
fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr = 
53905  91 
HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN 
92 
mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN 

93 
REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN 

53929  94 
HEADGOAL (SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o 
53904  95 
(rtac refl ORELSE' atac ORELSE' 
96 
resolve_tac split_connectI ORELSE' 

97 
Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' 

98 
Splitter.split_tac (split_if :: splits) ORELSE' 

53929  99 
K (mk_primcorec_assumption_tac ctxt discIs) ORELSE' 
53910  100 
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' 
53929  101 
(TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))))); 
53903  102 

53921  103 
fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs splits split_asms ms ctr_thms = 
104 
EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) 

105 
ms ctr_thms); 

53693  106 

53921  107 
fun mk_primcorec_code_of_raw_tac splits disc_excludes raw = 
53904  108 
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o 
109 
(rtac refl ORELSE' 

110 
(TRY o rtac sym) THEN' atac ORELSE' 

111 
resolve_tac split_connectI ORELSE' 

112 
Splitter.split_tac (split_if :: splits) ORELSE' 

113 
etac notE THEN' atac ORELSE' 

53921  114 
(TRY o dresolve_tac disc_excludes) THEN' etac notE THEN' atac)); 
115 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

116 
end; 