author  wenzelm 
Thu, 09 Jun 2011 20:22:22 +0200  
changeset 43329  84472e198515 
parent 35985  0bbf0d2348f9 
child 46497  89ccf66aa73d 
permissions  rwrr 
19416  1 
(* Title: Pure/conjunction.ML 
2 
Author: Makarius 

3 

4 
Metalevel 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 = 
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
35985
diff
changeset

133 
let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invent 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; 