author  blanchet 
Thu, 26 Sep 2013 02:25:33 +0200  
changeset 53904  446076262e92 
parent 53903  27fd72593624 
child 53905  158609f78d0f 
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 > 

12 
thm list > int list > thm list > tactic 

53904  13 
val mk_primcorec_code_of_raw_tac: thm list > thm list > thm > thm list > 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 

53901  17 
val mk_primcorec_sel_tac: Proof.context > thm list > thm > int > int > 
18 
thm list list list > thm list > thm list > thm list > thm list > thm 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 

53902
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset

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

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

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

31 

53329  32 
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

33 
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

34 
HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN 
53329  35 
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

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

37 

53903  38 
fun mk_primcorec_assumption_tac ctxt discIs = 
39 
HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt 

40 
@{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN 

41 
SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' 

42 
resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE' 

43 
dresolve_tac discIs THEN' atac))))); 

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

44 

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

45 
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

46 
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

47 
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

48 

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

49 
fun 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

50 
unfold_thms_tac ctxt @{thms not_not not_False_eq_True} THEN 
53903  51 
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

52 

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

53 
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

54 
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

55 
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

56 
 [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

57 
(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

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

59 

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

60 
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

61 
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

62 

53706  63 
fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss = 
64 
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

65 

53901  66 
fun mk_primcorec_sel_tac ctxt defs f_sel k m exclsss maps map_idents map_comps splits split_asms = 
67 
mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN 

53693  68 
mk_primcorec_cases_tac ctxt k m exclsss THEN 
53900
527ece7edc51
made tactic more flexible w.r.t. case expressions and such
blanchet
parents:
53865
diff
changeset

69 
unfold_thms_tac ctxt (@{thms o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN 
527ece7edc51
made tactic more flexible w.r.t. case expressions and such
blanchet
parents:
53865
diff
changeset

70 
HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' 
527ece7edc51
made tactic more flexible w.r.t. case expressions and such
blanchet
parents:
53865
diff
changeset

71 
eresolve_tac @{thms not_TrueE FalseE} ORELSE' 
53902
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset

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

73 
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

74 
Splitter.split_tac (split_if :: splits) ORELSE' 
53900
527ece7edc51
made tactic more flexible w.r.t. case expressions and such
blanchet
parents:
53865
diff
changeset

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

76 

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

77 
fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs = 
53720  78 
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

79 
(the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN 
53706  80 
unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl); 
81 

53903  82 
fun mk_primcorec_split distincts discIs collapses splits split_asms = 
53904  83 
HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o 
84 
(rtac refl ORELSE' atac ORELSE' 

85 
eresolve_tac (@{thms not_TrueE FalseE} @ map (fn thm => thm RS trans) collapses) ORELSE' 

86 
resolve_tac split_connectI ORELSE' 

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

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

89 
eresolve_tac (map (fn thm => thm RS @{thm neq_eq_eq_contradict}) distincts) THEN' atac ORELSE' 

90 
(TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))); 

53903  91 

92 
fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr = 

53902
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset

93 
HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN 
53706  94 
mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN 
53903  95 
REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN 
96 
mk_primcorec_split distincts discIs collapses splits split_asms; 

53693  97 

53903  98 
fun mk_primcorec_code_of_ctr_tac ctxt distincs discIs collapses splits split_asms ms ctr_thms = 
99 
EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincs discIs collapses splits split_asms) 

100 
ms ctr_thms); 

53693  101 

53904  102 
fun mk_primcorec_code_of_raw_tac splits disc_excludes raw collapses = 
103 
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o 

104 
(rtac refl ORELSE' 

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

106 
resolve_tac split_connectI ORELSE' 

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

108 
etac notE THEN' atac ORELSE' 

53865  109 
dresolve_tac disc_excludes THEN' etac notE THEN' atac ORELSE' 
110 
eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses))); 

53693  111 

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

112 
end; 