|
7626
|
1 |
(* Title: HOL/BCV/Plus.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1999 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
(** option **)
|
|
|
8 |
|
|
|
9 |
Goalw [plus_option] "x+None = x";
|
|
7961
|
10 |
by (simp_tac (simpset() addsplits [option.split]) 1);
|
|
7626
|
11 |
qed "plus_None";
|
|
|
12 |
Addsimps [plus_None];
|
|
|
13 |
|
|
|
14 |
Goalw [plus_option] "None+x = x";
|
|
7961
|
15 |
by (simp_tac (simpset() addsplits [option.split]) 1);
|
|
7626
|
16 |
qed "None_plus";
|
|
|
17 |
Addsimps [None_plus];
|
|
|
18 |
|
|
|
19 |
Goalw [plus_option] "Some x + Some y = Some(x+y)";
|
|
7961
|
20 |
by (Simp_tac 1);
|
|
7626
|
21 |
qed "Some_plus_Some";
|
|
|
22 |
Addsimps [Some_plus_Some];
|
|
|
23 |
|
|
|
24 |
Goalw [plus_option] "? y. Some x + opt = Some y";
|
|
7961
|
25 |
by (simp_tac (simpset() addsplits [option.split]) 1);
|
|
7626
|
26 |
qed "plus_option_Some_Some";
|
|
|
27 |
|
|
|
28 |
(** list **)
|
|
|
29 |
|
|
|
30 |
Goal "list_plus xs [] = xs";
|
|
7961
|
31 |
by (induct_tac "xs" 1);
|
|
|
32 |
by (Simp_tac 1);
|
|
|
33 |
by (asm_simp_tac (simpset() addsplits [list.split]) 1);
|
|
7626
|
34 |
qed "list_plus_Nil2";
|
|
|
35 |
Addsimps [list_plus_Nil2];
|
|
|
36 |
|
|
|
37 |
Goal "!ys. length(list_plus xs ys) = max(length xs) (length ys)";
|
|
7961
|
38 |
by (induct_tac "xs" 1);
|
|
|
39 |
by (Simp_tac 1);
|
|
|
40 |
by (asm_simp_tac (simpset() addsplits [list.split]) 1);
|
|
7626
|
41 |
qed_spec_mp "length_list_plus";
|
|
|
42 |
Addsimps [length_list_plus];
|
|
|
43 |
|
|
|
44 |
Goalw [plus_list]
|
|
|
45 |
"length(ts+us) = max (length ts) (length us)";
|
|
7961
|
46 |
by (Simp_tac 1);
|
|
7626
|
47 |
qed "length_plus_list";
|
|
|
48 |
Addsimps [length_plus_list];
|