14 (*** term_rec -- by Vset recursion ***) |
14 (*** term_rec -- by Vset recursion ***) |
15 |
15 |
16 (*Lemma: map works correctly on the underlying list of terms*) |
16 (*Lemma: map works correctly on the underlying list of terms*) |
17 val [major,ordi] = goal ListFn.thy |
17 val [major,ordi] = goal ListFn.thy |
18 "[| l: list(A); Ord(i) |] ==> \ |
18 "[| l: list(A); Ord(i) |] ==> \ |
19 \ rank(l): i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)"; |
19 \ rank(l)<i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)"; |
20 by (rtac (major RS List.induct) 1); |
20 by (rtac (major RS List.induct) 1); |
21 by (simp_tac list_ss 1); |
21 by (simp_tac list_ss 1); |
22 by (rtac impI 1); |
22 by (rtac impI 1); |
23 by (forward_tac [rank_Cons1 RS Ord_trans] 1); |
23 by (forward_tac [rank_Cons1 RS lt_trans] 1); |
24 by (dtac (rank_Cons2 RS Ord_trans) 2); |
24 by (dtac (rank_Cons2 RS lt_trans) 1); |
25 by (ALLGOALS (asm_simp_tac (list_ss addsimps [ordi, VsetI]))); |
25 by (asm_simp_tac (list_ss addsimps [ordi, VsetI]) 1); |
26 val map_lemma = result(); |
26 val map_lemma = result(); |
27 |
27 |
28 (*Typing premise is necessary to invoke map_lemma*) |
28 (*Typing premise is necessary to invoke map_lemma*) |
29 val [prem] = goal TermFn.thy |
29 val [prem] = goal TermFn.thy |
30 "ts: list(A) ==> \ |
30 "ts: list(A) ==> \ |