src/HOL/UNITY/AllocBase.ML
author paulson
Tue Jun 20 11:51:21 2000 +0200 (2000-06-20)
changeset 9090 7141b912b0bb
parent 9026 640c4fd8b5b3
child 9107 67202a50ee6d
permissions -rw-r--r--
changed a step for the improved rules for setsum
paulson@8928
     1
(*  Title:      HOL/UNITY/AllocBase
paulson@8928
     2
    ID:         $Id$
paulson@8928
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@8928
     4
    Copyright   1998  University of Cambridge
paulson@8928
     5
paulson@8928
     6
Basis declarations for Chandy and Charpentier's Allocator
paulson@8989
     7
paulson@9026
     8
add_path "../Induct";
paulson@9026
     9
time_use_thy "AllocBase";
paulson@8928
    10
*)
paulson@8928
    11
paulson@8928
    12
Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n";
paulson@8928
    13
by (induct_tac "n" 1);
paulson@8928
    14
by Auto_tac;
paulson@8928
    15
by (dres_inst_tac [("x","n")] spec 1);
paulson@8928
    16
by Auto_tac;
paulson@8928
    17
by (arith_tac 1);
paulson@8928
    18
qed_spec_mp "sum_mono";
paulson@8928
    19
paulson@8928
    20
Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
paulson@8928
    21
by (induct_tac "ys" 1);
paulson@8928
    22
by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
paulson@8928
    23
qed_spec_mp "tokens_mono_prefix";
paulson@8928
    24
paulson@8928
    25
Goalw [mono_def] "mono tokens";
paulson@8928
    26
by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
paulson@8928
    27
qed "mono_tokens";
paulson@8989
    28
paulson@9026
    29
paulson@9026
    30
(*** sublist ***)
paulson@9026
    31
paulson@9026
    32
Goalw [sublist_def] "sublist l {} = []";
paulson@9026
    33
by Auto_tac;
paulson@9026
    34
qed "sublist_empty";
paulson@9026
    35
paulson@9026
    36
Goalw [sublist_def] "sublist [] A = []";
paulson@8989
    37
by Auto_tac;
paulson@9026
    38
qed "sublist_nil";
paulson@9026
    39
paulson@9026
    40
Goal "map fst [p:zip xs [i..i + length xs(] . snd p : A] =     \
paulson@9026
    41
\     map fst [p:zip xs [0..length xs(] . snd p + i : A]";
paulson@9026
    42
by (res_inst_tac [("xs","xs")] rev_induct 1);
paulson@9026
    43
 by (asm_simp_tac (simpset() addsimps [add_commute]) 2);
paulson@9026
    44
by (Simp_tac 1);
paulson@9026
    45
qed "sublist_shift_lemma";
paulson@9026
    46
paulson@9026
    47
Goalw [sublist_def]
paulson@9026
    48
     "sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}";
paulson@9026
    49
by (res_inst_tac [("xs","l'")] rev_induct 1);
paulson@9026
    50
by (Simp_tac 1);
paulson@9026
    51
by (asm_simp_tac (simpset() addsimps [inst "i" "0" upt_add_eq_append, 
paulson@9026
    52
	                              zip_append, sublist_shift_lemma]) 1);
paulson@9026
    53
by (asm_simp_tac (simpset() addsimps [add_commute]) 1);
paulson@9026
    54
qed "sublist_append";
paulson@9026
    55
paulson@9026
    56
Addsimps [sublist_empty, sublist_nil];
paulson@9026
    57
paulson@9026
    58
Goal "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}";
paulson@9026
    59
by (res_inst_tac [("xs","l")] rev_induct 1);
paulson@9026
    60
 by (asm_simp_tac (simpset() delsimps [append_Cons]
paulson@9026
    61
	 		     addsimps [append_Cons RS sym, sublist_append]) 2);
paulson@9026
    62
by (simp_tac (simpset() addsimps [sublist_def]) 1);
paulson@9026
    63
qed "sublist_Cons";
paulson@9026
    64
paulson@9026
    65
Goal "sublist [x] A = (if 0 : A then [x] else [])";
paulson@9026
    66
by (simp_tac (simpset() addsimps [sublist_Cons]) 1);
paulson@9026
    67
qed "sublist_singleton";
paulson@9026
    68
Addsimps [sublist_singleton];
paulson@9026
    69
paulson@9026
    70
Goal "sublist l {..n(} = take n l";
paulson@9026
    71
by (res_inst_tac [("xs","l")] rev_induct 1);
paulson@9026
    72
 by (asm_simp_tac (simpset() addsplits [nat_diff_split]
paulson@9026
    73
                             addsimps [sublist_append]) 2);
paulson@9026
    74
by (Simp_tac 1);
paulson@9026
    75
qed "sublist_upt_eq_take";
paulson@9026
    76
Addsimps [sublist_upt_eq_take];
paulson@9026
    77
paulson@9026
    78
paulson@9026
    79
(** bag_of **)
paulson@8989
    80
paulson@9026
    81
Goal "bag_of (l@l') = bag_of l + bag_of l'";
paulson@9026
    82
by (induct_tac "l" 1);
paulson@9026
    83
 by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2);
