21 open BNF_FP_Util |
21 open BNF_FP_Util |
22 open BNF_FP_Def_Sugar |
22 open BNF_FP_Def_Sugar |
23 |
23 |
24 fun nchotomy_tac nchotomy = |
24 fun nchotomy_tac nchotomy = |
25 HEADGOAL (rtac (nchotomy RS @{thm all_reg[rotated]}) THEN' |
25 HEADGOAL (rtac (nchotomy RS @{thm all_reg[rotated]}) THEN' |
26 CHANGED_PROP o REPEAT_ALL_NEW (match_tac [allI, impI]) THEN' |
26 REPEAT_ALL_NEW (match_tac [allI, impI]) THEN' REPEAT_ALL_NEW (ematch_tac [exE, disjE])); |
27 CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac [exE, disjE])); |
|
28 |
27 |
29 fun meta_spec_mp_tac 0 = K all_tac |
28 fun meta_spec_mp_tac 0 = K all_tac |
30 | meta_spec_mp_tac depth = |
29 | meta_spec_mp_tac depth = |
31 dtac meta_spec THEN' meta_spec_mp_tac (depth - 1) THEN' dtac meta_mp THEN' atac; |
30 dtac meta_spec THEN' meta_spec_mp_tac (depth - 1) THEN' dtac meta_mp THEN' atac; |
32 |
31 |
34 DEEPEN (1, 64 (* large number *)) |
33 DEEPEN (1, 64 (* large number *)) |
35 (fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0; |
34 (fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0; |
36 |
35 |
37 val same_ctr_simps = |
36 val same_ctr_simps = |
38 @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split snd_conv simp_thms}; |
37 @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split snd_conv simp_thms}; |
|
38 val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms}; |
39 |
39 |
40 fun same_ctr_tac ctxt injects recs map_comps' inj_map_strongs' = |
40 fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' = |
41 HEADGOAL (asm_full_simp_tac (ss_only (injects @ recs @ map_comps' @ same_ctr_simps) ctxt) THEN' |
41 HEADGOAL (asm_full_simp_tac |
42 REPEAT_DETERM o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac (conjE :: inj_map_strongs')) |
42 (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE' |
43 THEN_ALL_NEW use_induction_hypothesis_tac); |
43 TRY o REPEAT_ALL_NEW (rtac conjI) THEN_ALL_NEW |
|
44 REPEAT_ALL_NEW (eresolve_tac (conjE :: inj_map_strongs')) THEN_ALL_NEW |
|
45 use_induction_hypothesis_tac); |
44 |
46 |
45 fun distinct_ctrs_tac ctxt recs = |
47 fun distinct_ctrs_tac ctxt recs = |
46 HEADGOAL (asm_full_simp_tac (ss_only (recs @ |
48 HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt)); |
47 @{thms sum_encode_eq sum.inject sum.distinct simp_thms}) ctxt)); |
|
48 |
49 |
49 fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' = |
50 fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' = |
50 let val ks = 1 upto n in |
51 let val ks = 1 upto n in |
51 EVERY (maps (fn k => nchotomy_tac nchotomy :: map (fn k' => |
52 EVERY (maps (fn k => nchotomy_tac nchotomy :: map (fn k' => |
52 if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs' |
53 if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs' |
118 fun derive_encode_injectives_thms _ [] = [] |
119 fun derive_encode_injectives_thms _ [] = [] |
119 | derive_encode_injectives_thms ctxt fpT_names0 = |
120 | derive_encode_injectives_thms ctxt fpT_names0 = |
120 let |
121 let |
121 fun not_datatype s = error (quote s ^ " is not a new-style datatype"); |
122 fun not_datatype s = error (quote s ^ " is not a new-style datatype"); |
122 fun not_mutually_recursive ss = |
123 fun not_mutually_recursive ss = |
123 error ("{" ^ commas ss ^ "} are not mutually recursive new-style datatypes"); |
124 error (commas ss ^ " are not mutually recursive new-style datatypes"); |
124 |
125 |
125 fun lfp_sugar_of s = |
126 fun lfp_sugar_of s = |
126 (case fp_sugar_of ctxt s of |
127 (case fp_sugar_of ctxt s of |
127 SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar |
128 SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar |
128 | _ => not_datatype s); |
129 | _ => not_datatype s); |