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 
(* Junk: *)

3842

8 
val [maj,min] = goal Prefix.thy "[ Q([]); !! y ys. Q(y#ys) ] ==> ! l. Q(l)";

1465

9 
by (rtac allI 1);

1344

10 
by (list.induct_tac "l" 1);

1465

11 
by (rtac maj 1);


12 
by (rtac min 1);

1344

13 
val list_cases = result();


14 

4643

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


16 

5069

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

5132

18 
by (Simp_tac 1);

4643

19 
qed "prefix_refl";

4647

20 
AddIffs[prefix_refl];

4643

21 

5069

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

5132

23 
by (Clarify_tac 1);


24 
by (Simp_tac 1);

4643

25 
qed "prefix_trans";


26 

5069

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

5132

28 
by (Clarify_tac 1);


29 
by (Asm_full_simp_tac 1);

4643

30 
qed "prefix_antisym";


31 


32 
(** recursion equations **)


33 

5069

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

4089

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

1344

36 
qed "Nil_prefix";

4647

37 
AddIffs[Nil_prefix];

1344

38 

5069

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

1344

40 
by (list.induct_tac "xs" 1);


41 
by (Simp_tac 1);


42 
by (Simp_tac 1);


43 
qed "prefix_Nil";


44 
Addsimps [prefix_Nil];


45 

5069

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

5132

47 
by (rtac iffI 1);


48 
by (etac exE 1);


49 
by (rename_tac "zs" 1);


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


51 
by (Asm_full_simp_tac 1);


52 
by (hyp_subst_tac 1);


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

4643

54 
addsimps [append_assoc RS sym])1);

5132

55 
by (etac disjE 1);


56 
by (Asm_simp_tac 1);


57 
by (Clarify_tac 1);

4643

58 
by (Simp_tac 1);


59 
qed "prefix_snoc";


60 
Addsimps [prefix_snoc];


61 

5069

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

4643

63 
by (Simp_tac 1);


64 
by (Fast_tac 1);


65 
qed"Cons_prefix_Cons";


66 
Addsimps [Cons_prefix_Cons];


67 

5069

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

4647

69 
by (induct_tac "xs" 1);

5132

70 
by (ALLGOALS Asm_simp_tac);

4647

71 
qed "same_prefix_prefix";


72 
Addsimps [same_prefix_prefix];


73 


74 
AddIffs


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


76 

5118

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

5132

78 
by (Clarify_tac 1);

4643

79 
by (Simp_tac 1);


80 
qed "prefix_prefix";


81 
Addsimps [prefix_prefix];


82 

1344

83 
(* nicht sehr elegant bewiesen  Induktion eigentlich ueberfluessig *)

5069

84 
Goalw [prefix_def]

1344

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


86 
by (list.induct_tac "xs" 1);


87 
by (Simp_tac 1);


88 
by (Simp_tac 1);

1894

89 
by (Fast_tac 1);

1344

90 
qed "prefix_Cons";

4647

91 

5069

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

5132

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


94 
by (Simp_tac 1);


95 
by (Blast_tac 1);


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

4647

97 
addsimps [append_assoc RS sym])1);

5132

98 
by (Simp_tac 1);


99 
by (Blast_tac 1);

4647

100 
qed "prefix_append";
