author  wenzelm 
Tue, 29 Sep 2009 22:48:24 +0200  
changeset 32765  3032c0308019 
parent 30823  eb99b9134f2e 
child 33277  1bdc3c732fdd 
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; 
33 
val read_prop = certify o SimpleSyntax.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 = 
28674  78 
Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def"); 
19416  79 

80 
fun conjunctionD which = 

81 
Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP 

26653  82 
Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B)); 
19416  83 

84 
in 

85 

86 
val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1); 

87 
val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2); 

88 

89 
val conjunctionI = Drule.store_standard_thm "conjunctionI" 

90 
(Drule.implies_intr_list [A, B] 

91 
(Thm.equal_elim 

92 
(Thm.symmetric conjunction_def) 

93 
(Thm.forall_intr C (Thm.implies_intr ABC 

94 
(Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B]))))); 

95 

23422  96 

20508
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset

97 
fun intr tha thb = 
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset

98 
Thm.implies_elim 
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset

99 
(Thm.implies_elim 
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset

100 
(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

101 
tha) 
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset

102 
thb; 
19416  103 

104 
fun elim th = 

20508
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset

105 
let 
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset

106 
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

107 
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

108 
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

109 
in 
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset

110 
(Thm.implies_elim (inst conjunctionD1) th, 
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset

111 
Thm.implies_elim (inst conjunctionD2) th) 
8182d961c7cc
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents:
20260
diff
changeset

112 
end; 
19416  113 

23422  114 
end; 
115 

116 

23535
58147e5bd070
removed obsolete mk_conjunction_list, intr/elim_list;
wenzelm
parents:
23422
diff
changeset

117 
(* balanced conjuncts *) 
23422  118 

119 
fun intr_balanced [] = asm_rl 

32765  120 
 intr_balanced ths = Balanced_Tree.make (uncurry intr) ths; 
23422  121 

122 
fun elim_balanced 0 _ = [] 

32765  123 
 elim_balanced n th = Balanced_Tree.dest elim n th; 
19416  124 

125 

126 
(* currying *) 

127 

128 
local 

129 

26424  130 
fun conjs thy n = 
131 
let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n) 

23422  132 
in (As, mk_conjunction_balanced As) end; 
19416  133 

24241  134 
val B = read_prop "B"; 
19416  135 

136 
fun comp_rule th rule = 

20260  137 
Thm.adjust_maxidx_thm ~1 (th COMP 
26653  138 
(rule > Drule.forall_intr_frees > Thm.forall_elim_vars (Thm.maxidx_of th + 1))); 
19416  139 

140 
in 

141 

142 
(* 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28674
diff
changeset

143 
A1 &&& ... &&& An ==> B 
19416  144 
 
145 
A1 ==> ... ==> An ==> B 

146 
*) 

23422  147 
fun curry_balanced n th = 
148 
if n < 2 then th 

149 
else 

150 
let 

26424  151 
val thy = Thm.theory_of_thm th; 
152 
val (As, C) = conjs thy n; 

23422  153 
val D = Drule.mk_implies (C, B); 
154 
in 

155 
comp_rule th 

156 
(Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As)) 

157 
> Drule.implies_intr_list (D :: As)) 

158 
end; 

19416  159 

160 
(* 

161 
A1 ==> ... ==> An ==> B 

162 
 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28674
diff
changeset

163 
A1 &&& ... &&& An ==> B 
19416  164 
*) 
23422  165 
fun uncurry_balanced n th = 
166 
if n < 2 then th 

167 
else 

168 
let 

26424  169 
val thy = Thm.theory_of_thm th; 
170 
val (As, C) = conjs thy n; 

23422  171 
val D = Drule.list_implies (As, B); 
172 
in 

173 
comp_rule th 

174 
(Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C)) 

175 
> Drule.implies_intr_list [D, C]) 

176 
end; 

19416  177 

178 
end; 

179 

180 
end; 