equal
deleted
inserted
replaced
13 val [tc] = chopr.tcs; |
13 val [tc] = chopr.tcs; |
14 goalw_cterm [reducing_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc)); |
14 goalw_cterm [reducing_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc)); |
15 by (blast_tac (claset() addDs [sym]) 1); |
15 by (blast_tac (claset() addDs [sym]) 1); |
16 val lemma = result(); |
16 val lemma = result(); |
17 |
17 |
18 val chopr_rule = let val [chopr_rule] = chopr.rules in lemma RS chopr_rule end; |
18 val chopr_rule = let val [chopr_rule] = chopr.simps in lemma RS chopr_rule end; |
19 |
19 |
20 Goalw [chop_def] "reducing splitf ==> \ |
20 Goalw [chop_def] "reducing splitf ==> \ |
21 \ chop splitf xs = (let (pre,post) = splitf xs \ |
21 \ chop splitf xs = (let (pre,post) = splitf xs \ |
22 \ in if pre=[] then ([],xs) \ |
22 \ in if pre=[] then ([],xs) \ |
23 \ else let (xss,zs) = chop splitf post \ |
23 \ else let (xss,zs) = chop splitf post \ |