44 val prems = goal Type.thy |
44 val prems = goal Type.thy |
45 "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B"; |
45 "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B"; |
46 by (cut_facts_tac prems 1); |
46 by (cut_facts_tac prems 1); |
47 by (etac (letB RS ssubst) 1); |
47 by (etac (letB RS ssubst) 1); |
48 by (assume_tac 1); |
48 by (assume_tac 1); |
49 val letT = result(); |
49 qed "letT"; |
50 |
50 |
51 val prems = goal Type.thy |
51 val prems = goal Type.thy |
52 "[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)"; |
52 "[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)"; |
53 by (REPEAT (ares_tac (applyT::prems) 1)); |
53 by (REPEAT (ares_tac (applyT::prems) 1)); |
54 val applyT2 = result(); |
54 qed "applyT2"; |
55 |
55 |
56 val prems = goal Type.thy |
56 val prems = goal Type.thy |
57 "[| a:A; a:A ==> P(a) |] ==> a : {x:A.P(x)}"; |
57 "[| a:A; a:A ==> P(a) |] ==> a : {x:A.P(x)}"; |
58 by (fast_tac (type_cs addSIs prems) 1); |
58 by (fast_tac (type_cs addSIs prems) 1); |
59 val rcall_lemma1 = result(); |
59 qed "rcall_lemma1"; |
60 |
60 |
61 val prems = goal Type.thy |
61 val prems = goal Type.thy |
62 "[| a:{x:A.Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A.P(x)}"; |
62 "[| a:{x:A.Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A.P(x)}"; |
63 by (cut_facts_tac prems 1); |
63 by (cut_facts_tac prems 1); |
64 by (fast_tac (type_cs addSIs prems) 1); |
64 by (fast_tac (type_cs addSIs prems) 1); |
65 val rcall_lemma2 = result(); |
65 qed "rcall_lemma2"; |
66 |
66 |
67 val rcall_lemmas = [asm_rl,rcall_lemma1,SubtypeD1,rcall_lemma2]; |
67 val rcall_lemmas = [asm_rl,rcall_lemma1,SubtypeD1,rcall_lemma2]; |
68 |
68 |
69 (***********************************TYPECHECKING*************************************) |
69 (***********************************TYPECHECKING*************************************) |
70 |
70 |