(* Title: HOL/Lex/Prefix.thy ID: $Id$ Author: Richard Mayr & Tobias Nipkow Copyright 1995 TUM *) open Prefix; val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l.Q(l)"; br allI 1; by (list.induct_tac "l" 1); br maj 1; br min 1; val list_cases = result(); goalw Prefix.thy [prefix_def] "[] <= xs"; by (simp_tac (!simpset addsimps [eq_sym_conv]) 1); qed "Nil_prefix"; Addsimps[Nil_prefix]; goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])"; by (list.induct_tac "xs" 1); by (Simp_tac 1); by (fast_tac HOL_cs 1); by (Simp_tac 1); qed "prefix_Nil"; Addsimps [prefix_Nil]; (* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *) goalw Prefix.thy [prefix_def] "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"; by (list.induct_tac "xs" 1); by (Simp_tac 1); by (fast_tac HOL_cs 1); by (Simp_tac 1); by (fast_tac HOL_cs 1); qed "prefix_Cons"; goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)"; by(Simp_tac 1); by (fast_tac HOL_cs 1); qed"Cons_prefix_Cons"; Addsimps [Cons_prefix_Cons];