# HG changeset patch # User nipkow # Date 894890440 -7200 # Node ID 697d17fe16654b77e7e2476ad232c5155f3d031b # Parent 2213a9ac0e4c63f23b6b6378df063f4952dc2d92 Reordered a few parameters. diff -r 2213a9ac0e4c -r 697d17fe1665 src/HOL/Lex/AutoMaxChop.ML --- a/src/HOL/Lex/AutoMaxChop.ML Mon May 11 13:18:25 1998 +0200 +++ b/src/HOL/Lex/AutoMaxChop.ML Mon May 11 14:40:40 1998 +0200 @@ -9,8 +9,8 @@ qed "delta_snoc"; goal thy - "!q ps res. auto_split A (delta A ps q) ps xs res = \ -\ maxsplit (%ys. fin A (delta A ys q)) ps xs res"; + "!q ps res. auto_split A (delta A ps q) res ps xs = \ +\ maxsplit (%ys. fin A (delta A ys q)) res ps xs"; by(induct_tac "xs" 1); by(Simp_tac 1); by(asm_simp_tac (simpset() addsimps [delta_snoc RS sym] @@ -18,14 +18,14 @@ qed_spec_mp "auto_split_lemma"; goalw thy [accepts_def] - "auto_split A (start A) [] xs res = maxsplit (accepts A) [] xs res"; + "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs"; by(stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1); by(stac auto_split_lemma 1); by(Simp_tac 1); qed_spec_mp "auto_split_is_maxsplit"; goal thy - "is_maxsplitter (accepts A) (%xs. auto_split A (start A) [] xs ([],xs))"; + "is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)"; by(simp_tac (simpset() addsimps [auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1); qed "is_maxsplitter_auto_split"; diff -r 2213a9ac0e4c -r 697d17fe1665 src/HOL/Lex/AutoMaxChop.thy --- a/src/HOL/Lex/AutoMaxChop.thy Mon May 11 13:18:25 1998 +0200 +++ b/src/HOL/Lex/AutoMaxChop.thy Mon May 11 14:40:40 1998 +0200 @@ -7,14 +7,13 @@ AutoMaxChop = DA + MaxChop + consts - auto_split :: "('a,'s)da => 's => 'a list => 'a list => 'a list * 'a list - => 'a list * 'a list" + auto_split :: "('a,'s)da => 's => 'a list * 'a list => 'a list => 'a splitter" primrec auto_split list -"auto_split A q ps [] res = (if fin A q then (ps,[]) else res)" -"auto_split A q ps (x#xs) res = auto_split A (next A x q) (ps@[x]) xs - (if fin A q then (ps,x#xs) else res)" +"auto_split A q res ps [] = (if fin A q then (ps,[]) else res)" +"auto_split A q res ps (x#xs) = + auto_split A (next A x q) (if fin A q then (ps,x#xs) else res) (ps@[x]) xs" constdefs auto_chop :: "('a,'s)da => 'a chopper" -"auto_chop A == chop (%xs. auto_split A (start A) [] xs ([],xs))" +"auto_chop A == chop (%xs. auto_split A (start A) ([],xs) [] xs)" end diff -r 2213a9ac0e4c -r 697d17fe1665 src/HOL/Lex/MaxChop.ML --- a/src/HOL/Lex/MaxChop.ML Mon May 11 13:18:25 1998 +0200 +++ b/src/HOL/Lex/MaxChop.ML Mon May 11 14:40:40 1998 +0200 @@ -6,7 +6,7 @@ (* Termination of chop *) -goalw thy [reducing_def] "reducing(%qs. maxsplit P [] qs ([],qs))"; +goalw thy [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)"; by(asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1); qed "reducing_maxsplit"; diff -r 2213a9ac0e4c -r 697d17fe1665 src/HOL/Lex/MaxPrefix.ML --- a/src/HOL/Lex/MaxPrefix.ML Mon May 11 13:18:25 1998 +0200 +++ b/src/HOL/Lex/MaxPrefix.ML Mon May 11 14:40:40 1998 +0200 @@ -6,8 +6,8 @@ Delsplits [split_if]; goalw thy [is_maxpref_def] "!(ps::'a list) res. \ -\ (maxsplit P ps qs res = (xs,ys)) = \ -\ (if (? us. us <= qs & P(ps@us)) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) \ +\ (maxsplit P res ps qs = (xs,ys)) = \ +\ (if ? us. us <= qs & P(ps@us) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) \ \ else (xs,ys)=res)"; by(induct_tac "qs" 1); by(simp_tac (simpset() addsplits [split_if]) 1); @@ -56,7 +56,7 @@ Addsimps [is_maxpref_Nil]; goalw thy [is_maxsplitter_def] - "is_maxsplitter P (%xs. maxsplit P [] xs ([],xs))"; + "is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)"; by(simp_tac (simpset() addsimps [maxsplit_lemma]) 1); by(fast_tac (claset() addss simpset()) 1); qed "is_maxsplitter_maxsplit"; diff -r 2213a9ac0e4c -r 697d17fe1665 src/HOL/Lex/MaxPrefix.thy --- a/src/HOL/Lex/MaxPrefix.thy Mon May 11 13:18:25 1998 +0200 +++ b/src/HOL/Lex/MaxPrefix.thy Mon May 11 14:40:40 1998 +0200 @@ -18,10 +18,9 @@ (!xs ps qs. f xs = (ps,qs) = (xs=ps@qs & is_maxpref P ps xs))" consts - maxsplit :: "('a list => bool) => 'a list => 'a list => 'a list * 'a list - => 'a list * 'a list" + maxsplit :: "('a list => bool) => 'a list * 'a list => 'a list => 'a splitter" primrec maxsplit list -"maxsplit P ps [] res = (if P ps then (ps,[]) else res)" -"maxsplit P ps (q#qs) res = maxsplit P (ps@[q]) qs - (if P ps then (ps,q#qs) else res)" +"maxsplit P res ps [] = (if P ps then (ps,[]) else res)" +"maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res) + (ps@[q]) qs" end