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 list_implies_rev concl trms = Logic.list_implies (trms, concl) |
|
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) |
|
27 |
|
28 fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
21 fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
29 | strip_outer_params B = ([], B) |
22 | strip_outer_params B = ([], B) |
30 |
23 |
31 fun strip_params_prems_concl trm = |
24 fun strip_params_prems_concl trm = |
32 let |
25 let |
33 val (params, body) = strip_outer_params trm |
26 val (params, body) = strip_outer_params trm |
34 val (prems, concl) = strip_prems_concl body |
27 val (prems, concl) = Logic.strip_horn body |
35 in |
28 in |
36 (params, prems, concl) |
29 (params, prems, concl) |
37 end |
30 end |
38 |
31 |
39 fun list_params_prems_concl params prems concl = |
32 fun list_params_prems_concl params prems concl = |
40 Logic.list_implies (prems, concl) |
33 Logic.list_implies (prems, concl) |
41 |> fold_rev mk_all params |
34 |> fold_rev mk_all params |
42 |
|
43 |
35 |
44 fun mk_binop_env tys c (t, u) = |
36 fun mk_binop_env tys c (t, u) = |
45 let val ty = fastype_of1 (tys, t) in |
37 let val ty = fastype_of1 (tys, t) in |
46 Const (c, [ty, ty] ---> ty) $ t $ u |
38 Const (c, [ty, ty] ---> ty) $ t $ u |
47 end |
39 end |
56 |
48 |
57 *} |
49 *} |
58 |
50 |
59 |
51 |
60 ML {* |
52 ML {* |
61 fun process_ecase lthy c (params, prems, concl) bclauses = |
53 fun process_ecase lthy c (params, prems, concl) binders = |
62 let |
54 let |
63 fun binder tys (opt, i) = |
55 val tys = map snd params |
|
56 |
|
57 fun prep_binder (opt, i) = |
64 let |
58 let |
65 val t = Bound (length tys - i - 1) |
59 val t = Bound (length tys - i - 1) |
66 in |
60 in |
67 case opt of |
61 case opt of |
68 NONE => setify_ty lthy (nth tys i) t |
62 NONE => setify_ty lthy (nth tys i) t |
69 | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) |
63 | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) |
70 end |
64 end |
71 |
65 |
72 val param_tys = map snd params |
|
73 |
|
74 val fresh_prem = |
66 val fresh_prem = |
75 case (get_all_binders bclauses) of |
67 case binders of |
76 [] => [] (* case: no binders *) |
68 [] => [] (* case: no binders *) |
77 | binders => binders (* case: binders *) |
69 | binders => binders (* case: binders *) |
78 |> map (binder param_tys) |
70 |> map prep_binder |
79 |> fold_union_env param_tys |
71 |> fold_union_env tys |
80 |> (fn t => mk_fresh_star t c) |
72 |> (fn t => mk_fresh_star t c) |
81 |> HOLogic.mk_Trueprop |
73 |> HOLogic.mk_Trueprop |
82 |> single |
74 |> single |
83 in |
75 in |
84 list_params_prems_concl params (fresh_prem @ prems) concl |
76 list_params_prems_concl params (fresh_prem @ prems) concl |
85 end |
77 end |
86 *} |
78 *} |
87 |
79 |
88 |
80 ML {* |
89 ML {* |
81 fun fresh_thm ctxt c params binders bn_finite_thms = |
90 fun mk_strong_exhausts_goal lthy qexhausts bclausesss = |
82 let |
|
83 fun prep_binder (opt, i) = |
|
84 case opt of |
|
85 NONE => setify ctxt (nth params i) |
|
86 | SOME bn => to_set (bn $ (nth params i)) |
|
87 |
|
88 val rhs = HOLogic.mk_tuple (c :: params) |
|
89 val lhs = binders |
|
90 |> map prep_binder |
|
91 |> fold_union |
|
92 |> mk_perm (Bound 0) |
|
93 |
|
94 val goal = mk_fresh_star lhs rhs |
|
95 |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t)) |
|
96 |> HOLogic.mk_Trueprop |
|
97 val ss = @{thms finite.emptyI finite.insertI finite_supp supp_Pair finite_Un finite_fset finite_set} |
|
98 @ bn_finite_thms |
|
99 in |
|
100 Goal.prove ctxt [] [] goal |
|
101 (K (HEADGOAL (rtac @{thm at_set_avoiding1} |
|
102 THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) |
|
103 end |
|
104 *} |
|
105 |
|
106 |
|
107 ML {* |
|
108 fun case_tac ctxt c bn_finite_thms binderss thm = |
|
109 let |
|
110 fun aux_tac (binders : (term option * int) list)= |
|
111 Subgoal.FOCUS (fn {params, context, ...} => |
|
112 let |
|
113 val prms = map (term_of o snd) params |
|
114 val fthm = fresh_thm ctxt c prms binders bn_finite_thms |
|
115 val _ = tracing ("params" ^ @{make_string} params) |
|
116 val _ = tracing ("binders" ^ @{make_string} binders) |
|
117 in |
|
118 Skip_Proof.cheat_tac (ProofContext.theory_of ctxt) |
|
119 end) ctxt |
|
120 in |
|
121 rtac thm THEN' RANGE (map aux_tac binderss) |
|
122 end |
|
123 |
|
124 fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms = |
91 let |
125 let |
92 val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy |
126 val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy |
93 |
127 |
94 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
128 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
95 val c = Free (c, TFree (a, @{sort fs})) |
129 val c = Free (c, TFree (a, @{sort fs})) |
96 |
130 |
97 val (ecases, main_concls) = qexhausts' |
131 val binderss = map (map get_all_binders) bclausesss |
|
132 |
|
133 val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *) |
98 |> map prop_of |
134 |> map prop_of |
99 |> map strip_prems_concl |
135 |> map Logic.strip_horn |
100 |> split_list |
136 |> split_list |
101 |>> map (map strip_params_prems_concl) |
137 |>> map (map strip_params_prems_concl) |
|
138 |
|
139 val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat binderss) |
|
140 |
|
141 val _ = tracing ("binderss: " ^ @{make_string} binderss) |
102 in |
142 in |
103 map2 (map2 (process_ecase lthy'' c)) ecases bclausesss |
143 Goal.prove_multi lthy'' [] prems main_concls |
104 |> map2 list_implies_rev main_concls |
144 (fn {prems, context} => |
105 |> rpair lthy'' |
145 EVERY1 [Goal.conjunction_tac, |
106 end |
146 RANGE (map2 (case_tac context c bn_finite_thms) binderss qexhausts')]) |
107 |
147 end |
108 fun prove_strong_exhausts lthy qexhausts qtrms bclausesss = |
148 *} |
109 let |
149 |
110 val (goal, lthy') = mk_strong_exhausts_goal lthy qexhausts bclausesss |
150 |
111 |
|
112 val _ = goal |
|
113 |> map (Syntax.check_term lthy') |
|
114 |> map (Syntax.string_of_term lthy') |
|
115 |> cat_lines |
|
116 |> tracing |
|
117 in |
|
118 @{thms TrueI} |
|
119 end |
|
120 *} |
|
121 |
151 |
122 ML {* |
152 ML {* |
123 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
153 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
124 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
154 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
125 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
155 val simp_attr = Attrib.internal (K Simplifier.simp_add) |