1465

1 
(* Title: HOL/Lex/Prefix.thy

1344

2 
ID: $Id$

1465

3 
Author: Richard Mayr & Tobias Nipkow

1344

4 
Copyright 1995 TUM


5 
*)


6 

4643

7 
(** <= is a partial order: **)


8 

5069

9 
Goalw [prefix_def] "xs <= (xs::'a list)";

5132

10 
by (Simp_tac 1);

4643

11 
qed "prefix_refl";

4647

12 
AddIffs[prefix_refl];

4643

13 

5069

14 
Goalw [prefix_def] "!!xs::'a list. [ xs <= ys; ys <= zs ] ==> xs <= zs";

5132

15 
by (Clarify_tac 1);


16 
by (Simp_tac 1);

4643

17 
qed "prefix_trans";


18 

5069

19 
Goalw [prefix_def] "!!xs::'a list. [ xs <= ys; ys <= xs ] ==> xs = ys";

5132

20 
by (Clarify_tac 1);


21 
by (Asm_full_simp_tac 1);

4643

22 
qed "prefix_antisym";


23 


24 
(** recursion equations **)


25 

5069

26 
Goalw [prefix_def] "[] <= xs";

4089

27 
by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);

1344

28 
qed "Nil_prefix";

4647

29 
AddIffs[Nil_prefix];

1344

30 

5069

31 
Goalw [prefix_def] "(xs <= []) = (xs = [])";

5184

32 
by (induct_tac "xs" 1);

1344

33 
by (Simp_tac 1);


34 
by (Simp_tac 1);


35 
qed "prefix_Nil";


36 
Addsimps [prefix_Nil];


37 

5069

38 
Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y]  xs <= ys)";

5132

39 
by (rtac iffI 1);


40 
by (etac exE 1);


41 
by (rename_tac "zs" 1);


42 
by (res_inst_tac [("xs","zs")] rev_exhaust 1);


43 
by (Asm_full_simp_tac 1);


44 
by (hyp_subst_tac 1);


45 
by (asm_full_simp_tac (simpset() delsimps [append_assoc]

4643

46 
addsimps [append_assoc RS sym])1);

5132

47 
by (etac disjE 1);


48 
by (Asm_simp_tac 1);


49 
by (Clarify_tac 1);

4643

50 
by (Simp_tac 1);


51 
qed "prefix_snoc";


52 
Addsimps [prefix_snoc];


53 

5069

54 
Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";

4643

55 
by (Simp_tac 1);


56 
by (Fast_tac 1);


57 
qed"Cons_prefix_Cons";


58 
Addsimps [Cons_prefix_Cons];


59 

5069

60 
Goal "(xs@ys <= xs@zs) = (ys <= zs)";

4647

61 
by (induct_tac "xs" 1);

5132

62 
by (ALLGOALS Asm_simp_tac);

4647

63 
qed "same_prefix_prefix";


64 
Addsimps [same_prefix_prefix];


65 

5456

66 
AddIffs (* (xs@ys <= xs) = (ys <= []) *)

4647

67 
[simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];


68 

5118

69 
Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";

5132

70 
by (Clarify_tac 1);

4643

71 
by (Simp_tac 1);


72 
qed "prefix_prefix";


73 
Addsimps [prefix_prefix];


74 

5069

75 
Goalw [prefix_def]

1344

76 
"(xs <= y#ys) = (xs=[]  (? zs. xs=y#zs & zs <= ys))";

5456

77 
by (exhaust_tac "xs" 1);


78 
by Auto_tac;

1344

79 
qed "prefix_Cons";

4647

80 

5069

81 
Goal "(xs <= ys@zs) = (xs <= ys  (? us. xs = ys@us & us <= zs))";

5132

82 
by (res_inst_tac [("xs","zs")] rev_induct 1);


83 
by (Simp_tac 1);


84 
by (Blast_tac 1);


85 
by (asm_full_simp_tac (simpset() delsimps [append_assoc]

5456

86 
addsimps [append_assoc RS sym])1);

5132

87 
by (Simp_tac 1);


88 
by (Blast_tac 1);

4647

89 
qed "prefix_append";

5619

90 


91 
Goalw [prefix_def]


92 
"[ xs <= ys; length xs < length ys ] ==> xs @ [ys ! length xs] <= ys";


93 
by (auto_tac(claset(), simpset() addsimps [nth_append]));


94 
by (exhaust_tac "ys" 1);


95 
by Auto_tac;


96 
qed "append_one_prefix";


97 


98 
Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";


99 
by Auto_tac;


100 
qed "prefix_length_le";
