src/HOL/Lex/Prefix.ML
changeset 6675 63e53327f5e5
parent 5619 76a8c72e3fd4
child 6808 d5dfe040c183
equal deleted inserted replaced
6674:32892a8ecb15 6675:63e53327f5e5
    18 
    18 
    19 Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
    19 Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
    20 by (Clarify_tac 1);
    20 by (Clarify_tac 1);
    21 by (Asm_full_simp_tac 1);
    21 by (Asm_full_simp_tac 1);
    22 qed "prefix_antisym";
    22 qed "prefix_antisym";
       
    23 
       
    24 Goalw [strict_prefix_def] "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)";
       
    25 by Auto_tac;
       
    26 qed "prefix_less_le";
       
    27 
    23 
    28 
    24 (** recursion equations **)
    29 (** recursion equations **)
    25 
    30 
    26 Goalw [prefix_def] "[] <= xs";
    31 Goalw [prefix_def] "[] <= xs";
    27 by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    32 by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    96 qed "append_one_prefix";
   101 qed "append_one_prefix";
    97 
   102 
    98 Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";
   103 Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";
    99 by Auto_tac;
   104 by Auto_tac;
   100 qed "prefix_length_le";
   105 qed "prefix_length_le";
       
   106 
       
   107 Goal "mono length";
       
   108 by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1);
       
   109 qed "mono_length";