|
1 |
|
2 fun dest_relcomp (t as (Const (@{const_name "Collect"}, _) $ Abs (_, pT, ex_exp))) = |
|
3 let |
|
4 val (T1, T2) = HOLogic.dest_prodT pT |
|
5 val qs = Term.strip_qnt_vars "Ex" ex_exp |
|
6 val bod = Term.strip_qnt_body "Ex" ex_exp |
|
7 |
|
8 val (l, r, cond) = case bod of |
|
9 Const ("op &", _) |
|
10 $ (Const ("op =", _) $ Bound idx |
|
11 $ (Const ("Pair", _) $ l $ r)) |
|
12 $ cond |
|
13 => if idx = length qs then (l, r, cond) |
|
14 else raise TERM ("dest_relcomp", [t]) |
|
15 | _ => raise TERM ("dest_relcomp", [t]) |
|
16 in |
|
17 (T1, T2, qs, l, r, cond) |
|
18 end |
|
19 | dest_relcomp t = raise TERM ("dest_relcomp", [t]) |
|
20 |
|
21 fun mk_pair_compr (T1, T2, qs, l, r, cond) = |
|
22 let |
|
23 val pT = HOLogic.mk_prodT (T1, T2) |
|
24 val peq = HOLogic.eq_const pT $ Bound (length qs) $ (HOLogic.pair_const T1 T2 $ l $ r) |
|
25 val bod = HOLogic.mk_conj (peq, cond) |
|
26 in |
|
27 HOLogic.Collect_const pT $ |
|
28 Abs ("uu_", pT, fold_rev (fn (a,T) => fn b => HOLogic.exists_const T $ Abs(a, T, b)) qs bod) |
|
29 end |
|
30 |
|
31 fun join_compr c1 c2 : term = |
|
32 let |
|
33 val (T1, T2, qs1, l1, r1, cond1) = dest_relcomp c1 |
|
34 val (T2, T3, qs2, l2, r2, cond2) = dest_relcomp c2 |
|
35 |
|
36 val lift = incr_boundvars (length qs2) |
|
37 val cond = HOLogic.mk_conj (HOLogic.eq_const T2 $ lift r1 $ l2, |
|
38 HOLogic.mk_conj (lift cond1, cond2)) |
|
39 in |
|
40 mk_pair_compr |
|
41 (T1, T3, qs1 @ qs2, lift l1, r2, cond) |
|
42 end |
|
43 |
|
44 val compr_compose_tac'= |
|
45 EVERY1 (map (curry op o DETERM) |
|
46 [rtac @{thm set_ext}, |
|
47 rtac @{thm iffI}, |
|
48 etac @{thm rel_compE}, |
|
49 etac @{thm CollectE}, |
|
50 etac @{thm CollectE}, |
|
51 single_hyp_subst_tac 0, |
|
52 (fn i => REPEAT_DETERM (etac @{thm exE} i)), |
|
53 K (print_tac "A"), |
|
54 etac @{thm conjE}, |
|
55 K (print_tac "B"), |
|
56 etac @{thm conjE}, |
|
57 K (print_tac "B'"), |
|
58 etac @{thm Pair_inject}, |
|
59 K (print_tac "C"), |
|
60 rotate_tac 1, |
|
61 K (print_tac "D"), |
|
62 etac @{thm Pair_inject}, |
|
63 K (print_tac "E"), |
|
64 single_hyp_subst_tac 2, |
|
65 single_hyp_subst_tac 3, |
|
66 single_hyp_subst_tac 3, |
|
67 rtac @{thm CollectI}, |
|
68 (fn i => REPEAT_DETERM (rtac @{thm exI} i)), |
|
69 rtac @{thm conjI}, |
|
70 rtac @{thm refl}, |
|
71 rtac @{thm conjI}, |
|
72 assume_tac, |
|
73 rtac @{thm conjI}, |
|
74 assume_tac, |
|
75 assume_tac, |
|
76 etac @{thm CollectE}, |
|
77 (fn i => REPEAT (etac @{thm exE} i)), |
|
78 etac @{thm conjE}, |
|
79 single_hyp_subst_tac 0, |
|
80 etac @{thm conjE}, |
|
81 etac @{thm conjE}, |
|
82 rtac @{thm rel_compI}, |
|
83 rtac @{thm CollectI}, |
|
84 (fn i => REPEAT (rtac @{thm exI} i)), |
|
85 rtac @{thm conjI}, |
|
86 rtac @{thm refl}, |
|
87 assume_tac, |
|
88 rtac @{thm CollectI}, |
|
89 (fn i => REPEAT (rtac @{thm exI} i)), |
|
90 rtac @{thm conjI}, |
|
91 stac @{thm Pair_eq}, |
|
92 rtac @{thm conjI}, |
|
93 assume_tac, |
|
94 rtac @{thm refl}, |
|
95 assume_tac]) |
|
96 |
|
97 |
|
98 fun compose_simproc _ ss ct : thm option = |
|
99 let |
|
100 val thy = theory_of_cterm ct |
|
101 val sCt as (_ $ s $ t) = term_of ct |
|
102 val T = fastype_of sCt |
|
103 val g : term = Logic.mk_equals (sCt, join_compr t s) |
|
104 (* val _ = Output.tracing (Syntax.string_of_term (Simplifier.the_context ss) g)*) |
|
105 in |
|
106 SOME (Goal.prove_internal [] (cterm_of thy g) |
|
107 (K (rtac @{thm eq_reflection} 1 |
|
108 THEN compr_compose_tac'))) |
|
109 end |
|
110 handle TERM _ => NONE |
|
111 |