src/HOL/Integ/Bin.ML
changeset 7517 bad2f36810e1
parent 7074 e0730ffaafcc
child 7549 1dcf2a7a2b5b
equal deleted inserted replaced
7516:a1d476251238 7517:bad2f36810e1
    72 Goal "bin_add w Pls = w";
    72 Goal "bin_add w Pls = w";
    73 by (induct_tac "w" 1);
    73 by (induct_tac "w" 1);
    74 by Auto_tac;
    74 by Auto_tac;
    75 qed "bin_add_Pls_right";
    75 qed "bin_add_Pls_right";
    76 
    76 
    77 Goal "bin_add (v BIT x) Min = bin_pred (v BIT x)";
    77 Goal "bin_add w Min = bin_pred w";
    78 by (Simp_tac 1);
    78 by (induct_tac "w" 1);
    79 qed "bin_add_BIT_Min";
    79 by Auto_tac;
       
    80 qed "bin_add_Min_right";
    80 
    81 
    81 Goal "bin_add (v BIT x) (w BIT y) = \
    82 Goal "bin_add (v BIT x) (w BIT y) = \
    82 \    NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)";
    83 \    NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)";
    83 by (Simp_tac 1);
    84 by (Simp_tac 1);
    84 qed "bin_add_BIT_BIT";
    85 qed "bin_add_BIT_BIT";
   407      number_of_minus RS sym,
   408      number_of_minus RS sym,
   408      number_of_mult RS sym,
   409      number_of_mult RS sym,
   409      bin_succ_1, bin_succ_0, 
   410      bin_succ_1, bin_succ_0, 
   410      bin_pred_1, bin_pred_0, 
   411      bin_pred_1, bin_pred_0, 
   411      bin_minus_1, bin_minus_0,  
   412      bin_minus_1, bin_minus_0,  
   412      bin_add_Pls_right, bin_add_BIT_Min,
   413      bin_add_Pls_right, bin_add_Min_right,
   413      bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
   414      bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
   414      diff_number_of_eq, 
   415      diff_number_of_eq, 
   415      bin_mult_1, bin_mult_0, 
   416      bin_mult_1, bin_mult_0, 
   416      NCons_Pls_0, NCons_Pls_1, 
   417      NCons_Pls_0, NCons_Pls_1, 
   417      NCons_Min_0, NCons_Min_1, NCons_BIT];
   418      NCons_Min_0, NCons_Min_1, NCons_BIT];