author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24241  424cb8b5e5b4 
child 24976  821628d16552 
permissions  rwrr 
19416  1 
(* Title: Pure/conjunction.ML 
2 
ID: $Id$ 

3 
Author: Makarius 

4 

5 
Metalevel conjunction. 

6 
*) 

7 

8 
signature CONJUNCTION = 

9 
sig 

10 
val conjunction: cterm 

11 
val mk_conjunction: cterm * cterm > cterm 

23422  12 
val mk_conjunction_balanced: cterm list > cterm 
19416  13 
val dest_conjunction: cterm > cterm * cterm 
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 

32 
val cert = Thm.cterm_of ProtoPure.thy; 

24241  33 
val read_prop = cert o SimpleSyntax.read_prop; 
19416  34 

23422  35 
val true_prop = cert Logic.true_prop; 
19416  36 
val conjunction = cert 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 
41 
 mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts; 

42 

19416  43 
fun dest_conjunction ct = 
44 
(case Thm.term_of ct of 

20666  45 
(Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct 
23422  46 
 _ => raise TERM ("dest_conjunction", [Thm.term_of ct])); 
19416  47 

48 

49 

50 
(** derived rules **) 

51 

52 
(* conversion *) 

53 

54 
val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction); 

55 

23422  56 
fun convs cv ct = 
57 
(case try dest_conjunction ct of 

58 
NONE => cv ct 

59 
 SOME (A, B) => cong (convs cv A) (convs cv B)); 

19416  60 

61 

62 
(* intro/elim *) 

63 

64 
local 

65 

24241  66 
val A = read_prop "A" and vA = read_prop "?A"; 
67 
val B = read_prop "B" and vB = read_prop "?B"; 

68 
val C = read_prop "C"; 

69 
val ABC = read_prop "A ==> B ==> C"; 

70 
val A_B = read_prop "A && B"; 

19416  71 

20238  72 
val conjunction_def = Drule.unvarify ProtoPure.conjunction_def; 
19416  73 

74 
fun conjunctionD which = 

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

76 
Drule.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B)); 

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 

23422  124 
fun conjs n = 
125 
let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n) 

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 
19416  132 
(rule > Drule.forall_intr_frees > Drule.forall_elim_vars (Thm.maxidx_of th + 1))); 
133 

134 
in 

135 

136 
(* 

137 
A1 && ... && An ==> B 

138 
 

139 
A1 ==> ... ==> An ==> B 

140 
*) 

23422  141 
fun curry_balanced n th = 
142 
if n < 2 then th 

143 
else 

144 
let 

145 
val (As, C) = conjs n; 

146 
val D = Drule.mk_implies (C, B); 

147 
in 

148 
comp_rule th 

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

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

151 
end; 

19416  152 

153 
(* 

154 
A1 ==> ... ==> An ==> B 

155 
 

23422  156 
A1 && ... && An ==> B 
19416  157 
*) 
23422  158 
fun uncurry_balanced n th = 
159 
if n < 2 then th 

160 
else 

161 
let 

162 
val (As, C) = conjs n; 

163 
val D = Drule.list_implies (As, B); 

164 
in 

165 
comp_rule th 

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

167 
> Drule.implies_intr_list [D, C]) 

168 
end; 

19416  169 

170 
end; 

171 

172 
end; 