author  blanchet 
Thu, 26 Sep 2013 15:13:55 +0200  
changeset 53921  46fc95abef09 
parent 53910  2c5055a3583d 
child 53922  6d40f6e69686 
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 

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

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

45 
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

46 

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

47 
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

48 
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

49 
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

50 

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

51 
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

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

54 

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

55 
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

56 
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

57 
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

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

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

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

61 

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

62 
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

63 
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

64 

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

67 

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

53901  70 
mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN 
53693  71 
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

72 
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

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

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

76 
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

77 
Splitter.split_tac (split_if :: splits) ORELSE' 
53910  78 
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' 
53900
527ece7edc51
made tactic more flexible w.r.t. case expressions and such
blanchet
parents:
53865
diff
changeset

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

80 

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

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

83 
(the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN 
53706  84 
unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl); 
85 

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

90 
REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN 

53904  91 
HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o 
92 
(rtac refl ORELSE' atac ORELSE' 

93 
resolve_tac split_connectI ORELSE' 

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

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

53910  96 
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' 
53904  97 
(TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))); 
53903  98 

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

101 
ms ctr_thms); 

53693  102 

53921  103 
fun mk_primcorec_code_of_raw_tac splits disc_excludes raw = 
53904  104 
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o 
105 
(rtac refl ORELSE' 

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

107 
resolve_tac split_connectI ORELSE' 

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

109 
etac notE THEN' atac ORELSE' 

53921  110 
(TRY o dresolve_tac disc_excludes) THEN' etac notE THEN' atac)); 
111 

53693  112 

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

113 
end; 