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
     1 (*  Title:      HOL/UNITY/AllocBase
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Basis declarations for Chandy and Charpentier's Allocator
     7 
     8 add_path "../Induct";
     9 time_use_thy "AllocBase";
    10 *)
    11 
    12 Goal "!!f :: nat=>nat. \
    13 \     (ALL i. i<n --> f i <= g i) --> \
    14 \     setsum f (lessThan n) <= setsum g (lessThan n)";
    15 by (induct_tac "n" 1);
    16 by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
    17 by (dres_inst_tac [("x","n")] spec 1);
    18 by (arith_tac 1);
    19 qed_spec_mp "setsum_fun_mono";
    20 
    21 Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
    22 by (induct_tac "ys" 1);
    23 by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
    24 qed_spec_mp "tokens_mono_prefix";
    25 
    26 Goalw [mono_def] "mono tokens";
    27 by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
    28 qed "mono_tokens";
    29 
    30 
    31 (** bag_of **)
    32 
    33 Goal "bag_of (l@l') = bag_of l + bag_of l'";
    34 by (induct_tac "l" 1);
    35  by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2);
    36 by (Simp_tac 1);
    37 qed "bag_of_append";
    38 Addsimps [bag_of_append];
    39 
    40 Goal "mono (bag_of :: 'a list => ('a::order) multiset)";
    41 by (rtac monoI 1); 
    42 by (rewtac prefix_def);
    43 by (etac genPrefix.induct 1);
    44 by Auto_tac;
    45 by (asm_full_simp_tac (simpset() addsimps [union_le_mono]) 1); 
    46 by (etac order_trans 1); 
    47 by (rtac union_upper1 1); 
    48 qed "mono_bag_of";
    49 
    50 (** setsum **)
    51 
    52 Addcongs [setsum_cong];
    53 
    54 Goal "setsum (%i. {#if i<k then f i else g i#}) (A Int lessThan k) = \
    55 \     setsum (%i. {#f i#}) (A Int lessThan k)";
    56 by (rtac setsum_cong 1);
    57 by Auto_tac;  
    58 qed "bag_of_sublist_lemma";
    59 
    60 Goal "bag_of (sublist l A) = \
    61 \     setsum (%i. {# l!i #}) (A Int lessThan (length l))";
    62 by (rev_induct_tac "l" 1);
    63 by (Simp_tac 1);
    64 by (asm_simp_tac
    65     (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc, 
    66                     nth_append, bag_of_sublist_lemma] @ thms "plus_ac0") 1);
    67 qed "bag_of_sublist";
    68 
    69 
    70 Goal "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
    71 \     bag_of (sublist l A) + bag_of (sublist l B)";
    72 by (subgoal_tac "A Int B Int {..length l(} = \
    73 \                (A Int {..length l(}) Int (B Int {..length l(})" 1);
    74 by (asm_simp_tac (simpset() addsimps [bag_of_sublist, Int_Un_distrib2, 
    75                                       setsum_Un_Int]) 1);
    76 by (Blast_tac 1);
    77 qed "bag_of_sublist_Un_Int";
    78 
    79 Goal "A Int B = {} \
    80 \     ==> bag_of (sublist l (A Un B)) = \
    81 \         bag_of (sublist l A) + bag_of (sublist l B)"; 
    82 by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1);
    83 qed "bag_of_sublist_Un_disjoint";
    84 
    85 Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
    86 \     ==> bag_of (sublist l (UNION I A)) =  \
    87 \         setsum (%i. bag_of (sublist l (A i))) I";  
    88 by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
    89 			    addsimps [bag_of_sublist]) 1);
    90 by (stac setsum_UN_disjoint 1);
    91 by Auto_tac;  
    92 qed_spec_mp "bag_of_sublist_UN_disjoint";