11 val mk_case_cong_tac: thm -> thm list -> tactic |
11 val mk_case_cong_tac: thm -> thm list -> tactic |
12 val mk_case_eq_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list -> |
12 val mk_case_eq_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list -> |
13 tactic |
13 tactic |
14 val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic |
14 val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic |
15 val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic |
15 val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic |
|
16 val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list -> |
|
17 thm list list list -> thm list list list -> tactic |
16 val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic |
18 val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic |
17 val mk_nchotomy_tac: int -> thm -> tactic |
19 val mk_nchotomy_tac: int -> thm -> tactic |
18 val mk_other_half_disc_exclude_tac: thm -> tactic |
20 val mk_other_half_disc_exclude_tac: thm -> tactic |
19 val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic |
21 val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic |
20 val mk_split_asm_tac: Proof.context -> thm -> tactic |
22 val mk_split_asm_tac: Proof.context -> thm -> tactic |
25 struct |
27 struct |
26 |
28 |
27 open BNF_Util |
29 open BNF_Util |
28 open BNF_Tactics |
30 open BNF_Tactics |
29 |
31 |
|
32 val meta_mp = @{thm meta_mp}; |
|
33 |
30 fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P}); |
34 fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P}); |
31 |
35 |
32 fun mk_nchotomy_tac n exhaust = |
36 fun mk_nchotomy_tac n exhaust = |
33 (rtac allI THEN' rtac exhaust THEN' |
37 (rtac allI THEN' rtac exhaust THEN' |
34 EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; |
38 EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; |
35 |
39 |
36 fun mk_unique_disc_def_tac m exhaust' = |
40 fun mk_unique_disc_def_tac m uexhaust = |
37 EVERY' [rtac iffI, rtac exhaust', REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1; |
41 EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1; |
38 |
42 |
39 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct exhaust' = |
43 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust = |
40 EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE, |
44 EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE, |
41 hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, |
45 hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, |
42 rtac distinct, rtac exhaust'] @ |
46 rtac distinct, rtac uexhaust] @ |
43 (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac]) |
47 (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac]) |
44 |> k = 1 ? swap |> op @)) 1; |
48 |> k = 1 ? swap |> op @)) 1; |
45 |
49 |
46 fun mk_half_disc_exclude_tac m discD disc' = |
50 fun mk_half_disc_exclude_tac m discD disc' = |
47 (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' rtac disc') 1; |
51 (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' rtac disc') 1; |
49 fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1; |
53 fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1; |
50 |
54 |
51 fun mk_disc_exhaust_tac n exhaust discIs = |
55 fun mk_disc_exhaust_tac n exhaust discIs = |
52 (rtac exhaust THEN' |
56 (rtac exhaust THEN' |
53 EVERY' (map2 (fn k => fn discI => |
57 EVERY' (map2 (fn k => fn discI => |
54 dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1; |
58 dtac discI THEN' select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) discIs)) 1; |
55 |
59 |
56 fun mk_collapse_tac ctxt m discD sels = |
60 fun mk_collapse_tac ctxt m discD sels = |
57 (dtac discD THEN' |
61 (dtac discD THEN' |
58 (if m = 0 then |
62 (if m = 0 then |
59 atac |
63 atac |
60 else |
64 else |
61 REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' |
65 REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' |
62 SELECT_GOAL (unfold_defs_tac ctxt sels) THEN' rtac refl)) 1; |
66 SELECT_GOAL (unfold_defs_tac ctxt sels) THEN' rtac refl)) 1; |
63 |
67 |
64 fun mk_case_eq_tac ctxt n exhaust' cases discss' selss = |
68 fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss |
65 (rtac exhaust' THEN' |
69 disc_excludesss' = |
|
70 if ms = [0] then |
|
71 rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses RS sym))) 1 |
|
72 else |
|
73 let |
|
74 val ks = 1 upto n; |
|
75 val maybe_atac = if n = 1 then K all_tac else atac; |
|
76 in |
|
77 (rtac udisc_exhaust THEN' |
|
78 EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse => |
|
79 EVERY' [if m = 0 then K all_tac else subst_tac ctxt [uuncollapse] THEN' maybe_atac, |
|
80 rtac sym, rtac vdisc_exhaust, |
|
81 EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse => |
|
82 EVERY' |
|
83 (if k' = k then |
|
84 if m = 0 then |
|
85 [hyp_subst_tac, rtac refl] |
|
86 else |
|
87 [subst_tac ctxt [vuncollapse], maybe_atac, |
|
88 if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac], |
|
89 REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE, asm_simp_tac (ss_only [])] |
|
90 else |
|
91 [dtac (the_single (if k = n then disc_excludes else disc_excludes')), |
|
92 etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}), |
|
93 atac, atac])) |
|
94 ks disc_excludess disc_excludess' uncollapses)]) |
|
95 ks ms disc_excludesss disc_excludesss' uncollapses)) 1 |
|
96 end; |
|
97 |
|
98 fun mk_case_eq_tac ctxt n uexhaust cases discss' selss = |
|
99 (rtac uexhaust THEN' |
66 EVERY' (map3 (fn casex => fn if_discs => fn sels => |
100 EVERY' (map3 (fn casex => fn if_discs => fn sels => |
67 EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_discs @ sels)), rtac casex]) |
101 EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_discs @ sels)), rtac casex]) |
68 cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1; |
102 cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1; |
69 |
103 |
70 fun mk_case_cong_tac exhaust' cases = |
104 fun mk_case_cong_tac uexhaust cases = |
71 (rtac exhaust' THEN' |
105 (rtac uexhaust THEN' |
72 EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex])]) cases)) 1; |
106 EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex])]) cases)) 1; |
73 |
107 |
74 val naked_ctxt = Proof_Context.init_global @{theory HOL}; |
108 val naked_ctxt = Proof_Context.init_global @{theory HOL}; |
75 |
109 |
76 fun mk_split_tac exhaust' cases injectss distinctsss = |
110 fun mk_split_tac uexhaust cases injectss distinctsss = |
77 rtac exhaust' 1 THEN |
111 rtac uexhaust 1 THEN |
78 ALLGOALS (fn k => (hyp_subst_tac THEN' |
112 ALLGOALS (fn k => (hyp_subst_tac THEN' |
79 simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @ |
113 simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @ |
80 flat (nth distinctsss (k - 1))))) k) THEN |
114 flat (nth distinctsss (k - 1))))) k) THEN |
81 ALLGOALS (blast_tac naked_ctxt); |
115 ALLGOALS (blast_tac naked_ctxt); |
82 |
116 |