equal
deleted
inserted
replaced
6 |
6 |
7 (** sum_case -- the selection operator for sums **) |
7 (** sum_case -- the selection operator for sums **) |
8 |
8 |
9 (*compatibility*) |
9 (*compatibility*) |
10 val [sum_case_Inl, sum_case_Inr] = sum.cases; |
10 val [sum_case_Inl, sum_case_Inr] = sum.cases; |
|
11 bind_thm ("sum_case_Inl", sum_case_Inl); |
|
12 bind_thm ("sum_case_Inr", sum_case_Inr); |
11 |
13 |
12 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; |
14 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; |
13 by (EVERY1 [res_inst_tac [("s","s")] sumE, |
15 by (EVERY1 [res_inst_tac [("s","s")] sumE, |
14 etac ssubst, rtac sum_case_Inl, |
16 etac ssubst, rtac sum_case_Inl, |
15 etac ssubst, rtac sum_case_Inr]); |
17 etac ssubst, rtac sum_case_Inr]); |