7 |
7 |
8 signature CONJUNCTION = |
8 signature CONJUNCTION = |
9 sig |
9 sig |
10 val conjunction: cterm |
10 val conjunction: cterm |
11 val mk_conjunction: cterm * cterm -> cterm |
11 val mk_conjunction: cterm * cterm -> cterm |
12 val mk_conjunction_list: cterm list -> cterm |
|
13 val mk_conjunction_balanced: cterm list -> cterm |
12 val mk_conjunction_balanced: cterm list -> cterm |
14 val dest_conjunction: cterm -> cterm * cterm |
13 val dest_conjunction: cterm -> cterm * cterm |
15 val cong: thm -> thm -> thm |
14 val cong: thm -> thm -> thm |
16 val convs: (cterm -> thm) -> cterm -> thm |
15 val convs: (cterm -> thm) -> cterm -> thm |
17 val conjunctionD1: thm |
16 val conjunctionD1: thm |
18 val conjunctionD2: thm |
17 val conjunctionD2: thm |
19 val conjunctionI: thm |
18 val conjunctionI: thm |
20 val intr: thm -> thm -> thm |
19 val intr: thm -> thm -> thm |
21 val intr_list: thm list -> thm |
|
22 val intr_balanced: thm list -> thm |
20 val intr_balanced: thm list -> thm |
23 val elim: thm -> thm * thm |
21 val elim: thm -> thm * thm |
24 val elim_list: thm -> thm list |
|
25 val elim_balanced: int -> thm -> thm list |
22 val elim_balanced: int -> thm -> thm list |
26 val curry_balanced: int -> thm -> thm |
23 val curry_balanced: int -> thm -> thm |
27 val uncurry_balanced: int -> thm -> thm |
24 val uncurry_balanced: int -> thm -> thm |
28 end; |
25 end; |
29 |
26 |
37 |
34 |
38 val true_prop = cert Logic.true_prop; |
35 val true_prop = cert Logic.true_prop; |
39 val conjunction = cert Logic.conjunction; |
36 val conjunction = cert Logic.conjunction; |
40 |
37 |
41 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B; |
38 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B; |
42 |
|
43 fun mk_conjunction_list [] = true_prop |
|
44 | mk_conjunction_list ts = foldr1 mk_conjunction ts; |
|
45 |
39 |
46 fun mk_conjunction_balanced [] = true_prop |
40 fun mk_conjunction_balanced [] = true_prop |
47 | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts; |
41 | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts; |
48 |
42 |
49 fun dest_conjunction ct = |
43 fun dest_conjunction ct = |
112 end; |
106 end; |
113 |
107 |
114 end; |
108 end; |
115 |
109 |
116 |
110 |
117 (* multiple conjuncts *) |
111 (* balanced conjuncts *) |
118 |
|
119 fun intr_list [] = asm_rl |
|
120 | intr_list ths = foldr1 (uncurry intr) ths; |
|
121 |
112 |
122 fun intr_balanced [] = asm_rl |
113 fun intr_balanced [] = asm_rl |
123 | intr_balanced ths = BalancedTree.make (uncurry intr) ths; |
114 | intr_balanced ths = BalancedTree.make (uncurry intr) ths; |
124 |
|
125 fun elim_list th = (* FIXME improper!? rename to "elims" *) |
|
126 let val (th1, th2) = elim th |
|
127 in elim_list th1 @ elim_list th2 end handle THM _ => [th]; |
|
128 |
115 |
129 fun elim_balanced 0 _ = [] |
116 fun elim_balanced 0 _ = [] |
130 | elim_balanced n th = BalancedTree.dest elim n th; |
117 | elim_balanced n th = BalancedTree.dest elim n th; |
131 |
118 |
132 |
119 |