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
     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 "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n";
    13 by (induct_tac "n" 1);
    14 by Auto_tac;
    15 by (dres_inst_tac [("x","n")] spec 1);
    16 by Auto_tac;
    17 by (arith_tac 1);
    18 qed_spec_mp "sum_mono";
    19 
    20 Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
    21 by (induct_tac "ys" 1);
    22 by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
    23 qed_spec_mp "tokens_mono_prefix";
    24 
    25 Goalw [mono_def] "mono tokens";
    26 by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
    27 qed "mono_tokens";
    28 
    29 
    30 (*** sublist ***)
    31 
    32 Goalw [sublist_def] "sublist l {} = []";
    33 by Auto_tac;
    34 qed "sublist_empty";
    35 
    36 Goalw [sublist_def] "sublist [] A = []";
    37 by Auto_tac;
    38 qed "sublist_nil";
    39 
    40 Goal "map fst [p:zip xs [i..i + length xs(] . snd p : A] =     \
    41 \     map fst [p:zip xs [0..length xs(] . snd p + i : A]";
    42 by (res_inst_tac [("xs","xs")] rev_induct 1);
    43  by (asm_simp_tac (simpset() addsimps [add_commute]) 2);
    44 by (Simp_tac 1);
    45 qed "sublist_shift_lemma";
    46 
    47 Goalw [sublist_def]
    48      "sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}";
    49 by (res_inst_tac [("xs","l'")] rev_induct 1);
    50 by (Simp_tac 1);
    51 by (asm_simp_tac (simpset() addsimps [inst "i" "0" upt_add_eq_append, 
    52 	                              zip_append, sublist_shift_lemma]) 1);
    53 by (asm_simp_tac (simpset() addsimps [add_commute]) 1);
    54 qed "sublist_append";
    55 
    56 Addsimps [sublist_empty, sublist_nil];
    57 
    58 Goal "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}";
    59 by (res_inst_tac [("xs","l")] rev_induct 1);
    60  by (asm_simp_tac (simpset() delsimps [append_Cons]
    61 	 		     addsimps [append_Cons RS sym, sublist_append]) 2);
    62 by (simp_tac (simpset() addsimps [sublist_def]) 1);
    63 qed "sublist_Cons";
    64 
    65 Goal "sublist [x] A = (if 0 : A then [x] else [])";
    66 by (simp_tac (simpset() addsimps [sublist_Cons]) 1);
    67 qed "sublist_singleton";
    68 Addsimps [sublist_singleton];
    69 
    70 Goal "sublist l {..n(} = take n l";
    71 by (res_inst_tac [("xs","l")] rev_induct 1);
    72  by (asm_simp_tac (simpset() addsplits [nat_diff_split]
    73                              addsimps [sublist_append]) 2);
    74 by (Simp_tac 1);
    75 qed "sublist_upt_eq_take";
    76 Addsimps [sublist_upt_eq_take];
    77 
    78 
    79 (** bag_of **)
    80 
    81 Goal "bag_of (l@l') = bag_of l + bag_of l'";
    82 by (induct_tac "l" 1);
    83  by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2);
    84 by (Simp_tac 1);
    85 qed "bag_of_append";
    86 Addsimps [bag_of_append];
    87 
    88 Goal "mono (bag_of :: 'a list => ('a::order) multiset)";
    89 by (rtac monoI 1); 
    90 by (rewtac prefix_def);
    91 by (etac genPrefix.induct 1);
    92 by Auto_tac;
    93 by (asm_full_simp_tac (simpset() addsimps [union_le_mono]) 1); 
    94 by (etac order_trans 1); 
    95 by (rtac union_upper1 1); 
    96 qed "mono_bag_of";
    97 
    98 Goal "finite A ==> \
    99 \     setsum (%i. if i < Suc(length zs) then {#(zs @ [z]) ! i#} else {#}) A = \
   100 \       setsum (%i. if i < length zs then {#zs ! i#} else {#}) A + \
   101 \       (if length zs : A then {#z#} else {#})";
   102 by (etac finite_induct 1);
   103 by (Simp_tac 1);
   104 by (asm_simp_tac (simpset() addsimps (nth_append :: thms "plus_ac0")) 1);
   105 by (subgoal_tac "x < Suc (length zs) & ~ x < length zs --> length zs = x" 1);
   106 by Auto_tac;
   107 qed "bag_of_sublist_lemma";
   108 
   109 Goal "finite A \
   110 \     ==> bag_of (sublist l A) = \
   111 \         setsum (%i. if i < length l then {# nth l i #} else {#}) A";
   112 by (res_inst_tac [("xs","l")] rev_induct 1);
   113 by (Simp_tac 1);
   114 by (stac (symmetric Zero_def) 1);
   115 by (rtac (setsum_0 RS sym) 1);
   116 by (asm_simp_tac (simpset() addsimps [sublist_append, 
   117 				      bag_of_sublist_lemma]) 1);
   118 qed "bag_of_sublist";
   119 
   120 Goal "[| finite A; finite B |] \
   121 \     ==> bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
   122 \         bag_of (sublist l A) + bag_of (sublist l B)";
   123 by (asm_simp_tac (simpset() addsimps [bag_of_sublist, setsum_Un_Int]) 1);
   124 qed "bag_of_sublist_Un_Int";