16 ML {* open Nominal_Dt_Quot *} |
16 ML {* open Nominal_Dt_Quot *} |
17 |
17 |
18 text {* TEST *} |
18 text {* TEST *} |
19 |
19 |
20 ML {* |
20 ML {* |
21 fun strip_prems_concl trm = |
21 fun list_implies_rev concl trms = Logic.list_implies (trms, concl) |
22 (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm) |
22 |
|
23 fun mk_all (a, T) t = Const ("all", (T --> propT) --> propT) $ Abs (a, T, t) |
|
24 |
|
25 fun strip_prems_concl (Const("==>", _) $ A $ B) = strip_prems_concl B |>> cons A |
|
26 | strip_prems_concl B = ([], B) |
23 |
27 |
24 fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
28 fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
25 | strip_outer_params B = ([], B) |
29 | strip_outer_params B = ([], B) |
26 *} |
30 |
27 |
31 fun strip_params_prems_concl trm = |
28 |
|
29 ML {* |
|
30 fun binders bclauses = |
|
31 let |
32 let |
32 fun aux1 (NONE, i) = Bound i |
33 val (params, body) = strip_outer_params trm |
33 | aux1 (SOME bn, i) = bn $ Bound i |
34 val (prems, concl) = strip_prems_concl body |
34 in |
35 in |
35 bclauses |
36 (params, prems, concl) |
36 |> map (fn (BC (_, x, _)) => x) |
37 end |
37 |> flat |
38 |
38 |> map aux1 |
39 fun list_params_prems_concl params prems concl = |
39 end |
40 Logic.list_implies (prems, concl) |
40 *} |
41 |> fold_rev mk_all params |
41 |
42 |
42 ML {* |
43 |
43 fun prove_strong_exhausts lthy qexhausts qtrms bclausess = |
44 fun mk_binop_env tys c (t, u) = |
|
45 let val ty = fastype_of1 (tys, t) in |
|
46 Const (c, [ty, ty] ---> ty) $ t $ u |
|
47 end |
|
48 |
|
49 fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1 |
|
50 | mk_union_env tys (@{term "{}::atom set"}, t2) = t2 |
|
51 | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1 |
|
52 | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2 |
|
53 | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2) |
|
54 |
|
55 fun fold_union_env tys trms = fold_rev (curry (mk_union_env tys)) trms @{term "{}::atom set"} |
|
56 |
|
57 *} |
|
58 |
|
59 |
|
60 ML {* |
|
61 fun process_ecase lthy c (params, prems, concl) bclauses = |
|
62 let |
|
63 fun binder tys (opt, i) = |
|
64 let |
|
65 val t = Bound (length tys - i - 1) |
|
66 in |
|
67 case opt of |
|
68 NONE => setify_ty lthy (nth tys i) t |
|
69 | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) |
|
70 end |
|
71 |
|
72 val param_tys = map snd params |
|
73 |
|
74 val fresh_prem = |
|
75 case (get_all_binders bclauses) of |
|
76 [] => [] (* case: no binders *) |
|
77 | binders => binders (* case: binders *) |
|
78 |> map (binder param_tys) |
|
79 |> fold_union_env param_tys |
|
80 |> (fn t => mk_fresh_star t c) |
|
81 |> HOLogic.mk_Trueprop |
|
82 |> single |
|
83 in |
|
84 list_params_prems_concl params (fresh_prem @ prems) concl |
|
85 end |
|
86 *} |
|
87 |
|
88 |
|
89 ML {* |
|
90 fun mk_strong_exhausts_goal lthy qexhausts bclausesss = |
44 let |
91 let |
45 val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy |
92 val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy |
46 |
93 |
47 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
94 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
48 val c = Free (c, TFree (a, @{sort fs})) |
95 val c = Free (c, TFree (a, @{sort fs})) |
49 |
96 |
50 val (cses, main_concls) = qexhausts' |
97 val (ecases, main_concls) = qexhausts' |
51 |> map prop_of |
98 |> map prop_of |
52 |> map strip_prems_concl |
99 |> map strip_prems_concl |
53 |> split_list |
100 |> split_list |
54 |
101 |>> map (map strip_params_prems_concl) |
55 fun process_case cse bclauses = |
102 in |
56 let |
103 map2 (map2 (process_ecase lthy'' c)) ecases bclausesss |
57 val (params, (body, concl)) = cse |
104 |> map2 list_implies_rev main_concls |
58 |> strip_outer_params |
105 |> rpair lthy'' |
59 ||> Logic.dest_implies |
106 end |
60 |
107 |
61 (*val bnds = HOLogic.mk_tuple (binders bclauses)*) |
108 fun prove_strong_exhausts lthy qexhausts qtrms bclausesss = |
62 val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (c, c)) |
109 let |
63 in |
110 val (goal, lthy') = mk_strong_exhausts_goal lthy qexhausts bclausesss |
64 Logic.mk_implies (prem, Logic.mk_implies (body, concl)) |
111 |
65 end |
112 val _ = goal |
66 |
113 |> map (Syntax.check_term lthy') |
67 val cses' = map2 (map2 process_case) cses bclausess |
114 |> map (Syntax.string_of_term lthy') |
68 |> map (map (Syntax.string_of_term lthy'')) |
|
69 |> map commas |
|
70 |> cat_lines |
115 |> cat_lines |
71 |
116 |> tracing |
72 val _ = tracing ("cases\n " ^ cses') |
|
73 in |
117 in |
74 () |
118 @{thms TrueI} |
75 end |
119 end |
76 *} |
120 *} |
77 |
121 |
78 ML {* |
122 ML {* |
79 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
123 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
227 val _ = warning "Definition of raw datatypes"; |
271 val _ = warning "Definition of raw datatypes"; |
228 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
272 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
229 if get_STEPS lthy > 0 |
273 if get_STEPS lthy > 0 |
230 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
274 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
231 else raise TEST lthy |
275 else raise TEST lthy |
232 |
|
233 val _ = tracing ("bclauses\n" ^ cat_lines (map @{make_string} bclauses)) |
|
234 val _ = tracing ("raw_bclauses\n" ^ cat_lines (map @{make_string} raw_bclauses)) |
|
235 |
276 |
236 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
277 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
237 val {descr, sorts, ...} = dtinfo |
278 val {descr, sorts, ...} = dtinfo |
238 |
279 |
239 val raw_tys = all_dtyps descr sorts |
280 val raw_tys = all_dtyps descr sorts |