author | blanchet |
Thu, 16 Dec 2010 22:45:02 +0100 | |
changeset 41220 | 4d11b0de7dd8 |
parent 35985 | 0bbf0d2348f9 |
child 43329 | 84472e198515 |
permissions | -rw-r--r-- |
19416 | 1 |
(* Title: Pure/conjunction.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Meta-level conjunction. |
|
5 |
*) |
|
6 |
||
7 |
signature CONJUNCTION = |
|
8 |
sig |
|
9 |
val conjunction: cterm |
|
10 |
val mk_conjunction: cterm * cterm -> cterm |
|
23422 | 11 |
val mk_conjunction_balanced: cterm list -> cterm |
19416 | 12 |
val dest_conjunction: cterm -> cterm * cterm |
30823
eb99b9134f2e
added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents:
29606
diff
changeset
|
13 |
val dest_conjunctions: cterm -> cterm list |
19416 | 14 |
val cong: thm -> thm -> thm |
23422 | 15 |
val convs: (cterm -> thm) -> cterm -> thm |
19416 | 16 |
val conjunctionD1: thm |
17 |
val conjunctionD2: thm |
|
18 |
val conjunctionI: thm |
|
19 |
val intr: thm -> thm -> thm |
|
23422 | 20 |
val intr_balanced: thm list -> thm |
19416 | 21 |
val elim: thm -> thm * thm |
23422 | 22 |
val elim_balanced: int -> thm -> thm list |
23 |
val curry_balanced: int -> thm -> thm |
|
24 |
val uncurry_balanced: int -> thm -> thm |
|
19416 | 25 |
end; |
26 |
||
27 |
structure Conjunction: CONJUNCTION = |
|
28 |
struct |
|
29 |
||
30 |
(** abstract syntax **) |
|
31 |
||
26485 | 32 |
fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t; |
33384 | 33 |
val read_prop = certify o Simple_Syntax.read_prop; |
19416 | 34 |
|
26485 | 35 |
val true_prop = certify Logic.true_prop; |
36 |
val conjunction = certify Logic.conjunction; |
|
23422 | 37 |
|
19416 | 38 |
fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B; |
39 |
||
23422 | 40 |
fun mk_conjunction_balanced [] = true_prop |
32765 | 41 |
| mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts; |
23422 | 42 |
|
19416 | 43 |
fun dest_conjunction ct = |
44 |
(case Thm.term_of ct of |
|
26424 | 45 |
(Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct |
23422 | 46 |
| _ => raise TERM ("dest_conjunction", [Thm.term_of ct])); |
19416 | 47 |
|
30823
eb99b9134f2e
added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents:
29606
diff
changeset
|
48 |
fun dest_conjunctions ct = |
eb99b9134f2e
added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents:
29606
diff
changeset
|
49 |
(case try dest_conjunction ct of |
eb99b9134f2e
added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents:
29606
diff
changeset
|
50 |
NONE => [ct] |
eb99b9134f2e
added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents:
29606
diff
changeset
|
51 |
| SOME (A, B) => dest_conjunctions A @ dest_conjunctions B); |
eb99b9134f2e
added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents:
29606
diff
changeset
|
52 |
|
19416 | 53 |
|
54 |
||
55 |
(** derived rules **) |
|
56 |
||
57 |
(* conversion *) |
|
58 |
||
59 |
val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction); |
|
60 |
||
23422 | 61 |
fun convs cv ct = |
62 |
(case try dest_conjunction ct of |
|
63 |
NONE => cv ct |
|
64 |
| SOME (A, B) => cong (convs cv A) (convs cv B)); |
|
19416 | 65 |
|
66 |
||
67 |
(* intro/elim *) |
|
68 |
||
69 |
local |
|
70 |
||
24241 | 71 |
val A = read_prop "A" and vA = read_prop "?A"; |
72 |
val B = read_prop "B" and vB = read_prop "?B"; |
|
73 |
val C = read_prop "C"; |
|
74 |
val ABC = read_prop "A ==> B ==> C"; |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28674
diff
changeset
|
75 |
val A_B = read_prop "A &&& B"; |
19416 | 76 |
|
26424 | 77 |
val conjunction_def = |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
33384
diff
changeset
|
78 |
Thm.unvarify_global |
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
33384
diff
changeset
|
79 |
(Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def"); |
19416 | 80 |
|
81 |
fun conjunctionD which = |
|
82 |
Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP |
|
26653 | 83 |
Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B)); |
19416 | 84 |
|
85 |
in |
|
86 |
||
33277 | 87 |
val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1); |
88 |
val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2); |
|
19416 | 89 |
|
33277 | 90 |
val conjunctionI = |
91 |
Drule.store_standard_thm (Binding.name "conjunctionI") |
|
92 |
(Drule.implies_intr_list [A, B] |
|
93 |
(Thm.equal_elim |
|
94 |
(Thm.symmetric conjunction_def) |
|
95 |
(Thm.forall_intr C (Thm.implies_intr ABC |
|
96 |
(Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B]))))); |
|
19416 | 97 |
|
23422 | 98 |
|
20508
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
99 |
fun intr tha thb = |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
100 |
Thm.implies_elim |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
101 |
(Thm.implies_elim |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
102 |
(Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI) |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
103 |
tha) |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
104 |
thb; |
19416 | 105 |
|
106 |
fun elim th = |
|
20508
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
107 |
let |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
108 |
val (A, B) = dest_conjunction (Thm.cprop_of th) |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
109 |
handle TERM (msg, _) => raise THM (msg, 0, [th]); |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
110 |
val inst = Thm.instantiate ([], [(vA, A), (vB, B)]); |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
111 |
in |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
112 |
(Thm.implies_elim (inst conjunctionD1) th, |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
113 |
Thm.implies_elim (inst conjunctionD2) th) |
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset
|
114 |
end; |
19416 | 115 |
|
23422 | 116 |
end; |
117 |
||
118 |
||
23535
58147e5bd070
removed obsolete mk_conjunction_list, intr/elim_list;
wenzelm
parents:
23422
diff
changeset
|
119 |
(* balanced conjuncts *) |
23422 | 120 |
|
121 |
fun intr_balanced [] = asm_rl |
|
32765 | 122 |
| intr_balanced ths = Balanced_Tree.make (uncurry intr) ths; |
23422 | 123 |
|
124 |
fun elim_balanced 0 _ = [] |
|
32765 | 125 |
| elim_balanced n th = Balanced_Tree.dest elim n th; |
19416 | 126 |
|
127 |
||
128 |
(* currying *) |
|
129 |
||
130 |
local |
|
131 |
||
26424 | 132 |
fun conjs thy n = |
133 |
let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n) |
|
23422 | 134 |
in (As, mk_conjunction_balanced As) end; |
19416 | 135 |
|
24241 | 136 |
val B = read_prop "B"; |
19416 | 137 |
|
138 |
fun comp_rule th rule = |
|
20260 | 139 |
Thm.adjust_maxidx_thm ~1 (th COMP |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35845
diff
changeset
|
140 |
(rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1))); |
19416 | 141 |
|
142 |
in |
|
143 |
||
144 |
(* |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28674
diff
changeset
|
145 |
A1 &&& ... &&& An ==> B |
19416 | 146 |
----------------------- |
147 |
A1 ==> ... ==> An ==> B |
|
148 |
*) |
|
23422 | 149 |
fun curry_balanced n th = |
150 |
if n < 2 then th |
|
151 |
else |
|
152 |
let |
|
26424 | 153 |
val thy = Thm.theory_of_thm th; |
154 |
val (As, C) = conjs thy n; |
|
23422 | 155 |
val D = Drule.mk_implies (C, B); |
156 |
in |
|
157 |
comp_rule th |
|
158 |
(Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As)) |
|
159 |
|> Drule.implies_intr_list (D :: As)) |
|
160 |
end; |
|
19416 | 161 |
|
162 |
(* |
|
163 |
A1 ==> ... ==> An ==> B |
|
164 |
----------------------- |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28674
diff
changeset
|
165 |
A1 &&& ... &&& An ==> B |
19416 | 166 |
*) |
23422 | 167 |
fun uncurry_balanced n th = |
168 |
if n < 2 then th |
|
169 |
else |
|
170 |
let |
|
26424 | 171 |
val thy = Thm.theory_of_thm th; |
172 |
val (As, C) = conjs thy n; |
|
23422 | 173 |
val D = Drule.list_implies (As, B); |
174 |
in |
|
175 |
comp_rule th |
|
176 |
(Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C)) |
|
177 |
|> Drule.implies_intr_list [D, C]) |
|
178 |
end; |
|
19416 | 179 |
|
180 |
end; |
|
181 |
||
182 |
end; |