equal
deleted
inserted
replaced
74 lemmas simple = s_b strip_s strip_b app lam_ss pi_ss |
74 lemmas simple = s_b strip_s strip_b app lam_ss pi_ss |
75 lemmas rules = simple |
75 lemmas rules = simple |
76 |
76 |
77 lemma imp_elim: |
77 lemma imp_elim: |
78 assumes "f:A->B" and "a:A" and "f^a:B ==> PROP P" |
78 assumes "f:A->B" and "a:A" and "f^a:B ==> PROP P" |
79 shows "PROP P" by (rule app prems)+ |
79 shows "PROP P" by (rule app assms)+ |
80 |
80 |
81 lemma pi_elim: |
81 lemma pi_elim: |
82 assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P" |
82 assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P" |
83 shows "PROP P" by (rule app prems)+ |
83 shows "PROP P" by (rule app assms)+ |
84 |
84 |
85 |
85 |
86 locale L2 = |
86 locale L2 = |
87 assumes pi_bs: "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*" |
87 assumes pi_bs: "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*" |
88 and lam_bs: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] |
88 and lam_bs: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] |