# HG changeset patch # User nipkow # Date 1346680241 -7200 # Node ID 8ab9fb2483a909075c88d829fafcc4838b1ca5fe # Parent 7b6beb7e99c1c3620e37b9cf495fd08aaeb9f5e7# Parent 7df19036392e97ee018db36f51c5c128e16a09bb merged diff -r 7df19036392e -r 8ab9fb2483a9 Admin/lib/Tools/build_doc --- a/Admin/lib/Tools/build_doc Mon Sep 03 15:41:06 2012 +0200 +++ b/Admin/lib/Tools/build_doc Mon Sep 03 15:50:41 2012 +0200 @@ -67,6 +67,7 @@ declare -a BUILD_OPTIONS=(-g doc) else declare -a BUILD_OPTIONS=() + [ "$#" -eq 0 ] && usage fi @@ -97,7 +98,12 @@ do cp -f "$FILE" "$ISABELLE_HOME/doc" done - cp -f "$OUTPUT"/*.dvi "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc" + if [ "$PDF_ONLY" = true ]; then + cp -f "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc" + rm -f "$ISABELLE_HOME/doc/document.pdf" "$ISABELLE_HOME/doc/outline.pdf" + else + cp -f "$OUTPUT"/*.dvi "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc" + fi fi rm -rf "$OUTPUT" diff -r 7df19036392e -r 8ab9fb2483a9 NEWS --- a/NEWS Mon Sep 03 15:41:06 2012 +0200 +++ b/NEWS Mon Sep 03 15:50:41 2012 +0200 @@ -101,8 +101,8 @@ picked up from some surrounding directory. Potential INCOMPATIBILITY for home-made configurations. -* The "isabelle logo" tool allows to specify EPS or PDF format; the -latter is preferred now. Minor INCOMPATIBILITY. +* The "isabelle logo" tool produces EPS and PDF format simultaneously. +Minor INCOMPATIBILITY in command-line options. * Advanced support for Isabelle sessions and build management, see "system" manual for the chapter of that name, especially the "isabelle diff -r 7df19036392e -r 8ab9fb2483a9 etc/isar-keywords.el --- a/etc/isar-keywords.el Mon Sep 03 15:41:06 2012 +0200 +++ b/etc/isar-keywords.el Mon Sep 03 15:50:41 2012 +0200 @@ -32,10 +32,7 @@ "axiomatization" "axioms" "back" - "bnf_codata" - "bnf_data" "bnf_def" - "bnf_sugar" "boogie_end" "boogie_open" "boogie_status" @@ -50,6 +47,7 @@ "class_deps" "classes" "classrel" + "codata_raw" "code_abort" "code_class" "code_const" @@ -71,6 +69,7 @@ "context" "corollary" "cpodef" + "data_raw" "datatype" "declaration" "declare" @@ -294,6 +293,7 @@ "values" "welcome" "with" + "wrap_data" "write" "{" "}")) @@ -469,14 +469,13 @@ "attribute_setup" "axiomatization" "axioms" - "bnf_codata" - "bnf_data" "boogie_end" "boogie_open" "bundle" "class" "classes" "classrel" + "codata_raw" "code_abort" "code_class" "code_const" @@ -492,6 +491,7 @@ "coinductive_set" "consts" "context" + "data_raw" "datatype" "declaration" "declare" @@ -577,7 +577,6 @@ (defconst isar-keywords-theory-goal '("ax_specification" "bnf_def" - "bnf_sugar" "boogie_vc" "code_pred" "corollary" @@ -605,7 +604,8 @@ "sublocale" "termination" "theorem" - "typedef")) + "typedef" + "wrap_data")) (defconst isar-keywords-qed '("\\." diff -r 7df19036392e -r 8ab9fb2483a9 lib/Tools/logo --- a/lib/Tools/logo Mon Sep 03 15:41:06 2012 +0200 +++ b/lib/Tools/logo Mon Sep 03 15:50:41 2012 +0200 @@ -10,12 +10,12 @@ function usage() { echo - echo "Usage: isabelle $PRG [OPTIONS] NAME" + echo "Usage: isabelle $PRG [OPTIONS] [XYZ]" echo - echo " Create instance NAME of the Isabelle logo (as EPS or PDF)." + echo " Create instance XYZ of the Isabelle logo (as EPS and PDF)." echo echo " Options are:" - echo " -o OUTPUT specify output file and format (default \"isabelle_name.pdf\")" + echo " -n NAME alternative output base name (default \"isabelle_xyx\")" echo " -q quiet mode" echo exit 1 @@ -32,14 +32,14 @@ # options -OUTPUT="" +OUTPUT_NAME="" QUIET="" -while getopts "o:q" OPT +while getopts "n:q" OPT do case "$OPT" in - o) - OUTPUT="$OPTARG" + n) + OUTPUT_NAME="$OPTARG" ;; q) QUIET=true @@ -55,38 +55,33 @@ # args -NAME="-" -[ "$#" -ge 1 ] && { NAME="$1"; shift; } +TEXT="" +[ "$#" -ge 1 ] && { TEXT="$1"; shift; } -[ "$#" -ne 0 -o "$NAME" = "-" ] && usage +[ "$#" -ne 0 ] && usage ## main -if [ -z "$OUTPUT" ]; then - OUTPUT=$(echo "$NAME" | tr A-Z a-z) - [ -n "$OUTPUT" ] && OUTPUT="_${OUTPUT}" - OUTPUT="isabelle${OUTPUT}.pdf" - OUTPUT_FORMAT="pdf" -else - case "$OUTPUT" in - *.eps) - OUTPUT_FORMAT="eps" - ;; - *.pdf) - OUTPUT_FORMAT="pdf" - ;; - *) - fail "Cannot guess output format (eps or pdf) from \"$OUTPUT\"" - ;; - esac -fi +case "$OUTPUT_NAME" in + "") + OUTPUT_NAME=$(echo "$TEXT" | tr A-Z a-z) + if [ -z "$OUTPUT_NAME" ]; then + OUTPUT_NAME="isabelle" + else + OUTPUT_NAME="isabelle_${OUTPUT_NAME}" + fi + ;; + */* | *.eps | *.pdf) + fail "Bad output base name: \"$OUTPUT_NAME\"" + ;; + *) + ;; +esac -[ -z "$QUIET" ] && echo "$OUTPUT" >&2 +[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2 +perl -p -e "s,,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps" -if [ "$OUTPUT_FORMAT" = "eps" ]; then - perl -p -e "s,,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTPUT" -else - perl -p -e "s,,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \ - "$ISABELLE_EPSTOPDF" -f > "$OUTPUT" -fi +[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2 +"$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps" + diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/Classes/document/build --- a/src/Doc/Classes/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/Classes/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle_isar.pdf Isar -"$ISABELLE_TOOL" logo -o isabelle_isar.eps Isar +"$ISABELLE_TOOL" logo Isar cp "$ISABELLE_HOME/src/Doc/iman.sty" . cp "$ISABELLE_HOME/src/Doc/extra.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/Codegen/document/build --- a/src/Doc/Codegen/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/Codegen/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle_isar.pdf "Isar" -"$ISABELLE_TOOL" logo -o isabelle_isar.eps "Isar" +"$ISABELLE_TOOL" logo Isar cp "$ISABELLE_HOME/src/Doc/iman.sty" . cp "$ISABELLE_HOME/src/Doc/extra.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/HOL/document/build --- a/src/Doc/HOL/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/HOL/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle_hol.pdf "HOL" -"$ISABELLE_TOOL" logo -o isabelle_hol.eps "HOL" +"$ISABELLE_TOOL" logo HOL cp "$ISABELLE_HOME/src/Doc/iman.sty" . cp "$ISABELLE_HOME/src/Doc/extra.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/Intro/document/build --- a/src/Doc/Intro/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/Intro/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle.pdf "" -"$ISABELLE_TOOL" logo -o isabelle.eps "" +"$ISABELLE_TOOL" logo cp "$ISABELLE_HOME/src/Doc/iman.sty" . cp "$ISABELLE_HOME/src/Doc/extra.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/IsarImplementation/document/build --- a/src/Doc/IsarImplementation/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/IsarImplementation/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle_isar.pdf Isar -"$ISABELLE_TOOL" logo -o isabelle_isar.eps Isar +"$ISABELLE_TOOL" logo Isar cp "$ISABELLE_HOME/src/Doc/iman.sty" . cp "$ISABELLE_HOME/src/Doc/extra.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/IsarRef/document/build --- a/src/Doc/IsarRef/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/IsarRef/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle_isar.pdf "Isar" -"$ISABELLE_TOOL" logo -o isabelle_isar.eps "Isar" +"$ISABELLE_TOOL" logo Isar cp "$ISABELLE_HOME/src/Doc/iman.sty" . cp "$ISABELLE_HOME/src/Doc/extra.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/Logics/document/build --- a/src/Doc/Logics/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/Logics/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle.pdf "" -"$ISABELLE_TOOL" logo -o isabelle.eps "" +"$ISABELLE_TOOL" logo cp "$ISABELLE_HOME/src/Doc/iman.sty" . cp "$ISABELLE_HOME/src/Doc/extra.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/Nitpick/document/build --- a/src/Doc/Nitpick/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/Nitpick/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle_nitpick.pdf "Nitpick" -"$ISABELLE_TOOL" logo -o isabelle_nitpick.eps "Nitpick" +"$ISABELLE_TOOL" logo Nitpick cp "$ISABELLE_HOME/src/Doc/iman.sty" . cp "$ISABELLE_HOME/src/Doc/manual.bib" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/ProgProve/document/build --- a/src/Doc/ProgProve/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/ProgProve/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle_hol.pdf "HOL" -"$ISABELLE_TOOL" logo -o isabelle_hol.eps "HOL" +"$ISABELLE_TOOL" logo HOL cp "$ISABELLE_HOME/src/Doc/ProgProve/MyList.thy" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/Ref/document/build --- a/src/Doc/Ref/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/Ref/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle.pdf "" -"$ISABELLE_TOOL" logo -o isabelle.eps "" +"$ISABELLE_TOOL" logo cp "$ISABELLE_HOME/src/Doc/iman.sty" . cp "$ISABELLE_HOME/src/Doc/extra.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/Sledgehammer/document/build --- a/src/Doc/Sledgehammer/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/Sledgehammer/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle_sledgehammer.pdf "S/H" -"$ISABELLE_TOOL" logo -o isabelle_sledgehammer.eps "S/H" +"$ISABELLE_TOOL" logo -n isabelle_sledgehammer "S/H" cp "$ISABELLE_HOME/src/Doc/iman.sty" . cp "$ISABELLE_HOME/src/Doc/manual.bib" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/System/Misc.thy Mon Sep 03 15:50:41 2012 +0200 @@ -209,23 +209,21 @@ section {* Creating instances of the Isabelle logo *} -text {* The @{tool_def logo} tool creates any instance of the generic - Isabelle logo as EPS or PDF. +text {* The @{tool_def logo} tool creates instances of the generic + Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents. \begin{ttbox} -Usage: isabelle logo [OPTIONS] NAME +Usage: isabelle logo [OPTIONS] XYZ - Create instance NAME of the Isabelle logo (as EPS or PDF). + Create instance XYZ of the Isabelle logo (as EPS and PDF). Options are: - -o OUTFILE specify output file and format - (default "isabelle_name.pdf") + -n NAME alternative output base name (default "isabelle_xyx") -q quiet mode \end{ttbox} - Option @{verbatim "-o"} specifies an explicit output file name and - format, e.g.\ @{verbatim "mylogo.eps"} for an EPS logo. The default - is @{verbatim "isabelle_"}@{text name}@{verbatim ".pdf"}, with the - lower-case version of the given name and PDF output. + Option @{verbatim "-n"} specifies an altenative (base) name for the + generated files. The default is @{verbatim "isabelle_"}@{text xyz} + in lower-case. Option @{verbatim "-q"} omits printing of the result file name. diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/System/document/build --- a/src/Doc/System/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/System/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle.pdf "" -"$ISABELLE_TOOL" logo -o isabelle.eps "" +"$ISABELLE_TOOL" logo cp "$ISABELLE_HOME/src/Doc/IsarRef/document/style.sty" . cp "$ISABELLE_HOME/src/Doc/iman.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/Tutorial/document/build --- a/src/Doc/Tutorial/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/Tutorial/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle_hol.pdf "HOL" -"$ISABELLE_TOOL" logo -o isabelle_hol.eps "HOL" +"$ISABELLE_TOOL" logo HOL cp "$ISABELLE_HOME/src/Doc/proof.sty" . cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/Doc/ZF/document/build --- a/src/Doc/ZF/document/build Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Doc/ZF/document/build Mon Sep 03 15:50:41 2012 +0200 @@ -5,8 +5,7 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" logo -o isabelle_zf.pdf "ZF" -"$ISABELLE_TOOL" logo -o isabelle_zf.eps "ZF" +"$ISABELLE_TOOL" logo ZF cp "$ISABELLE_HOME/src/Doc/isar.sty" . cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/BNF_GFP.thy --- a/src/HOL/Codatatype/BNF_GFP.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/BNF_GFP.thy Mon Sep 03 15:50:41 2012 +0200 @@ -10,7 +10,7 @@ theory BNF_GFP imports BNF_Comp keywords - "bnf_codata" :: thy_decl + "codata_raw" :: thy_decl uses "Tools/bnf_gfp_util.ML" "Tools/bnf_gfp_tactics.ML" diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/BNF_LFP.thy --- a/src/HOL/Codatatype/BNF_LFP.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/BNF_LFP.thy Mon Sep 03 15:50:41 2012 +0200 @@ -10,7 +10,7 @@ theory BNF_LFP imports BNF_Comp keywords - "bnf_data" :: thy_decl + "data_raw" :: thy_decl uses "Tools/bnf_lfp_util.ML" "Tools/bnf_lfp_tactics.ML" diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/BNF_Library.thy --- a/src/HOL/Codatatype/BNF_Library.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Library.thy Mon Sep 03 15:50:41 2012 +0200 @@ -8,7 +8,9 @@ header {* Library for Bounded Natural Functors *} theory BNF_Library -imports "../Ordinals_and_Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/List_Prefix" +imports + "../Ordinals_and_Cardinals/Cardinal_Arithmetic" + "~~/src/HOL/Library/Prefix_Order" Equiv_Relations_More begin @@ -634,7 +636,7 @@ shows "PROP P x y" by (rule `(\x y. PROP P x y)`) -(*Extended List_Prefix*) +(*Extended Sublist*) definition prefCl where "prefCl Kl = (\ kl1 kl2. kl1 \ kl2 \ kl2 \ Kl \ kl1 \ Kl)" diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/BNF_Wrap.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codatatype/BNF_Wrap.thy Mon Sep 03 15:50:41 2012 +0200 @@ -0,0 +1,19 @@ +(* Title: HOL/Codatatype/BNF_Wrap.thy + Author: Dmitriy Traytel, TU Muenchen + Copyright 2012 + +Wrapping datatypes. +*) + +header {* Wrapping Datatypes *} + +theory BNF_Wrap +imports BNF_Def +keywords + "wrap_data" :: thy_goal +uses + "Tools/bnf_wrap_tactics.ML" + "Tools/bnf_wrap.ML" +begin + +end diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Codatatype.thy --- a/src/HOL/Codatatype/Codatatype.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Codatatype.thy Mon Sep 03 15:50:41 2012 +0200 @@ -10,12 +10,7 @@ header {* The (Co)datatype Package *} theory Codatatype -imports BNF_LFP BNF_GFP -keywords - "bnf_sugar" :: thy_goal -uses - "Tools/bnf_sugar_tactics.ML" - "Tools/bnf_sugar.ML" +imports BNF_Wrap BNF_LFP BNF_GFP begin end diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Examples/HFset.thy --- a/src/HOL/Codatatype/Examples/HFset.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Examples/HFset.thy Mon Sep 03 15:50:41 2012 +0200 @@ -14,7 +14,7 @@ section {* Datatype definition *} -bnf_data hfset: 'hfset = "'hfset fset" +data_raw hfset: 'hfset = "'hfset fset" section {* Customization of terms *} diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Mon Sep 03 15:50:41 2012 +0200 @@ -15,7 +15,7 @@ typedecl N typedecl T -bnf_codata Tree: 'Tree = "N \ (T + 'Tree) fset" +codata_raw Tree: 'Tree = "N \ (T + 'Tree) fset" section {* Sugar notations for Tree *} diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Examples/Lambda_Term.thy --- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Mon Sep 03 15:50:41 2012 +0200 @@ -15,7 +15,7 @@ section {* Datatype definition *} -bnf_data trm: 'trm = "'a + 'trm \ 'trm + 'a \ 'trm + ('a \ 'trm) fset \ 'trm" +data_raw trm: 'trm = "'a + 'trm \ 'trm + 'a \ 'trm + ('a \ 'trm) fset \ 'trm" section {* Customization of terms *} diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Examples/ListF.thy --- a/src/HOL/Codatatype/Examples/ListF.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Examples/ListF.thy Mon Sep 03 15:50:41 2012 +0200 @@ -12,7 +12,7 @@ imports "../Codatatype" begin -bnf_data listF: 'list = "unit + 'a \ 'list" +data_raw listF: 'list = "unit + 'a \ 'list" definition "NilF = listF_fld (Inl ())" definition "Conss a as \ listF_fld (Inr (a, as))" diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Examples/Misc_Codata.thy --- a/src/HOL/Codatatype/Examples/Misc_Codata.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy Mon Sep 03 15:50:41 2012 +0200 @@ -16,33 +16,33 @@ ML {* PolyML.fullGC (); *} -bnf_codata simple: 'a = "unit + unit + unit + unit" +codata_raw simple: 'a = "unit + unit + unit + unit" -bnf_codata stream: 's = "'a \ 's" +codata_raw stream: 's = "'a \ 's" -bnf_codata llist: 'llist = "unit + 'a \ 'llist" +codata_raw llist: 'llist = "unit + 'a \ 'llist" -bnf_codata some_passive: 'a = "'a + 'b + 'c + 'd + 'e" +codata_raw some_passive: 'a = "'a + 'b + 'c + 'd + 'e" (* ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 *) -bnf_codata F1: 'b1 = "'a \ 'b1 + 'a \ 'b2" +codata_raw F1: 'b1 = "'a \ 'b1 + 'a \ 'b2" and F2: 'b2 = "unit + 'b1 * 'b2" -bnf_codata EXPR: 'E = "'T + 'T \ 'E" +codata_raw EXPR: 'E = "'T + 'T \ 'E" and TERM: 'T = "'F + 'F \ 'T" and FACTOR: 'F = "'a + 'b + 'E" -bnf_codata llambda: +codata_raw llambda: 'trm = "string + 'trm \ 'trm + string \ 'trm + (string \ 'trm) fset \ 'trm" -bnf_codata par_llambda: +codata_raw par_llambda: 'trm = "'a + 'trm \ 'trm + 'a \ 'trm + @@ -53,29 +53,29 @@ 'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c) *) -bnf_codata tree: 'tree = "unit + 'a \ 'forest" +codata_raw tree: 'tree = "unit + 'a \ 'forest" and forest: 'forest = "unit + 'tree \ 'forest" -bnf_codata CPS: 'a = "'b + 'b \ 'a" +codata_raw CPS: 'a = "'b + 'b \ 'a" -bnf_codata fun_rhs: 'a = "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'a" +codata_raw fun_rhs: 'a = "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'a" -bnf_codata fun_rhs': 'a = "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'b10 \ +codata_raw fun_rhs': 'a = "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'b10 \ 'b11 \ 'b12 \ 'b13 \ 'b14 \ 'b15 \ 'b16 \ 'b17 \ 'b18 \ 'b19 \ 'b20 \ 'a" -bnf_codata some_killing: 'a = "'b \ 'd \ ('a + 'c)" +codata_raw some_killing: 'a = "'b \ 'd \ ('a + 'c)" and in_here: 'c = "'d \ 'b + 'e" -bnf_codata some_killing': 'a = "'b \ 'd \ ('a + 'c)" +codata_raw some_killing': 'a = "'b \ 'd \ ('a + 'c)" and in_here': 'c = "'d + 'e" -bnf_codata some_killing'': 'a = "'b \ 'c" +codata_raw some_killing'': 'a = "'b \ 'c" and in_here'': 'c = "'d \ 'b + 'e" -bnf_codata less_killing: 'a = "'b \ 'c" +codata_raw less_killing: 'a = "'b \ 'c" (* SLOW, MEMORY-HUNGRY -bnf_codata K1': 'K1 = "'K2 + 'a list" +codata_raw K1': 'K1 = "'K2 + 'a list" and K2': 'K2 = "'K3 + 'c fset" and K3': 'K3 = "'K3 + 'K4 + 'K4 \ 'K5" and K4': 'K4 = "'K5 + 'a list list list" diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Examples/Misc_Data.thy --- a/src/HOL/Codatatype/Examples/Misc_Data.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Mon Sep 03 15:50:41 2012 +0200 @@ -16,19 +16,19 @@ ML {* PolyML.fullGC (); *} -bnf_data simple: 'a = "unit + unit + unit + unit" +data_raw simple: 'a = "unit + unit + unit + unit" -bnf_data mylist: 'list = "unit + 'a \ 'list" +data_raw mylist: 'list = "unit + 'a \ 'list" -bnf_data some_passive: 'a = "'a + 'b + 'c + 'd + 'e" +data_raw some_passive: 'a = "'a + 'b + 'c + 'd + 'e" -bnf_data lambda: +data_raw lambda: 'trm = "string + 'trm \ 'trm + string \ 'trm + (string \ 'trm) fset \ 'trm" -bnf_data par_lambda: +data_raw par_lambda: 'trm = "'a + 'trm \ 'trm + 'a \ 'trm + @@ -39,7 +39,7 @@ ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 *) -bnf_data F1: 'b1 = "'a \ 'b1 + 'a \ 'b2" +data_raw F1: 'b1 = "'a \ 'b1 + 'a \ 'b2" and F2: 'b2 = "unit + 'b1 * 'b2" (* @@ -47,7 +47,7 @@ 'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c) *) -bnf_data tree: 'tree = "unit + 'a \ 'forest" +data_raw tree: 'tree = "unit + 'a \ 'forest" and forest: 'forest = "unit + 'tree \ 'forest" (* @@ -55,7 +55,7 @@ ' a branch = Branch of 'a * 'a tree ('c = 'a * 'b) *) -bnf_data tree': 'tree = "unit + 'branch \ 'branch" +data_raw tree': 'tree = "unit + 'branch \ 'branch" and branch: 'branch = "'a \ 'tree" (* @@ -64,54 +64,54 @@ factor = C 'a | V 'b | Paren exp ('e = 'a + 'b + 'c) *) -bnf_data EXPR: 'E = "'T + 'T \ 'E" +data_raw EXPR: 'E = "'T + 'T \ 'E" and TERM: 'T = "'F + 'F \ 'T" and FACTOR: 'F = "'a + 'b + 'E" -bnf_data some_killing: 'a = "'b \ 'd \ ('a + 'c)" +data_raw some_killing: 'a = "'b \ 'd \ ('a + 'c)" and in_here: 'c = "'d \ 'b + 'e" -bnf_data nofail1: 'a = "'a \ 'b + 'b" -bnf_data nofail2: 'a = "('a \ 'b \ 'a \ 'b) list" -bnf_data nofail3: 'a = "'b \ ('a \ 'b \ 'a \ 'b) fset" -bnf_data nofail4: 'a = "('a \ ('a \ 'b \ 'a \ 'b) fset) list" +data_raw nofail1: 'a = "'a \ 'b + 'b" +data_raw nofail2: 'a = "('a \ 'b \ 'a \ 'b) list" +data_raw nofail3: 'a = "'b \ ('a \ 'b \ 'a \ 'b) fset" +data_raw nofail4: 'a = "('a \ ('a \ 'b \ 'a \ 'b) fset) list" (* -bnf_data fail: 'a = "'a \ 'b \ 'a \ 'b list" -bnf_data fail: 'a = "'a \ 'b \ 'a \ 'b" -bnf_data fail: 'a = "'a \ 'b + 'a" -bnf_data fail: 'a = "'a \ 'b" +data_raw fail: 'a = "'a \ 'b \ 'a \ 'b list" +data_raw fail: 'a = "'a \ 'b \ 'a \ 'b" +data_raw fail: 'a = "'a \ 'b + 'a" +data_raw fail: 'a = "'a \ 'b" *) -bnf_data L1: 'L1 = "'L2 list" +data_raw L1: 'L1 = "'L2 list" and L2: 'L2 = "'L1 fset + 'L2" -bnf_data K1: 'K1 = "'K2" +data_raw K1: 'K1 = "'K2" and K2: 'K2 = "'K3" and K3: 'K3 = "'K1 list" -bnf_data t1: 't1 = "'t3 + 't2" +data_raw t1: 't1 = "'t3 + 't2" and t2: 't2 = "'t1" and t3: 't3 = "unit" -bnf_data t1': 't1 = "'t2 + 't3" +data_raw t1': 't1 = "'t2 + 't3" and t2': 't2 = "'t1" and t3': 't3 = "unit" (* -bnf_data fail1: 'L1 = "'L2" +data_raw fail1: 'L1 = "'L2" and fail2: 'L2 = "'L3" and fail2: 'L3 = "'L1" -bnf_data fail1: 'L1 = "'L2 list \ 'L2" +data_raw fail1: 'L1 = "'L2 list \ 'L2" and fail2: 'L2 = "'L2 fset \ 'L3" and fail2: 'L3 = "'L1" -bnf_data fail1: 'L1 = "'L2 list \ 'L2" +data_raw fail1: 'L1 = "'L2 list \ 'L2" and fail2: 'L2 = "'L1 fset \ 'L1" *) (* SLOW -bnf_data K1': 'K1 = "'K2 + 'a list" +data_raw K1': 'K1 = "'K2 + 'a list" and K2': 'K2 = "'K3 + 'c fset" and K3': 'K3 = "'K3 + 'K4 + 'K4 \ 'K5" and K4': 'K4 = "'K5 + 'a list list list" @@ -132,23 +132,23 @@ *) (* fail: -bnf_data t1: 't1 = "'t2 * 't3 + 't2 * 't4" +data_raw t1: 't1 = "'t2 * 't3 + 't2 * 't4" and t2: 't2 = "unit" and t3: 't3 = 't4 and t4: 't4 = 't1 *) -bnf_data k1: 'k1 = "'k2 * 'k3 + 'k2 * 'k4" +data_raw k1: 'k1 = "'k2 * 'k3 + 'k2 * 'k4" and k2: 'k2 = unit and k3: 'k3 = 'k4 and k4: 'k4 = unit -bnf_data tt1: 'tt1 = "'tt3 * 'tt2 + 'tt2 * 'tt4" +data_raw tt1: 'tt1 = "'tt3 * 'tt2 + 'tt2 * 'tt4" and tt2: 'tt2 = unit and tt3: 'tt3 = 'tt1 and tt4: 'tt4 = unit (* SLOW -bnf_data s1: 's1 = "'s2 * 's3 * 's4 + 's3 + 's2 * 's6 + 's4 * 's2 + 's2 * 's2" +data_raw s1: 's1 = "'s2 * 's3 * 's4 + 's3 + 's2 * 's6 + 's4 * 's2 + 's2 * 's2" and s2: 's2 = "'s7 * 's5 + 's5 * 's4 * 's6" and s3: 's3 = "'s1 * 's7 * 's2 + 's3 * 's3 + 's4 * 's5" and s4: 's4 = 's5 diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Examples/Process.thy --- a/src/HOL/Codatatype/Examples/Process.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Process.thy Mon Sep 03 15:50:41 2012 +0200 @@ -11,7 +11,7 @@ imports "../Codatatype" begin -bnf_codata process: 'p = "'a * 'p + 'p * 'p" +codata_raw process: 'p = "'a * 'p + 'p * 'p" (* codatatype 'a process = Action (prefOf :: 'a) (contOf :: 'a process) | Choice (ch1Of :: 'a process) (ch2Of :: 'a process) diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Examples/Stream.thy --- a/src/HOL/Codatatype/Examples/Stream.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Stream.thy Mon Sep 03 15:50:41 2012 +0200 @@ -12,7 +12,7 @@ imports TreeFI begin -bnf_codata stream: 's = "'a \ 's" +codata_raw stream: 's = "'a \ 's" (* selectors for streams *) definition "hdd as \ fst (stream_unf as)" diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Examples/TreeFI.thy --- a/src/HOL/Codatatype/Examples/TreeFI.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFI.thy Mon Sep 03 15:50:41 2012 +0200 @@ -12,7 +12,9 @@ imports ListF begin -bnf_codata treeFI: 'tree = "'a \ 'tree listF" +hide_const (open) Sublist.sub + +codata_raw treeFI: 'tree = "'a \ 'tree listF" lemma treeFIBNF_listF_set[simp]: "treeFIBNF_set2 (i, xs) = listF_set xs" unfolding treeFIBNF_set2_def collect_def[abs_def] prod_set_defs diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Examples/TreeFsetI.thy --- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Mon Sep 03 15:50:41 2012 +0200 @@ -12,10 +12,12 @@ imports "../Codatatype" begin +hide_const (open) Sublist.sub + definition pair_fun (infixr "\" 50) where "f \ g \ \x. (f x, g x)" -bnf_codata treeFsetI: 't = "'a \ 't fset" +codata_raw treeFsetI: 't = "'a \ 't fset" (* selectors for trees *) definition "lab t \ fst (treeFsetI_unf t)" diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Mon Sep 03 15:50:41 2012 +0200 @@ -75,21 +75,12 @@ val split_conj_thm: thm -> thm list val split_conj_prems: int -> thm -> thm - val list_all_free: term list -> term -> term - val list_exists_free: term list -> term -> term - val mk_Field: term -> term val mk_union: term * term -> term - val mk_disjIN: int -> int -> thm - val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list - val interleave: 'a list -> 'a list -> 'a list - - val certifyT: Proof.context -> typ -> ctyp - val certify: Proof.context -> term -> cterm val fp_bnf: (binding list -> typ list list -> BNF_Def.BNF list -> Proof.context -> Proof.context) -> @@ -190,28 +181,9 @@ val mk_union = HOLogic.mk_binop @{const_name sup}; -fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]} - | mk_disjIN _ 1 = disjI1 - | mk_disjIN 2 2 = disjI2 - | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2; - (*dangerous; use with monotonic, converging functions only!*) fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X); -val list_exists_free = - fold_rev (fn free => fn P => - let val (x, T) = Term.dest_Free free; - in HOLogic.exists_const T $ Term.absfree (x, T) P end); - -val list_all_free = - fold_rev (fn free => fn P => - let val (x, T) = Term.dest_Free free; - in HOLogic.all_const T $ Term.absfree (x, T) P end); - -(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*) -fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); -fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); - (* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *) fun split_conj_thm th = ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th]; @@ -225,8 +197,6 @@ fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull = [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull]; -fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys); - fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree) (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss; diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Mon Sep 03 15:50:41 2012 +0200 @@ -2776,7 +2776,7 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "bnf_codata"} "greatest fixed points for BNF equations" + Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points for BNF equations" (Parse.and_list1 ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >> (fp_bnf_cmd bnf_gfp o apsnd split_list o split_list)); diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Mon Sep 03 15:50:41 2012 +0200 @@ -1755,7 +1755,7 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "bnf_data"} "least fixed points for BNF equations" + Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points for BNF equations" (Parse.and_list1 ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >> (fp_bnf_cmd bnf_lfp o apsnd split_list o split_list)); diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Tools/bnf_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_sugar.ML Mon Sep 03 15:41:06 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,420 +0,0 @@ -(* Title: HOL/Codatatype/Tools/bnf_sugar.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 - -Sugar on top of a BNF. -*) - -signature BNF_SUGAR = -sig -end; - -structure BNF_Sugar : BNF_SUGAR = -struct - -open BNF_Util -open BNF_FP_Util -open BNF_Sugar_Tactics - -val is_N = "is_"; -val un_N = "un_"; -fun mk_un_N 1 1 suf = un_N ^ suf - | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l; - -val case_congN = "case_cong"; -val case_discsN = "case_discs"; -val casesN = "cases"; -val ctr_selsN = "ctr_sels"; -val disc_exclusN = "disc_exclus"; -val disc_exhaustN = "disc_exhaust"; -val discsN = "discs"; -val distinctN = "distinct"; -val selsN = "sels"; -val splitN = "split"; -val split_asmN = "split_asm"; -val weak_case_cong_thmsN = "weak_case_cong"; - -val default_name = @{binding _}; - -fun pad_list x n xs = xs @ replicate (n - length xs) x; - -fun mk_half_pairss' _ [] = [] - | mk_half_pairss' indent (y :: ys) = - indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys); - -fun mk_half_pairss ys = mk_half_pairss' [[]] ys; - -val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; - -fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T); - -fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs; - -fun name_of_ctr t = - case head_of t of - Const (s, _) => s - | Free (s, _) => s - | _ => error "Cannot extract name of constructor"; - -fun prepare_sugar prep_term ((raw_ctrs, raw_caseof), (raw_disc_names, raw_sel_namess)) - no_defs_lthy = - let - (* TODO: sanity checks on arguments *) - - (* TODO: normalize types of constructors w.r.t. each other *) - - val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; - val caseof0 = prep_term no_defs_lthy raw_caseof; - - val n = length ctrs0; - val ks = 1 upto n; - - val (T_name, As0) = dest_Type (body_type (fastype_of (hd ctrs0))); - val b = Binding.qualified_name T_name; - - val (As, B) = - no_defs_lthy - |> mk_TFrees (length As0) - ||> the_single o fst o mk_TFrees 1; - - fun mk_ctr Ts ctr = - let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in - Term.subst_atomic_types (Ts0 ~~ Ts) ctr - end; - - val T = Type (T_name, As); - val ctrs = map (mk_ctr As) ctrs0; - val ctr_Tss = map (binder_types o fastype_of) ctrs; - - val ms = map length ctr_Tss; - - val disc_names = - pad_list default_name n raw_disc_names - |> map2 (fn ctr => fn disc => - if Binding.eq_name (disc, default_name) then - Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr))) - else - disc) ctrs0; - - val sel_namess = - pad_list [] n raw_sel_namess - |> map3 (fn ctr => fn m => map2 (fn l => fn sel => - if Binding.eq_name (sel, default_name) then - Binding.name (mk_un_N m l (Long_Name.base_name (name_of_ctr ctr))) - else - sel) (1 upto m) o pad_list default_name m) ctrs0 ms; - - fun mk_caseof Ts T = - let val (binders, body) = strip_type (fastype_of caseof0) in - Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ Ts)) caseof0 - end; - - val caseofB = mk_caseof As B; - val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss; - - fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs); - - val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |> - mk_Freess "x" ctr_Tss - ||>> mk_Freess "y" ctr_Tss - ||>> mk_Frees "f" caseofB_Ts - ||>> mk_Frees "g" caseofB_Ts - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T - ||>> yield_singleton (mk_Frees "w") T - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; - - val q = Free (fst p', B --> HOLogic.boolT); - - val xctrs = map2 (curry Term.list_comb) ctrs xss; - val yctrs = map2 (curry Term.list_comb) ctrs yss; - - val xfs = map2 (curry Term.list_comb) fs xss; - val xgs = map2 (curry Term.list_comb) gs xss; - - val eta_fs = map2 eta_expand_caseof_arg xss xfs; - val eta_gs = map2 eta_expand_caseof_arg xss xgs; - - val caseofB_fs = Term.list_comb (caseofB, eta_fs); - - val exist_xs_v_eq_ctrs = - map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss; - - fun mk_sel_caseof_args k xs x T = - map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks; - - fun disc_spec b exist_xs_v_eq_ctr = - mk_Trueprop_eq (Free (Binding.name_of b, T --> HOLogic.boolT) $ v, exist_xs_v_eq_ctr); - - fun sel_spec b x xs k = - let val T' = fastype_of x in - mk_Trueprop_eq (Free (Binding.name_of b, T --> T') $ v, - Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v) - end; - - val (((raw_discs, (_, raw_disc_defs)), (raw_selss, (_, raw_sel_defss))), (lthy', lthy)) = - no_defs_lthy - |> apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn exist_xs_v_eq_ctr => - Specification.definition (SOME (b, NONE, NoSyn), - ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr))) disc_names exist_xs_v_eq_ctrs - ||>> apfst (apsnd split_list o split_list) o fold_map3 (fn bs => fn xs => fn k => - apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn x => - Specification.definition (SOME (b, NONE, NoSyn), - ((Thm.def_binding b, []), sel_spec b x xs k))) bs xs) sel_namess xss ks - ||> `Local_Theory.restore; - - (*transforms defined frees into consts (and more)*) - val phi = Proof_Context.export_morphism lthy lthy'; - - val disc_defs = map (Morphism.thm phi) raw_disc_defs; - val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss; - - val discs0 = map (Morphism.term phi) raw_discs; - val selss0 = map (map (Morphism.term phi)) raw_selss; - - fun mk_disc_or_sel Ts t = - Term.subst_atomic_types (snd (dest_Type (domain_type (fastype_of t))) ~~ Ts) t; - - val discs = map (mk_disc_or_sel As) discs0; - val selss = map (map (mk_disc_or_sel As)) selss0; - - fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); - - val goal_exhaust = - let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in - mk_imp_p (map2 mk_prem xctrs xss) - end; - - val goal_injectss = - let - fun mk_goal _ _ [] [] = [] - | mk_goal xctr yctr xs ys = - [mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), - Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))]; - in - map4 mk_goal xctrs yctrs xss yss - end; - - val goal_half_distinctss = - map (map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq)) (mk_half_pairss xctrs); - - val goal_cases = map2 (fn xctr => fn xf => mk_Trueprop_eq (caseofB_fs $ xctr, xf)) xctrs xfs; - - val goals = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases]; - - fun after_qed thmss lthy = - let - val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) = - (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); - - val exhaust_thm' = - let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in - Drule.instantiate' [] [SOME (certify lthy v)] - (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm)) - end; - - val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss; - - val (distinct_thmsss', distinct_thmsss) = - map2 (map2 append) (Library.chop_groups n half_distinct_thmss) - (transpose (Library.chop_groups n other_half_distinct_thmss)) - |> `transpose; - val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss); - - val nchotomy_thm = - let - val goal = - HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v', - Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs)); - in - Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) - end; - - val sel_thmss = - let - fun mk_thm k xs goal_case case_thm x sel_def = - let - val T = fastype_of x; - val cTs = - map ((fn T' => certifyT lthy (if T' = B then T else T')) o TFree) - (rev (Term.add_tfrees goal_case [])); - val cxs = map (certify lthy) (mk_sel_caseof_args k xs x T); - in - Local_Defs.fold lthy [sel_def] - (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm) - end; - fun mk_thms k xs goal_case case_thm sel_defs = - map2 (mk_thm k xs goal_case case_thm) xs sel_defs; - in - map5 mk_thms ks xss goal_cases case_thms sel_defss - end; - - val discD_thms = map (fn def => def RS iffD1) disc_defs; - val discI_thms = - map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs; - val not_disc_thms = - map2 (fn m => fn def => funpow m (fn thm => allI RS thm) - (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) - ms disc_defs; - - val (disc_thmss', disc_thmss) = - let - fun mk_thm discI _ [] = refl RS discI - | mk_thm _ not_disc [distinct] = distinct RS not_disc; - fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss; - in - map3 mk_thms discI_thms not_disc_thms distinct_thmsss' - |> `transpose - end; - - val disc_exclus_thms = - let - fun mk_goal ((_, disc), (_, disc')) = - Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), - HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)))); - fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); - - val bundles = ms ~~ discD_thms ~~ discs; - val half_pairss = mk_half_pairss bundles; - - val goal_halvess = map (map mk_goal) half_pairss; - val half_thmss = - map3 (fn [] => K (K []) - | [(((m, discD), _), _)] => fn disc_thm => fn [goal] => - [prove (mk_half_disc_exclus_tac m discD disc_thm) goal]) - half_pairss (flat disc_thmss') goal_halvess; - - val goal_other_halvess = map (map (mk_goal o swap)) half_pairss; - val other_half_thmss = - map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess; - in - interleave (flat half_thmss) (flat other_half_thmss) - end; - - val disc_exhaust_thm = - let - fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)]; - val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); - in - Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms) - end; - - val ctr_sel_thms = - let - fun mk_goal ctr disc sels = - Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), - mk_Trueprop_eq ((null sels ? swap) - (Term.list_comb (ctr, map (fn sel => sel $ v) sels), v)))); - val goals = map3 mk_goal ctrs discs selss; - in - map4 (fn goal => fn m => fn discD => fn sel_thms => - Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_ctr_sel_tac ctxt m discD sel_thms)) - goals ms discD_thms sel_thmss - end; - - val case_disc_thm = - let - fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); - fun mk_rhs _ [f] [sels] = mk_core f sels - | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) = - Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $ - (disc $ v) $ mk_core f sels $ mk_rhs discs fs selss; - val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss); - in - Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss) - |> singleton (Proof_Context.export names_lthy lthy) - end; - - val (case_cong_thm, weak_case_cong_thm) = - let - fun mk_prem xctr xs f g = - fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr), - mk_Trueprop_eq (f, g))); - - val v_eq_w = mk_Trueprop_eq (v, w); - val caseof_fs = mk_caseofB_term eta_fs; - val caseof_gs = mk_caseofB_term eta_gs; - - val goal = - Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs, - mk_Trueprop_eq (caseof_fs $ v, caseof_gs $ w)); - val goal_weak = - Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w)); - in - (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms), - Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) - |> pairself (singleton (Proof_Context.export names_lthy lthy)) - end; - - val (split_thm, split_asm_thm) = - let - fun mk_conjunct xctr xs f_xs = - list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs)); - fun mk_disjunct xctr xs f_xs = - list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr), - HOLogic.mk_not (q $ f_xs))); - - val lhs = q $ (mk_caseofB_term eta_fs $ v); - - val goal = - mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); - val goal_asm = - mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj - (map3 mk_disjunct xctrs xss xfs))); - - val split_thm = - Skip_Proof.prove lthy [] [] goal - (fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss) - |> singleton (Proof_Context.export names_lthy lthy) - val split_asm_thm = - Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} => - mk_split_asm_tac ctxt split_thm) - |> singleton (Proof_Context.export names_lthy lthy) - in - (split_thm, split_asm_thm) - end; - - (* TODO: case syntax *) - (* TODO: attributes (simp, case_names, etc.) *) - - val notes = - [(case_congN, [case_cong_thm]), - (case_discsN, [case_disc_thm]), - (casesN, case_thms), - (ctr_selsN, ctr_sel_thms), - (discsN, (flat disc_thmss)), - (disc_exclusN, disc_exclus_thms), - (disc_exhaustN, [disc_exhaust_thm]), - (distinctN, distinct_thms), - (exhaustN, [exhaust_thm]), - (injectN, (flat inject_thmss)), - (nchotomyN, [nchotomy_thm]), - (selsN, (flat sel_thmss)), - (splitN, [split_thm]), - (split_asmN, [split_asm_thm]), - (weak_case_cong_thmsN, [weak_case_cong_thm])] - |> map (fn (thmN, thms) => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); - in - lthy |> Local_Theory.notes notes |> snd - end; - in - (goals, after_qed, lthy') - end; - -val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; - -val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]"; - -val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) => - Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo - prepare_sugar Syntax.read_term; - -val _ = - Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF" - (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term -- - Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], [])) - >> bnf_sugar_cmd); - -end; diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Mon Sep 03 15:41:06 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,93 +0,0 @@ -(* Title: HOL/Codatatype/Tools/bnf_sugar_tactics.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 - -Tactics for sugar on top of a BNF. -*) - -signature BNF_SUGAR_TACTICS = -sig - val mk_case_cong_tac: thm -> thm list -> tactic - val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic - val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic - val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic - val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic - val mk_nchotomy_tac: int -> thm -> tactic - val mk_other_half_disc_exclus_tac: thm -> tactic - val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic - val mk_split_asm_tac: Proof.context -> thm -> tactic -end; - -structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS = -struct - -open BNF_Util -open BNF_Tactics -open BNF_FP_Util - -fun triangle _ [] = [] - | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss - -fun mk_if_P_or_not_P thm = - thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P} - -fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms - -fun mk_nchotomy_tac n exhaust = - (rtac allI THEN' rtac exhaust THEN' - EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; - -fun mk_half_disc_exclus_tac m discD disc'_thm = - (dtac discD THEN' - REPEAT_DETERM_N m o etac exE THEN' - hyp_subst_tac THEN' - rtac disc'_thm) 1; - -fun mk_other_half_disc_exclus_tac half_thm = - (etac @{thm contrapos_pn} THEN' etac half_thm) 1; - -fun mk_disc_exhaust_tac n exhaust discIs = - (rtac exhaust THEN' - EVERY' (map2 (fn k => fn discI => - dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1; - -fun mk_ctr_sel_tac ctxt m discD sel_thms = - (dtac discD THEN' - (if m = 0 then - atac - else - REPEAT_DETERM_N m o etac exE THEN' - hyp_subst_tac THEN' - SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' - rtac refl)) 1; - -fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss = - (rtac exhaust' THEN' - EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [ - hyp_subst_tac THEN' - SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN' - rtac case_thm]) case_thms - (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1; - -fun mk_case_cong_tac exhaust' case_thms = - (rtac exhaust' THEN' - EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1; - -val naked_ctxt = Proof_Context.init_global @{theory HOL}; - -fun mk_split_tac exhaust' case_thms injectss distinctsss = - rtac exhaust' 1 THEN - ALLGOALS (fn k => - (hyp_subst_tac THEN' - simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @ - flat (nth distinctsss (k - 1))))) k) THEN - ALLGOALS (blast_tac naked_ctxt); - -val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; - -fun mk_split_asm_tac ctxt split = - rtac (split RS trans) 1 THEN - Local_Defs.unfold_tac ctxt split_asm_thms THEN - rtac refl 1; - -end; diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Tools/bnf_util.ML --- a/src/HOL/Codatatype/Tools/bnf_util.ML Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML Mon Sep 03 15:50:41 2012 +0200 @@ -40,6 +40,7 @@ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h + val interleave: 'a list -> 'a list -> 'a list val transpose: 'a list list -> 'a list list val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context @@ -87,6 +88,9 @@ val mk_subset: term -> term -> term val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term + val list_all_free: term list -> term -> term + val list_exists_free: term list -> term -> term + (*parameterized terms*) val mk_nthN: int -> term -> int -> term @@ -94,6 +98,7 @@ val mk_Un_upper: int -> int -> thm val mk_conjIN: int -> thm val mk_conjunctN: int -> int -> thm + val mk_disjIN: int -> int -> thm val mk_nthI: int -> int -> thm val mk_nth_conv: int -> int -> thm val mk_ordLeq_csum: int -> int -> thm -> thm @@ -108,6 +113,9 @@ val mk_permute: ''a list -> ''a list -> 'b list -> 'b list val find_indices: ''a list -> ''a list -> int list + val certifyT: Proof.context -> typ -> ctyp + val certify: Proof.context -> term -> cterm + val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int -> tactic @@ -223,6 +231,10 @@ in (x :: xs, acc'') end | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; +(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*) +fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); +fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); + (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*) fun WRAP gen_before gen_after xs core_tac = fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac; @@ -434,6 +446,16 @@ fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest; +val list_all_free = + fold_rev (fn free => fn P => + let val (x, T) = Term.dest_Free free; + in HOLogic.all_const T $ Term.absfree (x, T) P end); + +val list_exists_free = + fold_rev (fn free => fn P => + let val (x, T) = Term.dest_Free free; + in HOLogic.exists_const T $ Term.absfree (x, T) P end); + fun find_indices xs ys = map_filter I (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys); @@ -471,6 +493,11 @@ fun mk_conjIN 1 = @{thm TrueE[OF TrueI]} | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI); +fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]} + | mk_disjIN _ 1 = disjI1 + | mk_disjIN 2 2 = disjI2 + | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2; + fun mk_ordLeq_csum 1 1 thm = thm | mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}] | mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}] @@ -497,6 +524,8 @@ | mk_UnN n m = mk_UnN' (n - m) end; +fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys); + fun transpose [] = [] | transpose ([] :: xss) = transpose xss | transpose xss = map hd xss :: transpose (map tl xss); diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Tools/bnf_wrap.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Mon Sep 03 15:50:41 2012 +0200 @@ -0,0 +1,422 @@ +(* Title: HOL/Codatatype/Tools/bnf_wrap.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Wrapping existing datatypes. +*) + +signature BNF_WRAP = +sig +end; + +structure BNF_Wrap : BNF_WRAP = +struct + +open BNF_Util +open BNF_Wrap_Tactics + +val is_N = "is_"; +val un_N = "un_"; +fun mk_un_N 1 1 suf = un_N ^ suf + | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l; + +val case_congN = "case_cong"; +val case_discsN = "case_discs"; +val casesN = "cases"; +val ctr_selsN = "ctr_sels"; +val disc_exclusN = "disc_exclus"; +val disc_exhaustN = "disc_exhaust"; +val discsN = "discs"; +val distinctN = "distinct"; +val exhaustN = "exhaust"; +val injectN = "inject"; +val nchotomyN = "nchotomy"; +val selsN = "sels"; +val splitN = "split"; +val split_asmN = "split_asm"; +val weak_case_cong_thmsN = "weak_case_cong"; + +val default_name = @{binding _}; + +fun pad_list x n xs = xs @ replicate (n - length xs) x; + +fun mk_half_pairss' _ [] = [] + | mk_half_pairss' indent (y :: ys) = + indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys); + +fun mk_half_pairss ys = mk_half_pairss' [[]] ys; + +val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; + +fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T); + +fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs; + +fun name_of_ctr t = + case head_of t of + Const (s, _) => s + | Free (s, _) => s + | _ => error "Cannot extract name of constructor"; + +fun prepare_wrap prep_term ((raw_ctrs, raw_caseof), (raw_disc_names, raw_sel_namess)) + no_defs_lthy = + let + (* TODO: sanity checks on arguments *) + + (* TODO: normalize types of constructors w.r.t. each other *) + + val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; + val caseof0 = prep_term no_defs_lthy raw_caseof; + + val n = length ctrs0; + val ks = 1 upto n; + + val (T_name, As0) = dest_Type (body_type (fastype_of (hd ctrs0))); + val b = Binding.qualified_name T_name; + + val (As, B) = + no_defs_lthy + |> mk_TFrees (length As0) + ||> the_single o fst o mk_TFrees 1; + + fun mk_ctr Ts ctr = + let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in + Term.subst_atomic_types (Ts0 ~~ Ts) ctr + end; + + val T = Type (T_name, As); + val ctrs = map (mk_ctr As) ctrs0; + val ctr_Tss = map (binder_types o fastype_of) ctrs; + + val ms = map length ctr_Tss; + + val disc_names = + pad_list default_name n raw_disc_names + |> map2 (fn ctr => fn disc => + if Binding.eq_name (disc, default_name) then + Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr))) + else + disc) ctrs0; + + val sel_namess = + pad_list [] n raw_sel_namess + |> map3 (fn ctr => fn m => map2 (fn l => fn sel => + if Binding.eq_name (sel, default_name) then + Binding.name (mk_un_N m l (Long_Name.base_name (name_of_ctr ctr))) + else + sel) (1 upto m) o pad_list default_name m) ctrs0 ms; + + fun mk_caseof Ts T = + let val (binders, body) = strip_type (fastype_of caseof0) in + Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ Ts)) caseof0 + end; + + val caseofB = mk_caseof As B; + val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss; + + fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs); + + val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |> + mk_Freess "x" ctr_Tss + ||>> mk_Freess "y" ctr_Tss + ||>> mk_Frees "f" caseofB_Ts + ||>> mk_Frees "g" caseofB_Ts + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T + ||>> yield_singleton (mk_Frees "w") T + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; + + val q = Free (fst p', B --> HOLogic.boolT); + + val xctrs = map2 (curry Term.list_comb) ctrs xss; + val yctrs = map2 (curry Term.list_comb) ctrs yss; + + val xfs = map2 (curry Term.list_comb) fs xss; + val xgs = map2 (curry Term.list_comb) gs xss; + + val eta_fs = map2 eta_expand_caseof_arg xss xfs; + val eta_gs = map2 eta_expand_caseof_arg xss xgs; + + val caseofB_fs = Term.list_comb (caseofB, eta_fs); + + val exist_xs_v_eq_ctrs = + map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss; + + fun mk_sel_caseof_args k xs x T = + map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks; + + fun disc_spec b exist_xs_v_eq_ctr = + mk_Trueprop_eq (Free (Binding.name_of b, T --> HOLogic.boolT) $ v, exist_xs_v_eq_ctr); + + fun sel_spec b x xs k = + let val T' = fastype_of x in + mk_Trueprop_eq (Free (Binding.name_of b, T --> T') $ v, + Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v) + end; + + val (((raw_discs, (_, raw_disc_defs)), (raw_selss, (_, raw_sel_defss))), (lthy', lthy)) = + no_defs_lthy + |> apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn exist_xs_v_eq_ctr => + Specification.definition (SOME (b, NONE, NoSyn), + ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr))) disc_names exist_xs_v_eq_ctrs + ||>> apfst (apsnd split_list o split_list) o fold_map3 (fn bs => fn xs => fn k => + apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn x => + Specification.definition (SOME (b, NONE, NoSyn), + ((Thm.def_binding b, []), sel_spec b x xs k))) bs xs) sel_namess xss ks + ||> `Local_Theory.restore; + + (*transforms defined frees into consts (and more)*) + val phi = Proof_Context.export_morphism lthy lthy'; + + val disc_defs = map (Morphism.thm phi) raw_disc_defs; + val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss; + + val discs0 = map (Morphism.term phi) raw_discs; + val selss0 = map (map (Morphism.term phi)) raw_selss; + + fun mk_disc_or_sel Ts t = + Term.subst_atomic_types (snd (dest_Type (domain_type (fastype_of t))) ~~ Ts) t; + + val discs = map (mk_disc_or_sel As) discs0; + val selss = map (map (mk_disc_or_sel As)) selss0; + + fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); + + val goal_exhaust = + let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in + mk_imp_p (map2 mk_prem xctrs xss) + end; + + val goal_injectss = + let + fun mk_goal _ _ [] [] = [] + | mk_goal xctr yctr xs ys = + [mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), + Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))]; + in + map4 mk_goal xctrs yctrs xss yss + end; + + val goal_half_distinctss = + map (map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq)) (mk_half_pairss xctrs); + + val goal_cases = map2 (fn xctr => fn xf => mk_Trueprop_eq (caseofB_fs $ xctr, xf)) xctrs xfs; + + val goals = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases]; + + fun after_qed thmss lthy = + let + val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) = + (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); + + val exhaust_thm' = + let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in + Drule.instantiate' [] [SOME (certify lthy v)] + (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm)) + end; + + val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss; + + val (distinct_thmsss', distinct_thmsss) = + map2 (map2 append) (Library.chop_groups n half_distinct_thmss) + (transpose (Library.chop_groups n other_half_distinct_thmss)) + |> `transpose; + val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss); + + val nchotomy_thm = + let + val goal = + HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v', + Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs)); + in + Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) + end; + + val sel_thmss = + let + fun mk_thm k xs goal_case case_thm x sel_def = + let + val T = fastype_of x; + val cTs = + map ((fn T' => certifyT lthy (if T' = B then T else T')) o TFree) + (rev (Term.add_tfrees goal_case [])); + val cxs = map (certify lthy) (mk_sel_caseof_args k xs x T); + in + Local_Defs.fold lthy [sel_def] + (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm) + end; + fun mk_thms k xs goal_case case_thm sel_defs = + map2 (mk_thm k xs goal_case case_thm) xs sel_defs; + in + map5 mk_thms ks xss goal_cases case_thms sel_defss + end; + + val discD_thms = map (fn def => def RS iffD1) disc_defs; + val discI_thms = + map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs; + val not_disc_thms = + map2 (fn m => fn def => funpow m (fn thm => allI RS thm) + (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) + ms disc_defs; + + val (disc_thmss', disc_thmss) = + let + fun mk_thm discI _ [] = refl RS discI + | mk_thm _ not_disc [distinct] = distinct RS not_disc; + fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss; + in + map3 mk_thms discI_thms not_disc_thms distinct_thmsss' + |> `transpose + end; + + val disc_exclus_thms = + let + fun mk_goal ((_, disc), (_, disc')) = + Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), + HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)))); + fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); + + val bundles = ms ~~ discD_thms ~~ discs; + val half_pairss = mk_half_pairss bundles; + + val goal_halvess = map (map mk_goal) half_pairss; + val half_thmss = + map3 (fn [] => K (K []) + | [(((m, discD), _), _)] => fn disc_thm => fn [goal] => + [prove (mk_half_disc_exclus_tac m discD disc_thm) goal]) + half_pairss (flat disc_thmss') goal_halvess; + + val goal_other_halvess = map (map (mk_goal o swap)) half_pairss; + val other_half_thmss = + map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess; + in + interleave (flat half_thmss) (flat other_half_thmss) + end; + + val disc_exhaust_thm = + let + fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)]; + val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); + in + Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms) + end; + + val ctr_sel_thms = + let + fun mk_goal ctr disc sels = + Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), + mk_Trueprop_eq ((null sels ? swap) + (Term.list_comb (ctr, map (fn sel => sel $ v) sels), v)))); + val goals = map3 mk_goal ctrs discs selss; + in + map4 (fn goal => fn m => fn discD => fn sel_thms => + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_ctr_sel_tac ctxt m discD sel_thms)) + goals ms discD_thms sel_thmss + end; + + val case_disc_thm = + let + fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); + fun mk_rhs _ [f] [sels] = mk_core f sels + | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) = + Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $ + (disc $ v) $ mk_core f sels $ mk_rhs discs fs selss; + val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss); + in + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss) + |> singleton (Proof_Context.export names_lthy lthy) + end; + + val (case_cong_thm, weak_case_cong_thm) = + let + fun mk_prem xctr xs f g = + fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr), + mk_Trueprop_eq (f, g))); + + val v_eq_w = mk_Trueprop_eq (v, w); + val caseof_fs = mk_caseofB_term eta_fs; + val caseof_gs = mk_caseofB_term eta_gs; + + val goal = + Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs, + mk_Trueprop_eq (caseof_fs $ v, caseof_gs $ w)); + val goal_weak = + Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w)); + in + (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms), + Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) + |> pairself (singleton (Proof_Context.export names_lthy lthy)) + end; + + val (split_thm, split_asm_thm) = + let + fun mk_conjunct xctr xs f_xs = + list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs)); + fun mk_disjunct xctr xs f_xs = + list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr), + HOLogic.mk_not (q $ f_xs))); + + val lhs = q $ (mk_caseofB_term eta_fs $ v); + + val goal = + mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); + val goal_asm = + mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj + (map3 mk_disjunct xctrs xss xfs))); + + val split_thm = + Skip_Proof.prove lthy [] [] goal + (fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss) + |> singleton (Proof_Context.export names_lthy lthy) + val split_asm_thm = + Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} => + mk_split_asm_tac ctxt split_thm) + |> singleton (Proof_Context.export names_lthy lthy) + in + (split_thm, split_asm_thm) + end; + + (* TODO: case syntax *) + (* TODO: attributes (simp, case_names, etc.) *) + + val notes = + [(case_congN, [case_cong_thm]), + (case_discsN, [case_disc_thm]), + (casesN, case_thms), + (ctr_selsN, ctr_sel_thms), + (discsN, (flat disc_thmss)), + (disc_exclusN, disc_exclus_thms), + (disc_exhaustN, [disc_exhaust_thm]), + (distinctN, distinct_thms), + (exhaustN, [exhaust_thm]), + (injectN, (flat inject_thmss)), + (nchotomyN, [nchotomy_thm]), + (selsN, (flat sel_thmss)), + (splitN, [split_thm]), + (split_asmN, [split_asm_thm]), + (weak_case_cong_thmsN, [weak_case_cong_thm])] + |> map (fn (thmN, thms) => + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); + in + lthy |> Local_Theory.notes notes |> snd + end; + in + (goals, after_qed, lthy') + end; + +val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; + +val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]"; + +val wrap_data_cmd = (fn (goalss, after_qed, lthy) => + Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo + prepare_wrap Syntax.read_term; + +val _ = + Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype" + (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term -- + Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], [])) + >> wrap_data_cmd); + +end; diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Mon Sep 03 15:50:41 2012 +0200 @@ -0,0 +1,92 @@ +(* Title: HOL/Codatatype/Tools/bnf_wrap_tactics.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Tactics for wrapping datatypes. +*) + +signature BNF_WRAP_TACTICS = +sig + val mk_case_cong_tac: thm -> thm list -> tactic + val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic + val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic + val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic + val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic + val mk_nchotomy_tac: int -> thm -> tactic + val mk_other_half_disc_exclus_tac: thm -> tactic + val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic + val mk_split_asm_tac: Proof.context -> thm -> tactic +end; + +structure BNF_Wrap_Tactics : BNF_WRAP_TACTICS = +struct + +open BNF_Util +open BNF_Tactics + +fun triangle _ [] = [] + | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss + +fun mk_if_P_or_not_P thm = + thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P} + +fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms + +fun mk_nchotomy_tac n exhaust = + (rtac allI THEN' rtac exhaust THEN' + EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; + +fun mk_half_disc_exclus_tac m discD disc'_thm = + (dtac discD THEN' + REPEAT_DETERM_N m o etac exE THEN' + hyp_subst_tac THEN' + rtac disc'_thm) 1; + +fun mk_other_half_disc_exclus_tac half_thm = + (etac @{thm contrapos_pn} THEN' etac half_thm) 1; + +fun mk_disc_exhaust_tac n exhaust discIs = + (rtac exhaust THEN' + EVERY' (map2 (fn k => fn discI => + dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1; + +fun mk_ctr_sel_tac ctxt m discD sel_thms = + (dtac discD THEN' + (if m = 0 then + atac + else + REPEAT_DETERM_N m o etac exE THEN' + hyp_subst_tac THEN' + SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' + rtac refl)) 1; + +fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss = + (rtac exhaust' THEN' + EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [ + hyp_subst_tac THEN' + SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN' + rtac case_thm]) case_thms + (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1; + +fun mk_case_cong_tac exhaust' case_thms = + (rtac exhaust' THEN' + EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1; + +val naked_ctxt = Proof_Context.init_global @{theory HOL}; + +fun mk_split_tac exhaust' case_thms injectss distinctsss = + rtac exhaust' 1 THEN + ALLGOALS (fn k => + (hyp_subst_tac THEN' + simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @ + flat (nth distinctsss (k - 1))))) k) THEN + ALLGOALS (blast_tac naked_ctxt); + +val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; + +fun mk_split_asm_tac ctxt split = + rtac (split RS trans) 1 THEN + Local_Defs.unfold_tac ctxt split_asm_thms THEN + rtac refl 1; + +end; diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Codegenerator_Test/Candidates.thy --- a/src/HOL/Codegenerator_Test/Candidates.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Codegenerator_Test/Candidates.thy Mon Sep 03 15:50:41 2012 +0200 @@ -7,7 +7,7 @@ imports Complex_Main Library - "~~/src/HOL/Library/List_Prefix" + "~~/src/HOL/Library/Sublist" "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/ex/Records" begin diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Library/List_Prefix.thy --- a/src/HOL/Library/List_Prefix.thy Mon Sep 03 15:41:06 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,382 +0,0 @@ -(* Title: HOL/Library/List_Prefix.thy - Author: Tobias Nipkow and Markus Wenzel, TU Muenchen -*) - -header {* List prefixes and postfixes *} - -theory List_Prefix -imports List Main -begin - -subsection {* Prefix order on lists *} - -instantiation list :: (type) "{order, bot}" -begin - -definition - prefix_def: "xs \ ys \ (\zs. ys = xs @ zs)" - -definition - strict_prefix_def: "xs < ys \ xs \ ys \ xs \ (ys::'a list)" - -definition - "bot = []" - -instance proof -qed (auto simp add: prefix_def strict_prefix_def bot_list_def) - -end - -lemma prefixI [intro?]: "ys = xs @ zs ==> xs \ ys" - unfolding prefix_def by blast - -lemma prefixE [elim?]: - assumes "xs \ ys" - obtains zs where "ys = xs @ zs" - using assms unfolding prefix_def by blast - -lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys" - unfolding strict_prefix_def prefix_def by blast - -lemma strict_prefixE' [elim?]: - assumes "xs < ys" - obtains z zs where "ys = xs @ z # zs" -proof - - from `xs < ys` obtain us where "ys = xs @ us" and "xs \ ys" - unfolding strict_prefix_def prefix_def by blast - with that show ?thesis by (auto simp add: neq_Nil_conv) -qed - -lemma strict_prefixI [intro?]: "xs \ ys ==> xs \ ys ==> xs < (ys::'a list)" - unfolding strict_prefix_def by blast - -lemma strict_prefixE [elim?]: - fixes xs ys :: "'a list" - assumes "xs < ys" - obtains "xs \ ys" and "xs \ ys" - using assms unfolding strict_prefix_def by blast - - -subsection {* Basic properties of prefixes *} - -theorem Nil_prefix [iff]: "[] \ xs" - by (simp add: prefix_def) - -theorem prefix_Nil [simp]: "(xs \ []) = (xs = [])" - by (induct xs) (simp_all add: prefix_def) - -lemma prefix_snoc [simp]: "(xs \ ys @ [y]) = (xs = ys @ [y] \ xs \ ys)" -proof - assume "xs \ ys @ [y]" - then obtain zs where zs: "ys @ [y] = xs @ zs" .. - show "xs = ys @ [y] \ xs \ ys" - by (metis append_Nil2 butlast_append butlast_snoc prefixI zs) -next - assume "xs = ys @ [y] \ xs \ ys" - then show "xs \ ys @ [y]" - by (metis order_eq_iff order_trans prefixI) -qed - -lemma Cons_prefix_Cons [simp]: "(x # xs \ y # ys) = (x = y \ xs \ ys)" - by (auto simp add: prefix_def) - -lemma less_eq_list_code [code]: - "([]\'a\{equal, ord} list) \ xs \ True" - "(x\'a\{equal, ord}) # xs \ [] \ False" - "(x\'a\{equal, ord}) # xs \ y # ys \ x = y \ xs \ ys" - by simp_all - -lemma same_prefix_prefix [simp]: "(xs @ ys \ xs @ zs) = (ys \ zs)" - by (induct xs) simp_all - -lemma same_prefix_nil [iff]: "(xs @ ys \ xs) = (ys = [])" - by (metis append_Nil2 append_self_conv order_eq_iff prefixI) - -lemma prefix_prefix [simp]: "xs \ ys ==> xs \ ys @ zs" - by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI) - -lemma append_prefixD: "xs @ ys \ zs \ xs \ zs" - by (auto simp add: prefix_def) - -theorem prefix_Cons: "(xs \ y # ys) = (xs = [] \ (\zs. xs = y # zs \ zs \ ys))" - by (cases xs) (auto simp add: prefix_def) - -theorem prefix_append: - "(xs \ ys @ zs) = (xs \ ys \ (\us. xs = ys @ us \ us \ zs))" - apply (induct zs rule: rev_induct) - apply force - apply (simp del: append_assoc add: append_assoc [symmetric]) - apply (metis append_eq_appendI) - done - -lemma append_one_prefix: - "xs \ ys ==> length xs < length ys ==> xs @ [ys ! length xs] \ ys" - unfolding prefix_def - by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj - eq_Nil_appendI nth_drop') - -theorem prefix_length_le: "xs \ ys ==> length xs \ length ys" - by (auto simp add: prefix_def) - -lemma prefix_same_cases: - "(xs\<^isub>1::'a list) \ ys \ xs\<^isub>2 \ ys \ xs\<^isub>1 \ xs\<^isub>2 \ xs\<^isub>2 \ xs\<^isub>1" - unfolding prefix_def by (metis append_eq_append_conv2) - -lemma set_mono_prefix: "xs \ ys \ set xs \ set ys" - by (auto simp add: prefix_def) - -lemma take_is_prefix: "take n xs \ xs" - unfolding prefix_def by (metis append_take_drop_id) - -lemma map_prefixI: "xs \ ys \ map f xs \ map f ys" - by (auto simp: prefix_def) - -lemma prefix_length_less: "xs < ys \ length xs < length ys" - by (auto simp: strict_prefix_def prefix_def) - -lemma strict_prefix_simps [simp, code]: - "xs < [] \ False" - "[] < x # xs \ True" - "x # xs < y # ys \ x = y \ xs < ys" - by (simp_all add: strict_prefix_def cong: conj_cong) - -lemma take_strict_prefix: "xs < ys \ take n xs < ys" - apply (induct n arbitrary: xs ys) - apply (case_tac ys, simp_all)[1] - apply (metis order_less_trans strict_prefixI take_is_prefix) - done - -lemma not_prefix_cases: - assumes pfx: "\ ps \ ls" - obtains - (c1) "ps \ []" and "ls = []" - | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\ as \ xs" - | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \ a" -proof (cases ps) - case Nil then show ?thesis using pfx by simp -next - case (Cons a as) - note c = `ps = a#as` - show ?thesis - proof (cases ls) - case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil) - next - case (Cons x xs) - show ?thesis - proof (cases "x = a") - case True - have "\ as \ xs" using pfx c Cons True by simp - with c Cons True show ?thesis by (rule c2) - next - case False - with c Cons show ?thesis by (rule c3) - qed - qed -qed - -lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]: - assumes np: "\ ps \ ls" - and base: "\x xs. P (x#xs) []" - and r1: "\x xs y ys. x \ y \ P (x#xs) (y#ys)" - and r2: "\x xs y ys. \ x = y; \ xs \ ys; P xs ys \ \ P (x#xs) (y#ys)" - shows "P ps ls" using np -proof (induct ls arbitrary: ps) - case Nil then show ?case - by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) -next - case (Cons y ys) - then have npfx: "\ ps \ (y # ys)" by simp - then obtain x xs where pv: "ps = x # xs" - by (rule not_prefix_cases) auto - show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2) -qed - - -subsection {* Parallel lists *} - -definition - parallel :: "'a list => 'a list => bool" (infixl "\" 50) where - "(xs \ ys) = (\ xs \ ys \ \ ys \ xs)" - -lemma parallelI [intro]: "\ xs \ ys ==> \ ys \ xs ==> xs \ ys" - unfolding parallel_def by blast - -lemma parallelE [elim]: - assumes "xs \ ys" - obtains "\ xs \ ys \ \ ys \ xs" - using assms unfolding parallel_def by blast - -theorem prefix_cases: - obtains "xs \ ys" | "ys < xs" | "xs \ ys" - unfolding parallel_def strict_prefix_def by blast - -theorem parallel_decomp: - "xs \ ys ==> \as b bs c cs. b \ c \ xs = as @ b # bs \ ys = as @ c # cs" -proof (induct xs rule: rev_induct) - case Nil - then have False by auto - then show ?case .. -next - case (snoc x xs) - show ?case - proof (rule prefix_cases) - assume le: "xs \ ys" - then obtain ys' where ys: "ys = xs @ ys'" .. - show ?thesis - proof (cases ys') - assume "ys' = []" - then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys) - next - fix c cs assume ys': "ys' = c # cs" - then show ?thesis - by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI - same_prefix_prefix snoc.prems ys) - qed - next - assume "ys < xs" then have "ys \ xs @ [x]" by (simp add: strict_prefix_def) - with snoc have False by blast - then show ?thesis .. - next - assume "xs \ ys" - with snoc obtain as b bs c cs where neq: "(b::'a) \ c" - and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" - by blast - from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp - with neq ys show ?thesis by blast - qed -qed - -lemma parallel_append: "a \ b \ a @ c \ b @ d" - apply (rule parallelI) - apply (erule parallelE, erule conjE, - induct rule: not_prefix_induct, simp+)+ - done - -lemma parallel_appendI: "xs \ ys \ x = xs @ xs' \ y = ys @ ys' \ x \ y" - by (simp add: parallel_append) - -lemma parallel_commute: "a \ b \ b \ a" - unfolding parallel_def by auto - - -subsection {* Postfix order on lists *} - -definition - postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where - "(xs >>= ys) = (\zs. xs = zs @ ys)" - -lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" - unfolding postfix_def by blast - -lemma postfixE [elim?]: - assumes "xs >>= ys" - obtains zs where "xs = zs @ ys" - using assms unfolding postfix_def by blast - -lemma postfix_refl [iff]: "xs >>= xs" - by (auto simp add: postfix_def) -lemma postfix_trans: "\xs >>= ys; ys >>= zs\ \ xs >>= zs" - by (auto simp add: postfix_def) -lemma postfix_antisym: "\xs >>= ys; ys >>= xs\ \ xs = ys" - by (auto simp add: postfix_def) - -lemma Nil_postfix [iff]: "xs >>= []" - by (simp add: postfix_def) -lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" - by (auto simp add: postfix_def) - -lemma postfix_ConsI: "xs >>= ys \ x#xs >>= ys" - by (auto simp add: postfix_def) -lemma postfix_ConsD: "xs >>= y#ys \ xs >>= ys" - by (auto simp add: postfix_def) - -lemma postfix_appendI: "xs >>= ys \ zs @ xs >>= ys" - by (auto simp add: postfix_def) -lemma postfix_appendD: "xs >>= zs @ ys \ xs >>= ys" - by (auto simp add: postfix_def) - -lemma postfix_is_subset: "xs >>= ys ==> set ys \ set xs" -proof - - assume "xs >>= ys" - then obtain zs where "xs = zs @ ys" .. - then show ?thesis by (induct zs) auto -qed - -lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" -proof - - assume "x#xs >>= y#ys" - then obtain zs where "x#xs = zs @ y#ys" .. - then show ?thesis - by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) -qed - -lemma postfix_to_prefix [code]: "xs >>= ys \ rev ys \ rev xs" -proof - assume "xs >>= ys" - then obtain zs where "xs = zs @ ys" .. - then have "rev xs = rev ys @ rev zs" by simp - then show "rev ys <= rev xs" .. -next - assume "rev ys <= rev xs" - then obtain zs where "rev xs = rev ys @ zs" .. - then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp - then have "xs = rev zs @ ys" by simp - then show "xs >>= ys" .. -qed - -lemma distinct_postfix: "distinct xs \ xs >>= ys \ distinct ys" - by (clarsimp elim!: postfixE) - -lemma postfix_map: "xs >>= ys \ map f xs >>= map f ys" - by (auto elim!: postfixE intro: postfixI) - -lemma postfix_drop: "as >>= drop n as" - unfolding postfix_def - apply (rule exI [where x = "take n as"]) - apply simp - done - -lemma postfix_take: "xs >>= ys \ xs = take (length xs - length ys) xs @ ys" - by (clarsimp elim!: postfixE) - -lemma parallelD1: "x \ y \ \ x \ y" - by blast - -lemma parallelD2: "x \ y \ \ y \ x" - by blast - -lemma parallel_Nil1 [simp]: "\ x \ []" - unfolding parallel_def by simp - -lemma parallel_Nil2 [simp]: "\ [] \ x" - unfolding parallel_def by simp - -lemma Cons_parallelI1: "a \ b \ a # as \ b # bs" - by auto - -lemma Cons_parallelI2: "\ a = b; as \ bs \ \ a # as \ b # bs" - by (metis Cons_prefix_Cons parallelE parallelI) - -lemma not_equal_is_parallel: - assumes neq: "xs \ ys" - and len: "length xs = length ys" - shows "xs \ ys" - using len neq -proof (induct rule: list_induct2) - case Nil - then show ?case by simp -next - case (Cons a as b bs) - have ih: "as \ bs \ as \ bs" by fact - show ?case - proof (cases "a = b") - case True - then have "as \ bs" using Cons by simp - then show ?thesis by (rule Cons_parallelI2 [OF True ih]) - next - case False - then show ?thesis by (rule Cons_parallelI1) - qed -qed - -end diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Library/Prefix_Order.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Prefix_Order.thy Mon Sep 03 15:50:41 2012 +0200 @@ -0,0 +1,40 @@ +(* Title: HOL/Library/Sublist.thy + Author: Tobias Nipkow and Markus Wenzel, TU Muenchen +*) + +header {* Prefix order on lists as order class instance *} + +theory Prefix_Order +imports Sublist +begin + +instantiation list :: (type) order +begin + +definition "(xs::'a list) \ ys \ prefixeq xs ys" +definition "(xs::'a list) < ys \ xs \ ys \ \ (ys \ xs)" + +instance by (default, unfold less_eq_list_def less_list_def) auto + +end + +lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def] +lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def] +lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def] +lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def] +lemmas strict_prefixI [intro?] = prefixI [folded less_list_def] +lemmas strict_prefixE [elim?] = prefixE [folded less_list_def] +theorems Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def] +theorems prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def] +lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def] +lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def] +lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def] +lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def] +lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def] +theorems prefix_Cons = prefixeq_Cons [folded less_eq_list_def] +theorems prefix_length_le = prefixeq_length_le [folded less_eq_list_def] +lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def] +lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] = + not_prefixeq_induct [folded less_eq_list_def] + +end diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Library/Sublist.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Sublist.thy Mon Sep 03 15:50:41 2012 +0200 @@ -0,0 +1,692 @@ +(* Title: HOL/Library/Sublist.thy + Author: Tobias Nipkow and Markus Wenzel, TU Muenchen + Author: Christian Sternagel, JAIST +*) + +header {* List prefixes, suffixes, and embedding*} + +theory Sublist +imports Main +begin + +subsection {* Prefix order on lists *} + +definition prefixeq :: "'a list => 'a list => bool" where + "prefixeq xs ys \ (\zs. ys = xs @ zs)" + +definition prefix :: "'a list => 'a list => bool" where + "prefix xs ys \ prefixeq xs ys \ xs \ ys" + +interpretation prefix_order: order prefixeq prefix + by default (auto simp: prefixeq_def prefix_def) + +interpretation prefix_bot: bot prefixeq prefix Nil + by default (simp add: prefixeq_def) + +lemma prefixeqI [intro?]: "ys = xs @ zs ==> prefixeq xs ys" + unfolding prefixeq_def by blast + +lemma prefixeqE [elim?]: + assumes "prefixeq xs ys" + obtains zs where "ys = xs @ zs" + using assms unfolding prefixeq_def by blast + +lemma prefixI' [intro?]: "ys = xs @ z # zs ==> prefix xs ys" + unfolding prefix_def prefixeq_def by blast + +lemma prefixE' [elim?]: + assumes "prefix xs ys" + obtains z zs where "ys = xs @ z # zs" +proof - + from `prefix xs ys` obtain us where "ys = xs @ us" and "xs \ ys" + unfolding prefix_def prefixeq_def by blast + with that show ?thesis by (auto simp add: neq_Nil_conv) +qed + +lemma prefixI [intro?]: "prefixeq xs ys ==> xs \ ys ==> prefix xs ys" + unfolding prefix_def by blast + +lemma prefixE [elim?]: + fixes xs ys :: "'a list" + assumes "prefix xs ys" + obtains "prefixeq xs ys" and "xs \ ys" + using assms unfolding prefix_def by blast + + +subsection {* Basic properties of prefixes *} + +theorem Nil_prefixeq [iff]: "prefixeq [] xs" + by (simp add: prefixeq_def) + +theorem prefixeq_Nil [simp]: "(prefixeq xs []) = (xs = [])" + by (induct xs) (simp_all add: prefixeq_def) + +lemma prefixeq_snoc [simp]: "prefixeq xs (ys @ [y]) \ xs = ys @ [y] \ prefixeq xs ys" +proof + assume "prefixeq xs (ys @ [y])" + then obtain zs where zs: "ys @ [y] = xs @ zs" .. + show "xs = ys @ [y] \ prefixeq xs ys" + by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs) +next + assume "xs = ys @ [y] \ prefixeq xs ys" + then show "prefixeq xs (ys @ [y])" + by (metis prefix_order.eq_iff prefix_order.order_trans prefixeqI) +qed + +lemma Cons_prefixeq_Cons [simp]: "prefixeq (x # xs) (y # ys) = (x = y \ prefixeq xs ys)" + by (auto simp add: prefixeq_def) + +lemma prefixeq_code [code]: + "prefixeq [] xs \ True" + "prefixeq (x # xs) [] \ False" + "prefixeq (x # xs) (y # ys) \ x = y \ prefixeq xs ys" + by simp_all + +lemma same_prefixeq_prefixeq [simp]: "prefixeq (xs @ ys) (xs @ zs) = prefixeq ys zs" + by (induct xs) simp_all + +lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])" + by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI) + +lemma prefixeq_prefixeq [simp]: "prefixeq xs ys ==> prefixeq xs (ys @ zs)" + by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI) + +lemma append_prefixeqD: "prefixeq (xs @ ys) zs \ prefixeq xs zs" + by (auto simp add: prefixeq_def) + +theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \ (\zs. xs = y # zs \ prefixeq zs ys))" + by (cases xs) (auto simp add: prefixeq_def) + +theorem prefixeq_append: + "prefixeq xs (ys @ zs) = (prefixeq xs ys \ (\us. xs = ys @ us \ prefixeq us zs))" + apply (induct zs rule: rev_induct) + apply force + apply (simp del: append_assoc add: append_assoc [symmetric]) + apply (metis append_eq_appendI) + done + +lemma append_one_prefixeq: + "prefixeq xs ys ==> length xs < length ys ==> prefixeq (xs @ [ys ! length xs]) ys" + unfolding prefixeq_def + by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj + eq_Nil_appendI nth_drop') + +theorem prefixeq_length_le: "prefixeq xs ys ==> length xs \ length ys" + by (auto simp add: prefixeq_def) + +lemma prefixeq_same_cases: + "prefixeq (xs\<^isub>1::'a list) ys \ prefixeq xs\<^isub>2 ys \ prefixeq xs\<^isub>1 xs\<^isub>2 \ prefixeq xs\<^isub>2 xs\<^isub>1" + unfolding prefixeq_def by (metis append_eq_append_conv2) + +lemma set_mono_prefixeq: "prefixeq xs ys \ set xs \ set ys" + by (auto simp add: prefixeq_def) + +lemma take_is_prefixeq: "prefixeq (take n xs) xs" + unfolding prefixeq_def by (metis append_take_drop_id) + +lemma map_prefixeqI: "prefixeq xs ys \ prefixeq (map f xs) (map f ys)" + by (auto simp: prefixeq_def) + +lemma prefixeq_length_less: "prefix xs ys \ length xs < length ys" + by (auto simp: prefix_def prefixeq_def) + +lemma prefix_simps [simp, code]: + "prefix xs [] \ False" + "prefix [] (x # xs) \ True" + "prefix (x # xs) (y # ys) \ x = y \ prefix xs ys" + by (simp_all add: prefix_def cong: conj_cong) + +lemma take_prefix: "prefix xs ys \ prefix (take n xs) ys" + apply (induct n arbitrary: xs ys) + apply (case_tac ys, simp_all)[1] + apply (metis prefix_order.less_trans prefixI take_is_prefixeq) + done + +lemma not_prefixeq_cases: + assumes pfx: "\ prefixeq ps ls" + obtains + (c1) "ps \ []" and "ls = []" + | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\ prefixeq as xs" + | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \ a" +proof (cases ps) + case Nil then show ?thesis using pfx by simp +next + case (Cons a as) + note c = `ps = a#as` + show ?thesis + proof (cases ls) + case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefixeq_nil) + next + case (Cons x xs) + show ?thesis + proof (cases "x = a") + case True + have "\ prefixeq as xs" using pfx c Cons True by simp + with c Cons True show ?thesis by (rule c2) + next + case False + with c Cons show ?thesis by (rule c3) + qed + qed +qed + +lemma not_prefixeq_induct [consumes 1, case_names Nil Neq Eq]: + assumes np: "\ prefixeq ps ls" + and base: "\x xs. P (x#xs) []" + and r1: "\x xs y ys. x \ y \ P (x#xs) (y#ys)" + and r2: "\x xs y ys. \ x = y; \ prefixeq xs ys; P xs ys \ \ P (x#xs) (y#ys)" + shows "P ps ls" using np +proof (induct ls arbitrary: ps) + case Nil then show ?case + by (auto simp: neq_Nil_conv elim!: not_prefixeq_cases intro!: base) +next + case (Cons y ys) + then have npfx: "\ prefixeq ps (y # ys)" by simp + then obtain x xs where pv: "ps = x # xs" + by (rule not_prefixeq_cases) auto + show ?case by (metis Cons.hyps Cons_prefixeq_Cons npfx pv r1 r2) +qed + + +subsection {* Parallel lists *} + +definition + parallel :: "'a list => 'a list => bool" (infixl "\" 50) where + "(xs \ ys) = (\ prefixeq xs ys \ \ prefixeq ys xs)" + +lemma parallelI [intro]: "\ prefixeq xs ys ==> \ prefixeq ys xs ==> xs \ ys" + unfolding parallel_def by blast + +lemma parallelE [elim]: + assumes "xs \ ys" + obtains "\ prefixeq xs ys \ \ prefixeq ys xs" + using assms unfolding parallel_def by blast + +theorem prefixeq_cases: + obtains "prefixeq xs ys" | "prefix ys xs" | "xs \ ys" + unfolding parallel_def prefix_def by blast + +theorem parallel_decomp: + "xs \ ys ==> \as b bs c cs. b \ c \ xs = as @ b # bs \ ys = as @ c # cs" +proof (induct xs rule: rev_induct) + case Nil + then have False by auto + then show ?case .. +next + case (snoc x xs) + show ?case + proof (rule prefixeq_cases) + assume le: "prefixeq xs ys" + then obtain ys' where ys: "ys = xs @ ys'" .. + show ?thesis + proof (cases ys') + assume "ys' = []" + then show ?thesis by (metis append_Nil2 parallelE prefixeqI snoc.prems ys) + next + fix c cs assume ys': "ys' = c # cs" + then show ?thesis + by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixeqI + same_prefixeq_prefixeq snoc.prems ys) + qed + next + assume "prefix ys xs" then have "prefixeq ys (xs @ [x])" by (simp add: prefix_def) + with snoc have False by blast + then show ?thesis .. + next + assume "xs \ ys" + with snoc obtain as b bs c cs where neq: "(b::'a) \ c" + and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" + by blast + from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp + with neq ys show ?thesis by blast + qed +qed + +lemma parallel_append: "a \ b \ a @ c \ b @ d" + apply (rule parallelI) + apply (erule parallelE, erule conjE, + induct rule: not_prefixeq_induct, simp+)+ + done + +lemma parallel_appendI: "xs \ ys \ x = xs @ xs' \ y = ys @ ys' \ x \ y" + by (simp add: parallel_append) + +lemma parallel_commute: "a \ b \ b \ a" + unfolding parallel_def by auto + + +subsection {* Suffix order on lists *} + +definition + suffixeq :: "'a list => 'a list => bool" where + "suffixeq xs ys = (\zs. ys = zs @ xs)" + +definition suffix :: "'a list \ 'a list \ bool" where + "suffix xs ys \ \us. ys = us @ xs \ us \ []" + +lemma suffix_imp_suffixeq: + "suffix xs ys \ suffixeq xs ys" + by (auto simp: suffixeq_def suffix_def) + +lemma suffixeqI [intro?]: "ys = zs @ xs ==> suffixeq xs ys" + unfolding suffixeq_def by blast + +lemma suffixeqE [elim?]: + assumes "suffixeq xs ys" + obtains zs where "ys = zs @ xs" + using assms unfolding suffixeq_def by blast + +lemma suffixeq_refl [iff]: "suffixeq xs xs" + by (auto simp add: suffixeq_def) +lemma suffix_trans: + "suffix xs ys \ suffix ys zs \ suffix xs zs" + by (auto simp: suffix_def) +lemma suffixeq_trans: "\suffixeq xs ys; suffixeq ys zs\ \ suffixeq xs zs" + by (auto simp add: suffixeq_def) +lemma suffixeq_antisym: "\suffixeq xs ys; suffixeq ys xs\ \ xs = ys" + by (auto simp add: suffixeq_def) + +lemma suffixeq_tl [simp]: "suffixeq (tl xs) xs" + by (induct xs) (auto simp: suffixeq_def) + +lemma suffix_tl [simp]: "xs \ [] \ suffix (tl xs) xs" + by (induct xs) (auto simp: suffix_def) + +lemma Nil_suffixeq [iff]: "suffixeq [] xs" + by (simp add: suffixeq_def) +lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])" + by (auto simp add: suffixeq_def) + +lemma suffixeq_ConsI: "suffixeq xs ys \ suffixeq xs (y#ys)" + by (auto simp add: suffixeq_def) +lemma suffixeq_ConsD: "suffixeq (x#xs) ys \ suffixeq xs ys" + by (auto simp add: suffixeq_def) + +lemma suffixeq_appendI: "suffixeq xs ys \ suffixeq xs (zs @ ys)" + by (auto simp add: suffixeq_def) +lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \ suffixeq xs ys" + by (auto simp add: suffixeq_def) + +lemma suffix_set_subset: + "suffix xs ys \ set xs \ set ys" by (auto simp: suffix_def) + +lemma suffixeq_set_subset: + "suffixeq xs ys \ set xs \ set ys" by (auto simp: suffixeq_def) + +lemma suffixeq_ConsD2: "suffixeq (x#xs) (y#ys) ==> suffixeq xs ys" +proof - + assume "suffixeq (x#xs) (y#ys)" + then obtain zs where "y#ys = zs @ x#xs" .. + then show ?thesis + by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI) +qed + +lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \ prefixeq (rev xs) (rev ys)" +proof + assume "suffixeq xs ys" + then obtain zs where "ys = zs @ xs" .. + then have "rev ys = rev xs @ rev zs" by simp + then show "prefixeq (rev xs) (rev ys)" .. +next + assume "prefixeq (rev xs) (rev ys)" + then obtain zs where "rev ys = rev xs @ zs" .. + then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp + then have "ys = rev zs @ xs" by simp + then show "suffixeq xs ys" .. +qed + +lemma distinct_suffixeq: "distinct ys \ suffixeq xs ys \ distinct xs" + by (clarsimp elim!: suffixeqE) + +lemma suffixeq_map: "suffixeq xs ys \ suffixeq (map f xs) (map f ys)" + by (auto elim!: suffixeqE intro: suffixeqI) + +lemma suffixeq_drop: "suffixeq (drop n as) as" + unfolding suffixeq_def + apply (rule exI [where x = "take n as"]) + apply simp + done + +lemma suffixeq_take: "suffixeq xs ys \ ys = take (length ys - length xs) ys @ xs" + by (clarsimp elim!: suffixeqE) + +lemma suffixeq_suffix_reflclp_conv: + "suffixeq = suffix\<^sup>=\<^sup>=" +proof (intro ext iffI) + fix xs ys :: "'a list" + assume "suffixeq xs ys" + show "suffix\<^sup>=\<^sup>= xs ys" + proof + assume "xs \ ys" + with `suffixeq xs ys` show "suffix xs ys" by (auto simp: suffixeq_def suffix_def) + qed +next + fix xs ys :: "'a list" + assume "suffix\<^sup>=\<^sup>= xs ys" + thus "suffixeq xs ys" + proof + assume "suffix xs ys" thus "suffixeq xs ys" by (rule suffix_imp_suffixeq) + next + assume "xs = ys" thus "suffixeq xs ys" by (auto simp: suffixeq_def) + qed +qed + +lemma parallelD1: "x \ y \ \ prefixeq x y" + by blast + +lemma parallelD2: "x \ y \ \ prefixeq y x" + by blast + +lemma parallel_Nil1 [simp]: "\ x \ []" + unfolding parallel_def by simp + +lemma parallel_Nil2 [simp]: "\ [] \ x" + unfolding parallel_def by simp + +lemma Cons_parallelI1: "a \ b \ a # as \ b # bs" + by auto + +lemma Cons_parallelI2: "\ a = b; as \ bs \ \ a # as \ b # bs" + by (metis Cons_prefixeq_Cons parallelE parallelI) + +lemma not_equal_is_parallel: + assumes neq: "xs \ ys" + and len: "length xs = length ys" + shows "xs \ ys" + using len neq +proof (induct rule: list_induct2) + case Nil + then show ?case by simp +next + case (Cons a as b bs) + have ih: "as \ bs \ as \ bs" by fact + show ?case + proof (cases "a = b") + case True + then have "as \ bs" using Cons by simp + then show ?thesis by (rule Cons_parallelI2 [OF True ih]) + next + case False + then show ?thesis by (rule Cons_parallelI1) + qed +qed + +lemma suffix_reflclp_conv: + "suffix\<^sup>=\<^sup>= = suffixeq" + by (intro ext) (auto simp: suffixeq_def suffix_def) + +lemma suffix_lists: + "suffix xs ys \ ys \ lists A \ xs \ lists A" + unfolding suffix_def by auto + + +subsection {* Embedding on lists *} + +inductive + emb :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" + for P :: "('a \ 'a \ bool)" +where + emb_Nil [intro, simp]: "emb P [] ys" +| emb_Cons [intro] : "emb P xs ys \ emb P xs (y#ys)" +| emb_Cons2 [intro]: "P x y \ emb P xs ys \ emb P (x#xs) (y#ys)" + +lemma emb_Nil2 [simp]: + assumes "emb P xs []" shows "xs = []" + using assms by (cases rule: emb.cases) auto + +lemma emb_Cons_Nil [simp]: + "emb P (x#xs) [] = False" +proof - + { assume "emb P (x#xs) []" + from emb_Nil2 [OF this] have False by simp + } moreover { + assume False + hence "emb P (x#xs) []" by simp + } ultimately show ?thesis by blast +qed + +lemma emb_append2 [intro]: + "emb P xs ys \ emb P xs (zs @ ys)" + by (induct zs) auto + +lemma emb_prefix [intro]: + assumes "emb P xs ys" shows "emb P xs (ys @ zs)" + using assms + by (induct arbitrary: zs) auto + +lemma emb_ConsD: + assumes "emb P (x#xs) ys" + shows "\us v vs. ys = us @ v # vs \ P x v \ emb P xs vs" +using assms +proof (induct x\"x#xs" y\"ys" arbitrary: x xs ys) + case emb_Cons thus ?case by (metis append_Cons) +next + case (emb_Cons2 x y xs ys) + thus ?case by (cases xs) (auto, blast+) +qed + +lemma emb_appendD: + assumes "emb P (xs @ ys) zs" + shows "\us vs. zs = us @ vs \ emb P xs us \ emb P ys vs" +using assms +proof (induction xs arbitrary: ys zs) + case Nil thus ?case by auto +next + case (Cons x xs) + then obtain us v vs where "zs = us @ v # vs" + and "P x v" and "emb P (xs @ ys) vs" by (auto dest: emb_ConsD) + with Cons show ?case by (metis append_Cons append_assoc emb_Cons2 emb_append2) +qed + +lemma emb_suffix: + assumes "emb P xs ys" and "suffix ys zs" + shows "emb P xs zs" + using assms(2) and emb_append2 [OF assms(1)] by (auto simp: suffix_def) + +lemma emb_suffixeq: + assumes "emb P xs ys" and "suffixeq ys zs" + shows "emb P xs zs" + using assms and emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto + +lemma emb_length: "emb P xs ys \ length xs \ length ys" + by (induct rule: emb.induct) auto + +(*FIXME: move*) +definition transp_on :: "('a \ 'a \ bool) \ 'a set \ bool" where + "transp_on P A \ \a\A. \b\A. \c\A. P a b \ P b c \ P a c" +lemma transp_onI [Pure.intro]: + "(\a b c. \a \ A; b \ A; c \ A; P a b; P b c\ \ P a c) \ transp_on P A" + unfolding transp_on_def by blast + +lemma transp_on_emb: + assumes "transp_on P A" + shows "transp_on (emb P) (lists A)" +proof + fix xs ys zs + assume "emb P xs ys" and "emb P ys zs" + and "xs \ lists A" and "ys \ lists A" and "zs \ lists A" + thus "emb P xs zs" + proof (induction arbitrary: zs) + case emb_Nil show ?case by blast + next + case (emb_Cons xs ys y) + from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs + where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast + hence "emb P ys (v#vs)" by blast + hence "emb P ys zs" unfolding zs by (rule emb_append2) + from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp + next + case (emb_Cons2 x y xs ys) + from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs + where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast + with emb_Cons2 have "emb P xs vs" by simp + moreover have "P x v" + proof - + from zs and `zs \ lists A` have "v \ A" by auto + moreover have "x \ A" and "y \ A" using emb_Cons2 by simp_all + ultimately show ?thesis using `P x y` and `P y v` and assms + unfolding transp_on_def by blast + qed + ultimately have "emb P (x#xs) (v#vs)" by blast + thus ?case unfolding zs by (rule emb_append2) + qed +qed + + +subsection {* Sublists (special case of embedding) *} + +abbreviation sub :: "'a list \ 'a list \ bool" where + "sub xs ys \ emb (op =) xs ys" + +lemma sub_Cons2: "sub xs ys \ sub (x#xs) (x#ys)" by auto + +lemma sub_same_length: + assumes "sub xs ys" and "length xs = length ys" shows "xs = ys" + using assms by (induct) (auto dest: emb_length) + +lemma not_sub_length [simp]: "length ys < length xs \ \ sub xs ys" + by (metis emb_length linorder_not_less) + +lemma [code]: + "emb P [] ys \ True" + "emb P (x#xs) [] \ False" + by (simp_all) + +lemma sub_Cons': "sub (x#xs) ys \ sub xs ys" + by (induct xs) (auto dest: emb_ConsD) + +lemma sub_Cons2': + assumes "sub (x#xs) (x#ys)" shows "sub xs ys" + using assms by (cases) (rule sub_Cons') + +lemma sub_Cons2_neq: + assumes "sub (x#xs) (y#ys)" + shows "x \ y \ sub (x#xs) ys" + using assms by (cases) auto + +lemma sub_Cons2_iff [simp, code]: + "sub (x#xs) (y#ys) = (if x = y then sub xs ys else sub (x#xs) ys)" + by (metis emb_Cons emb_Cons2 [of "op =", OF refl] sub_Cons2' sub_Cons2_neq) + +lemma sub_append': "sub (zs @ xs) (zs @ ys) \ sub xs ys" + by (induct zs) simp_all + +lemma sub_refl [simp, intro!]: "sub xs xs" by (induct xs) simp_all + +lemma sub_antisym: + assumes "sub xs ys" and "sub ys xs" + shows "xs = ys" +using assms +proof (induct) + case emb_Nil + from emb_Nil2 [OF this] show ?case by simp +next + case emb_Cons2 thus ?case by simp +next + case emb_Cons thus ?case + by (metis sub_Cons' emb_length Suc_length_conv Suc_n_not_le_n) +qed + +lemma transp_on_sub: "transp_on sub UNIV" +proof - + have "transp_on (op =) UNIV" by (simp add: transp_on_def) + from transp_on_emb [OF this] show ?thesis by simp +qed + +lemma sub_trans: "sub xs ys \ sub ys zs \ sub xs zs" + using transp_on_sub [unfolded transp_on_def] by blast + +lemma sub_append_le_same_iff: "sub (xs @ ys) ys \ xs = []" + by (auto dest: emb_length) + +lemma emb_append_mono: + "\ emb P xs xs'; emb P ys ys' \ \ emb P (xs@ys) (xs'@ys')" +apply (induct rule: emb.induct) + apply (metis eq_Nil_appendI emb_append2) + apply (metis append_Cons emb_Cons) +by (metis append_Cons emb_Cons2) + + +subsection {* Appending elements *} + +lemma sub_append [simp]: + "sub (xs @ zs) (ys @ zs) \ sub xs ys" (is "?l = ?r") +proof + { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'" + hence "xs' = xs @ zs & ys' = ys @ zs \ sub xs ys" + proof (induct arbitrary: xs ys zs) + case emb_Nil show ?case by simp + next + case (emb_Cons xs' ys' x) + { assume "ys=[]" hence ?case using emb_Cons(1) by auto } + moreover + { fix us assume "ys = x#us" + hence ?case using emb_Cons(2) by(simp add: emb.emb_Cons) } + ultimately show ?case by (auto simp:Cons_eq_append_conv) + next + case (emb_Cons2 x y xs' ys') + { assume "xs=[]" hence ?case using emb_Cons2(1) by auto } + moreover + { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using emb_Cons2 by auto} + moreover + { fix us assume "xs=x#us" "ys=[]" hence ?case using emb_Cons2(2) by bestsimp } + ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv) + qed } + moreover assume ?l + ultimately show ?r by blast +next + assume ?r thus ?l by (metis emb_append_mono sub_refl) +qed + +lemma sub_drop_many: "sub xs ys \ sub xs (zs @ ys)" + by (induct zs) auto + +lemma sub_rev_drop_many: "sub xs ys \ sub xs (ys @ zs)" + by (metis append_Nil2 emb_Nil emb_append_mono) + + +subsection {* Relation to standard list operations *} + +lemma sub_map: + assumes "sub xs ys" shows "sub (map f xs) (map f ys)" + using assms by (induct) auto + +lemma sub_filter_left [simp]: "sub (filter P xs) xs" + by (induct xs) auto + +lemma sub_filter [simp]: + assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)" + using assms by (induct) auto + +lemma "sub xs ys \ (\ N. xs = sublist ys N)" (is "?L = ?R") +proof + assume ?L + thus ?R + proof (induct) + case emb_Nil show ?case by (metis sublist_empty) + next + case (emb_Cons xs ys x) + then obtain N where "xs = sublist ys N" by blast + hence "xs = sublist (x#ys) (Suc ` N)" + by (clarsimp simp add:sublist_Cons inj_image_mem_iff) + thus ?case by blast + next + case (emb_Cons2 x y xs ys) + then obtain N where "xs = sublist ys N" by blast + hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))" + by (clarsimp simp add:sublist_Cons inj_image_mem_iff) + thus ?case unfolding `x = y` by blast + qed +next + assume ?R + then obtain N where "xs = sublist ys N" .. + moreover have "sub (sublist ys N) ys" + proof (induct ys arbitrary:N) + case Nil show ?case by simp + next + case Cons thus ?case by (auto simp: sublist_Cons) + qed + ultimately show ?L by simp +qed + +end diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Library/Sublist_Order.thy --- a/src/HOL/Library/Sublist_Order.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Library/Sublist_Order.thy Mon Sep 03 15:50:41 2012 +0200 @@ -6,7 +6,7 @@ header {* Sublist Ordering *} theory Sublist_Order -imports Main +imports Sublist begin text {* @@ -20,241 +20,63 @@ instantiation list :: (type) ord begin -inductive less_eq_list where - empty [simp, intro!]: "[] \ xs" - | drop: "ys \ xs \ ys \ x # xs" - | take: "ys \ xs \ x # ys \ x # xs" +definition + "(xs :: 'a list) \ ys \ sub xs ys" definition - "(xs \ 'a list) < ys \ xs \ ys \ \ ys \ xs" + "(xs :: 'a list) < ys \ xs \ ys \ \ ys \ xs" -instance proof qed +instance .. end -lemma le_list_length: "xs \ ys \ length xs \ length ys" -by (induct rule: less_eq_list.induct) auto - -lemma le_list_same_length: "xs \ ys \ length xs = length ys \ xs = ys" -by (induct rule: less_eq_list.induct) (auto dest: le_list_length) - -lemma not_le_list_length[simp]: "length ys < length xs \ ~ xs <= ys" -by (metis le_list_length linorder_not_less) - -lemma le_list_below_empty [simp]: "xs \ [] \ xs = []" -by (auto dest: le_list_length) - -lemma le_list_drop_many: "xs \ ys \ xs \ zs @ ys" -by (induct zs) (auto intro: drop) - -lemma [code]: "[] <= xs \ True" -by(metis less_eq_list.empty) - -lemma [code]: "(x#xs) <= [] \ False" -by simp - -lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys" -proof- - { fix xs' ys' - assume "xs' <= ys" - hence "ALL x xs. xs' = x#xs \ xs <= ys" - proof induct - case empty thus ?case by simp - next - case drop thus ?case by (metis less_eq_list.drop) - next - case take thus ?case by (simp add: drop) - qed } - from this[OF assms] show ?thesis by simp -qed - -lemma le_list_drop_Cons2: -assumes "x#xs <= x#ys" shows "xs <= ys" -using assms -proof cases - case drop thus ?thesis by (metis le_list_drop_Cons list.inject) -qed simp_all - -lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys" -shows "x ~= y \ x # xs <= ys" -using assms proof cases qed auto - -lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \ - (if x=y then xs <= ys else (x#xs) <= ys)" -by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq) - -lemma le_list_take_many_iff: "zs @ xs \ zs @ ys \ xs \ ys" -by (induct zs) (auto intro: take) - -lemma le_list_Cons_EX: - assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs" -proof- - { fix xys zs :: "'a list" assume "xys <= zs" - hence "ALL x ys. xys = x#ys \ (EX us vs. zs = us @ x # vs & ys <= vs)" - proof induct - case empty show ?case by simp - next - case take thus ?case by (metis list.inject self_append_conv2) - next - case drop thus ?case by (metis append_eq_Cons_conv) - qed - } with assms show ?thesis by blast -qed - -instantiation list :: (type) order -begin - -instance proof +instance list :: (type) order +proof fix xs ys :: "'a list" show "xs < ys \ xs \ ys \ \ ys \ xs" unfolding less_list_def .. next fix xs :: "'a list" - show "xs \ xs" by (induct xs) (auto intro!: less_eq_list.drop) + show "xs \ xs" by (simp add: less_eq_list_def) next fix xs ys :: "'a list" - assume "xs <= ys" - hence "ys <= xs \ xs = ys" - proof induct - case empty show ?case by simp - next - case take thus ?case by simp - next - case drop thus ?case - by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n) - qed - moreover assume "ys <= xs" - ultimately show "xs = ys" by blast + assume "xs <= ys" and "ys <= xs" + thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym) next fix xs ys zs :: "'a list" - assume "xs <= ys" - hence "ys <= zs \ xs <= zs" - proof (induct arbitrary:zs) - case empty show ?case by simp - next - case (take xs ys x) show ?case - proof - assume "x # ys <= zs" - with take show "x # xs <= zs" - by(metis le_list_Cons_EX le_list_drop_many less_eq_list.take local.take(2)) - qed - next - case drop thus ?case by (metis le_list_drop_Cons) - qed - moreover assume "ys <= zs" - ultimately show "xs <= zs" by blast + assume "xs <= ys" and "ys <= zs" + thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans) qed -end - -lemma le_list_append_le_same_iff: "xs @ ys <= ys \ xs=[]" -by (auto dest: le_list_length) - -lemma le_list_append_mono: "\ xs <= xs'; ys <= ys' \ \ xs@ys <= xs'@ys'" -apply (induct rule:less_eq_list.induct) - apply (metis eq_Nil_appendI le_list_drop_many) - apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans) -apply simp -done +lemmas less_eq_list_induct [consumes 1, case_names empty drop take] = + emb.induct [of "op =", folded less_eq_list_def] +lemmas less_eq_list_drop = emb.emb_Cons [of "op =", folded less_eq_list_def] +lemmas le_list_Cons2_iff [simp, code] = sub_Cons2_iff [folded less_eq_list_def] +lemmas le_list_map = sub_map [folded less_eq_list_def] +lemmas le_list_filter = sub_filter [folded less_eq_list_def] +lemmas le_list_length = emb_length [of "op =", folded less_eq_list_def] lemma less_list_length: "xs < ys \ length xs < length ys" -by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def) + by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def) lemma less_list_empty [simp]: "[] < xs \ xs \ []" -by (metis empty order_less_le) + by (metis less_eq_list_def emb_Nil order_less_le) -lemma less_list_below_empty[simp]: "xs < [] \ False" -by (metis empty less_list_def) +lemma less_list_below_empty [simp]: "xs < [] \ False" + by (metis emb_Nil less_eq_list_def less_list_def) lemma less_list_drop: "xs < ys \ xs < x # ys" -by (unfold less_le) (auto intro: less_eq_list.drop) + by (unfold less_le less_eq_list_def) (auto) lemma less_list_take_iff: "x # xs < x # ys \ xs < ys" -by (metis le_list_Cons2_iff less_list_def) + by (metis sub_Cons2_iff less_list_def less_eq_list_def) lemma less_list_drop_many: "xs < ys \ xs < zs @ ys" -by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2) + by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def) lemma less_list_take_many_iff: "zs @ xs < zs @ ys \ xs < ys" -by (metis le_list_take_many_iff less_list_def) - - -subsection {* Appending elements *} - -lemma le_list_rev_take_iff[simp]: "xs @ zs \ ys @ zs \ xs \ ys" (is "?L = ?R") -proof - { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'" - hence "xs' = xs @ zs & ys' = ys @ zs \ xs <= ys" - proof (induct arbitrary: xs ys zs) - case empty show ?case by simp - next - case (drop xs' ys' x) - { assume "ys=[]" hence ?case using drop(1) by auto } - moreover - { fix us assume "ys = x#us" - hence ?case using drop(2) by(simp add: less_eq_list.drop) } - ultimately show ?case by (auto simp:Cons_eq_append_conv) - next - case (take xs' ys' x) - { assume "xs=[]" hence ?case using take(1) by auto } - moreover - { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take(2) by auto} - moreover - { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp } - ultimately show ?case by (auto simp:Cons_eq_append_conv) - qed } - moreover assume ?L - ultimately show ?R by blast -next - assume ?R thus ?L by(metis le_list_append_mono order_refl) -qed + by (metis less_list_def less_eq_list_def sub_append') lemma less_list_rev_take: "xs @ zs < ys @ zs \ xs < ys" -by (unfold less_le) auto - -lemma le_list_rev_drop_many: "xs \ ys \ xs \ ys @ zs" -by (metis append_Nil2 empty le_list_append_mono) - - -subsection {* Relation to standard list operations *} - -lemma le_list_map: "xs \ ys \ map f xs \ map f ys" -by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop) - -lemma le_list_filter_left[simp]: "filter f xs \ xs" -by (induct xs) (auto intro: less_eq_list.drop) - -lemma le_list_filter: "xs \ ys \ filter f xs \ filter f ys" -by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop) - -lemma "xs \ ys \ (EX N. xs = sublist ys N)" (is "?L = ?R") -proof - assume ?L - thus ?R - proof induct - case empty show ?case by (metis sublist_empty) - next - case (drop xs ys x) - then obtain N where "xs = sublist ys N" by blast - hence "xs = sublist (x#ys) (Suc ` N)" - by (clarsimp simp add:sublist_Cons inj_image_mem_iff) - thus ?case by blast - next - case (take xs ys x) - then obtain N where "xs = sublist ys N" by blast - hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))" - by (clarsimp simp add:sublist_Cons inj_image_mem_iff) - thus ?case by blast - qed -next - assume ?R - then obtain N where "xs = sublist ys N" .. - moreover have "sublist ys N <= ys" - proof (induct ys arbitrary:N) - case Nil show ?case by simp - next - case Cons thus ?case by (auto simp add:sublist_Cons drop) - qed - ultimately show ?L by simp -qed + by (unfold less_le less_eq_list_def) auto end diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/ROOT --- a/src/HOL/ROOT Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/ROOT Mon Sep 03 15:50:41 2012 +0200 @@ -38,7 +38,7 @@ description {* Classical Higher-order Logic -- batteries included *} theories Library - List_Prefix + Sublist List_lexord Sublist_Order Product_Lattice diff -r 7df19036392e -r 8ab9fb2483a9 src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Mon Sep 03 15:41:06 2012 +0200 +++ b/src/HOL/Unix/Unix.thy Mon Sep 03 15:50:41 2012 +0200 @@ -7,7 +7,7 @@ theory Unix imports Nested_Environment - "~~/src/HOL/Library/List_Prefix" + "~~/src/HOL/Library/Sublist" begin text {* @@ -952,7 +952,7 @@ with tr obtain opt where root': "root' = update (path_of x) opt root" by cases auto show ?thesis - proof (rule prefix_cases) + proof (rule prefixeq_cases) assume "path_of x \ path" with inv root' have "\perms. access root' path user\<^isub>1 perms = access root path user\<^isub>1 perms" @@ -960,7 +960,7 @@ with inv show "invariant root' path" by (simp only: invariant_def) next - assume "path_of x \ path" + assume "prefixeq (path_of x) path" then obtain ys where path: "path = path_of x @ ys" .. show ?thesis @@ -997,7 +997,7 @@ by (simp only: invariant_def access_def) qed next - assume "path < path_of x" + assume "prefix path (path_of x)" then obtain y ys where path: "path_of x = path @ y # ys" .. obtain dir' where diff -r 7df19036392e -r 8ab9fb2483a9 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Mon Sep 03 15:41:06 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Mon Sep 03 15:50:41 2012 +0200 @@ -107,9 +107,9 @@ case _ => true }).toList html_panel.render(filtered_results) - case _ => + case _ => html_panel.render(Nil) } - case None => + case None => html_panel.render(Nil) } } }