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 text {* TEST *} |
|
19 |
18 ML {* |
20 ML {* |
19 fun strip_prems_concl trm = |
21 fun strip_prems_concl trm = |
20 (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm) |
22 (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm) |
21 |
23 |
22 fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
24 fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
23 | strip_outer_params B = ([], B) |
25 | strip_outer_params B = ([], B) |
24 *} |
26 *} |
25 |
27 |
|
28 |
|
29 ML {* |
|
30 fun binders bclauses = |
|
31 let |
|
32 fun aux1 (NONE, i) = Bound i |
|
33 | aux1 (SOME bn, i) = bn $ Bound i |
|
34 in |
|
35 bclauses |
|
36 |> map (fn (BC (_, x, _)) => x) |
|
37 |> flat |
|
38 |> map aux1 |
|
39 end |
|
40 *} |
|
41 |
26 ML {* |
42 ML {* |
27 fun prove_strong_exhausts lthy qexhausts qtrms bclausess = |
43 fun prove_strong_exhausts lthy qexhausts qtrms bclausess = |
28 let |
44 let |
29 val (cses, main_concls) = qexhausts |
45 val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy |
|
46 |
|
47 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
|
48 val c = Free (c, TFree (a, @{sort fs})) |
|
49 |
|
50 val (cses, main_concls) = qexhausts' |
30 |> map prop_of |
51 |> map prop_of |
31 |> map strip_prems_concl |
52 |> map strip_prems_concl |
32 |> split_list |
53 |> split_list |
33 |
54 |
34 fun process_case cse bclauses = |
55 fun process_case cse bclauses = |
35 let |
56 let |
36 val (params, (body, concl)) = cse |
57 val (params, (body, concl)) = cse |
37 |> strip_outer_params |
58 |> strip_outer_params |
38 ||> Logic.dest_implies |
59 ||> Logic.dest_implies |
|
60 |
|
61 (*val bnds = HOLogic.mk_tuple (binders bclauses)*) |
|
62 val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (c, c)) |
39 in |
63 in |
40 Logic.mk_implies (body, concl) |
64 Logic.mk_implies (prem, Logic.mk_implies (body, concl)) |
41 end |
65 end |
42 |
66 |
43 val cses' = map2 (map2 process_case) cses bclausess |
67 val cses' = map2 (map2 process_case) cses bclausess |
44 |> map (map (Syntax.string_of_term lthy)) |
68 |> map (map (Syntax.string_of_term lthy'')) |
45 |> map commas |
69 |> map commas |
46 |> cat_lines |
70 |> cat_lines |
47 |
71 |
48 val _ = tracing ("cases\n " ^ cses') |
72 val _ = tracing ("cases\n " ^ cses') |
49 in |
73 in |