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 


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


18 
by(Simp_tac 1);


19 
qed "prefix_refl";


20 
Addsimps[prefix_refl];


21 


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


23 
by(Clarify_tac 1);


24 
by(Simp_tac 1);


25 
qed "prefix_trans";


26 


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


28 
by(Clarify_tac 1);


29 
by(Asm_full_simp_tac 1);


30 
qed "prefix_antisym";


31 


32 
(** recursion equations **)


33 

1344

34 
goalw Prefix.thy [prefix_def] "[] <= xs";

4089

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

1344

36 
qed "Nil_prefix";


37 
Addsimps[Nil_prefix];


38 


39 
goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";


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 

4643

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


47 
br iffI 1;


48 
be exE 1;


49 
by(rename_tac "zs" 1);


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


51 
by(Asm_full_simp_tac 1);


52 
by(hyp_subst_tac 1);


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


54 
addsimps [append_assoc RS sym])1);


55 
be disjE 1;


56 
by(Asm_simp_tac 1);


57 
by(Clarify_tac 1);


58 
by (Simp_tac 1);


59 
qed "prefix_snoc";


60 
Addsimps [prefix_snoc];


61 


62 
goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";


63 
by (Simp_tac 1);


64 
by (Fast_tac 1);


65 
qed"Cons_prefix_Cons";


66 
Addsimps [Cons_prefix_Cons];


67 


68 
goalw thy [prefix_def] "!!xs. xs <= ys ==> xs <= ys@zs";


69 
by(Clarify_tac 1);


70 
by (Simp_tac 1);


71 
qed "prefix_prefix";


72 
Addsimps [prefix_prefix];


73 

1344

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


75 
goalw Prefix.thy [prefix_def]


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


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


78 
by (Simp_tac 1);


79 
by (Simp_tac 1);

1894

80 
by (Fast_tac 1);

1344

81 
qed "prefix_Cons";
