1344

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


2 
ID: $Id$


3 
Author: Richard Mayr & Tobias Nipkow


4 
Copyright 1995 TUM


5 
*)


6 


7 
open Prefix;


8 


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


10 
br allI 1;


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


12 
br maj 1;


13 
br min 1;


14 
val list_cases = result();


15 


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


17 
by (simp_tac (!simpset addsimps [eq_sym_conv]) 1);


18 
qed "Nil_prefix";


19 
Addsimps[Nil_prefix];


20 


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


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


23 
by (Simp_tac 1);


24 
by (fast_tac HOL_cs 1);


25 
by (Simp_tac 1);


26 
qed "prefix_Nil";


27 
Addsimps [prefix_Nil];


28 


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


30 
goalw Prefix.thy [prefix_def]


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


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


33 
by (Simp_tac 1);


34 
by (fast_tac HOL_cs 1);


35 
by (Simp_tac 1);


36 
by (fast_tac HOL_cs 1);


37 
qed "prefix_Cons";


38 


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


40 
by(Simp_tac 1);


41 
by (fast_tac HOL_cs 1);


42 
qed"Cons_prefix_Cons";


43 
Addsimps [Cons_prefix_Cons];
