src/HOL/UNITY/AllocBase.ML
author nipkow
Wed Aug 30 16:29:21 2000 +0200 (2000-08-30)
changeset 9747 043098ba5098
parent 9336 9ae89b9ce206
child 10265 4e004b548049
permissions -rw-r--r--
introduced induct_thm_tac
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@9109
    12
Goal "!!f :: nat=>nat. \
paulson@9109
    13
\     (ALL i. i<n --> f i <= g i) --> \
paulson@9109
    14
\     setsum f (lessThan n) <= setsum g (lessThan n)";
paulson@8928
    15
by (induct_tac "n" 1);
paulson@9109
    16
by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
paulson@8928
    17
by (dres_inst_tac [("x","n")] spec 1);
paulson@8928
    18
by (arith_tac 1);
paulson@9109
    19
qed_spec_mp "setsum_fun_mono";
paulson@8928
    20
paulson@8928
    21
Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
paulson@8928
    22
by (induct_tac "ys" 1);
paulson@8928
    23
by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
paulson@8928
    24
qed_spec_mp "tokens_mono_prefix";
paulson@8928
    25
paulson@8928
    26
Goalw [mono_def] "mono tokens";
paulson@8928
    27
by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
paulson@8928
    28
qed "mono_tokens";
paulson@8989
    29
paulson@9026
    30
paulson@9026
    31
(** bag_of **)
paulson@8989
    32
paulson@9026
    33
Goal "bag_of (l@l') = bag_of l + bag_of l'";
paulson@9026
    34
by (induct_tac "l" 1);
paulson@9026
    35
 by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2);
paulson@9026
    36
by (Simp_tac 1);
paulson@9026
    37
qed "bag_of_append";
paulson@9026
    38
Addsimps [bag_of_append];
paulson@9026
    39
paulson@9026
    40
Goal "mono (bag_of :: 'a list => ('a::order) multiset)";
paulson@9026
    41
by (rtac monoI 1); 
paulson@9026
    42
by (rewtac prefix_def);
paulson@9026
    43
by (etac genPrefix.induct 1);
paulson@9026
    44
by Auto_tac;
paulson@9026
    45
by (asm_full_simp_tac (simpset() addsimps [union_le_mono]) 1); 
paulson@9026
    46
by (etac order_trans 1); 
paulson@9026
    47
by (rtac union_upper1 1); 
paulson@9026
    48
qed "mono_bag_of";
paulson@9026
    49
paulson@9107
    50
(** setsum **)
paulson@9107
    51
paulson@9107
    52
Addcongs [setsum_cong];
paulson@9107
    53
paulson@9107
    54
Goal "setsum (%i. {#if i<k then f i else g i#}) (A Int lessThan k) = \
paulson@9107
    55
\     setsum (%i. {#f i#}) (A Int lessThan k)";
paulson@9107
    56
by (rtac setsum_cong 1);
paulson@9107
    57
by Auto_tac;  
paulson@9026
    58
qed "bag_of_sublist_lemma";
paulson@9026
    59
paulson@9107
    60
Goal "bag_of (sublist l A) = \
paulson@9107
    61
\     setsum (%i. {# l!i #}) (A Int lessThan (length l))";
nipkow@9747
    62
by (rev_induct_tac "l" 1);
paulson@9026
    63
by (Simp_tac 1);
paulson@9107
    64
by (asm_simp_tac
paulson@9107
    65
    (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc, 
paulson@9107
    66
                    nth_append, bag_of_sublist_lemma] @ thms "plus_ac0") 1);
paulson@9026
    67
qed "bag_of_sublist";
paulson@9026
    68
paulson@9107
    69
paulson@9107
    70
Goal "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
paulson@9107
    71
\     bag_of (sublist l A) + bag_of (sublist l B)";
paulson@9107
    72
by (subgoal_tac "A Int B Int {..length l(} = \
paulson@9107
    73
\                (A Int {..length l(}) Int (B Int {..length l(})" 1);
paulson@9107
    74
by (asm_simp_tac (simpset() addsimps [bag_of_sublist, Int_Un_distrib2, 
paulson@9107
    75
                                      setsum_Un_Int]) 1);
paulson@9107
    76
by (Blast_tac 1);
paulson@9026
    77
qed "bag_of_sublist_Un_Int";
paulson@9107
    78
paulson@9107
    79
Goal "A Int B = {} \
paulson@9107
    80
\     ==> bag_of (sublist l (A Un B)) = \
paulson@9107
    81
\         bag_of (sublist l A) + bag_of (sublist l B)"; 
paulson@9107
    82
by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1);
paulson@9107
    83
qed "bag_of_sublist_Un_disjoint";
paulson@9107
    84
paulson@9107
    85
Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
paulson@9107
    86
\     ==> bag_of (sublist l (UNION I A)) =  \
paulson@9107
    87
\         setsum (%i. bag_of (sublist l (A i))) I";  
paulson@9107
    88
by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
paulson@9107
    89
			    addsimps [bag_of_sublist]) 1);
paulson@9107
    90
by (stac setsum_UN_disjoint 1);
paulson@9107
    91
by Auto_tac;  
paulson@9107
    92
qed_spec_mp "bag_of_sublist_UN_disjoint";