equal
deleted
inserted
replaced
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"; 