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