paulson@9026
    84
by (Simp_tac 1);
paulson@9026
    85
qed "bag_of_append";
paulson@9026
    86
Addsimps [bag_of_append];
paulson@9026
    87
paulson@9026
    88
Goal "mono (bag_of :: 'a list => ('a::order) multiset)";
paulson@9026
    89
by (rtac monoI 1); 
paulson@9026
    90
by (rewtac prefix_def);
paulson@9026
    91
by (etac genPrefix.induct 1);
paulson@9026
    92
by Auto_tac;
paulson@9026
    93
by (asm_full_simp_tac (simpset() addsimps [union_le_mono]) 1); 
paulson@9026
    94
by (etac order_trans 1); 
paulson@9026
    95
by (rtac union_upper1 1); 
paulson@9026
    96
qed "mono_bag_of";
paulson@9026
    97
paulson@9026
    98
Goal "finite A ==> \
paulson@9026
    99
\     setsum (%i. if i < Suc(length zs) then {#(zs @ [z]) ! i#} else {#}) A = \
paulson@9026
   100
\       setsum (%i. if i < length zs then {#zs ! i#} else {#}) A + \
paulson@9026
   101
\       (if length zs : A then {#z#} else {#})";
paulson@9026
   102
by (etac finite_induct 1);
paulson@9026
   103
by (Simp_tac 1);
paulson@9026
   104
by (asm_simp_tac (simpset() addsimps (nth_append :: thms "plus_ac0")) 1);
paulson@9026
   105
by (subgoal_tac "x < Suc (length zs) & ~ x < length zs --> length zs = x" 1);
paulson@9026
   106
by Auto_tac;
paulson@9026
   107
qed "bag_of_sublist_lemma";
paulson@9026
   108
paulson@9026
   109
Goal "finite A \
paulson@9026
   110
\     ==> bag_of (sublist l A) = \
paulson@9026
   111
\         setsum (%i. if i < length l then {# nth l i #} else {#}) A";
paulson@9026
   112
by (res_inst_tac [("xs","l")] rev_induct 1);
paulson@9026
   113
by (Simp_tac 1);
paulson@9026
   114
by (stac (symmetric Zero_def) 1);
paulson@9090
   115
by (rtac (setsum_0 RS sym) 1);
paulson@9026
   116
by (asm_simp_tac (simpset() addsimps [sublist_append, 
paulson@9026
   117
				      bag_of_sublist_lemma]) 1);
paulson@9026
   118
qed "bag_of_sublist";
paulson@9026
   119
paulson@9026
   120
Goal "[| finite A; finite B |] \
paulson@9026
   121
\     ==> bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
paulson@9026
   122
\         bag_of (sublist l A) + bag_of (sublist l B)";
paulson@9026
   123
by (asm_simp_tac (simpset() addsimps [bag_of_sublist, setsum_Un_Int]) 1);
paulson@9026
   124
qed "bag_of_sublist_Un_Int";