13 ML {* open Nominal_Dt_Alpha *} |
13 ML {* open Nominal_Dt_Alpha *} |
14 |
14 |
15 use "nominal_dt_quot.ML" |
15 use "nominal_dt_quot.ML" |
16 ML {* open Nominal_Dt_Quot *} |
16 ML {* open Nominal_Dt_Quot *} |
17 |
17 |
|
18 ML {* |
|
19 fun strip_prems_concl trm = |
|
20 (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm) |
|
21 |
|
22 fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
|
23 | strip_outer_params B = ([], B) |
|
24 *} |
|
25 |
|
26 ML {* |
|
27 fun prove_strong_exhausts lthy qexhausts qtrms bclausess = |
|
28 let |
|
29 val (cses, main_concls) = qexhausts |
|
30 |> map prop_of |
|
31 |> map strip_prems_concl |
|
32 |> split_list |
|
33 |
|
34 fun process_case cse bclauses = |
|
35 let |
|
36 val (params, (body, concl)) = cse |
|
37 |> strip_outer_params |
|
38 ||> Logic.dest_implies |
|
39 in |
|
40 Logic.mk_implies (body, concl) |
|
41 end |
|
42 |
|
43 val cses' = map2 (map2 process_case) cses bclausess |
|
44 |> map (map (Syntax.string_of_term lthy)) |
|
45 |> map commas |
|
46 |> cat_lines |
|
47 |
|
48 val _ = tracing ("cases\n " ^ cses') |
|
49 in |
|
50 () |
|
51 end |
|
52 *} |
|
53 |
|
54 ML {* |
|
55 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
|
56 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
|
57 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
|
58 *} |
18 |
59 |
19 section{* Interface for nominal_datatype *} |
60 section{* Interface for nominal_datatype *} |
20 |
61 |
21 ML {* print_depth 50 *} |
62 ML {* print_depth 50 *} |
22 |
63 |
163 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
204 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
164 if get_STEPS lthy > 0 |
205 if get_STEPS lthy > 0 |
165 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
206 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
166 else raise TEST lthy |
207 else raise TEST lthy |
167 |
208 |
|
209 val _ = tracing ("bclauses\n" ^ cat_lines (map @{make_string} bclauses)) |
168 val _ = tracing ("raw_bclauses\n" ^ cat_lines (map @{make_string} raw_bclauses)) |
210 val _ = tracing ("raw_bclauses\n" ^ cat_lines (map @{make_string} raw_bclauses)) |
169 |
211 |
170 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
212 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
171 val {descr, sorts, ...} = dtinfo |
213 val {descr, sorts, ...} = dtinfo |
172 |
214 |
521 (* proving the relationship of bn and permute_bn *) |
563 (* proving the relationship of bn and permute_bn *) |
522 val qpermute_bn_thms = |
564 val qpermute_bn_thms = |
523 if get_STEPS lthy > 33 |
565 if get_STEPS lthy > 33 |
524 then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC |
566 then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC |
525 else [] |
567 else [] |
|
568 |
|
569 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses |
526 |
570 |
527 (* noting the theorems *) |
571 (* noting the theorems *) |
528 |
572 |
529 (* generating the prefix for the theorem names *) |
573 (* generating the prefix for the theorem names *) |
530 val thms_name = |
574 val thms_name = |