equal
deleted
inserted
replaced
35 (** Elimination -- structural induction on the set term(A) **) |
35 (** Elimination -- structural induction on the set term(A) **) |
36 |
36 |
37 (*Induction for the set term(A) *) |
37 (*Induction for the set term(A) *) |
38 val [major,minor] = goal Term.thy |
38 val [major,minor] = goal Term.thy |
39 "[| M: term(A); \ |
39 "[| M: term(A); \ |
40 \ !!x zs. [| x: A; zs: list(term(A)); zs: list({x.R(x)}) \ |
40 \ !!x zs. [| x: A; zs: list(term(A)); zs: list({x. R(x)}) \ |
41 \ |] ==> R(x$zs) \ |
41 \ |] ==> R(x$zs) \ |
42 \ |] ==> R(M)"; |
42 \ |] ==> R(M)"; |
43 by (rtac (major RS term.induct) 1); |
43 by (rtac (major RS term.induct) 1); |
44 by (REPEAT (eresolve_tac ([minor] @ |
44 by (REPEAT (eresolve_tac ([minor] @ |
45 ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1)); |
45 ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1)); |