--- 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"
--- 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
--- 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
'("\\."
--- 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,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"
-if [ "$OUTPUT_FORMAT" = "eps" ]; then
- perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTPUT"
-else
- perl -p -e "s,<any>,$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"
+
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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.
--- 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" .
--- 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" .
--- 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" .
--- 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"
--- 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"
--- 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 `(\<And>x y. PROP P x y)`)
-(*Extended List_Prefix*)
+(*Extended Sublist*)
definition prefCl where
"prefCl Kl = (\<forall> kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
--- /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
--- 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
--- 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 *}
--- 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 \<times> (T + 'Tree) fset"
+codata_raw Tree: 'Tree = "N \<times> (T + 'Tree) fset"
section {* Sugar notations for Tree *}
--- 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 \<times> 'trm + 'a \<times> 'trm + ('a \<times> 'trm) fset \<times> 'trm"
+data_raw trm: 'trm = "'a + 'trm \<times> 'trm + 'a \<times> 'trm + ('a \<times> 'trm) fset \<times> 'trm"
section {* Customization of terms *}
--- 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 \<times> 'list"
+data_raw listF: 'list = "unit + 'a \<times> 'list"
definition "NilF = listF_fld (Inl ())"
definition "Conss a as \<equiv> listF_fld (Inr (a, as))"
--- 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 \<times> 's"
+codata_raw stream: 's = "'a \<times> 's"
-bnf_codata llist: 'llist = "unit + 'a \<times> 'llist"
+codata_raw llist: 'llist = "unit + 'a \<times> '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 \<times> 'b1 + 'a \<times> 'b2"
+codata_raw F1: 'b1 = "'a \<times> 'b1 + 'a \<times> 'b2"
and F2: 'b2 = "unit + 'b1 * 'b2"
-bnf_codata EXPR: 'E = "'T + 'T \<times> 'E"
+codata_raw EXPR: 'E = "'T + 'T \<times> 'E"
and TERM: 'T = "'F + 'F \<times> 'T"
and FACTOR: 'F = "'a + 'b + 'E"
-bnf_codata llambda:
+codata_raw llambda:
'trm = "string +
'trm \<times> 'trm +
string \<times> 'trm +
(string \<times> 'trm) fset \<times> 'trm"
-bnf_codata par_llambda:
+codata_raw par_llambda:
'trm = "'a +
'trm \<times> 'trm +
'a \<times> 'trm +
@@ -53,29 +53,29 @@
'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c)
*)
-bnf_codata tree: 'tree = "unit + 'a \<times> 'forest"
+codata_raw tree: 'tree = "unit + 'a \<times> 'forest"
and forest: 'forest = "unit + 'tree \<times> 'forest"
-bnf_codata CPS: 'a = "'b + 'b \<Rightarrow> 'a"
+codata_raw CPS: 'a = "'b + 'b \<Rightarrow> 'a"
-bnf_codata fun_rhs: 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'a"
+codata_raw fun_rhs: 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'a"
-bnf_codata fun_rhs': 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'b10 \<Rightarrow>
+codata_raw fun_rhs': 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'b10 \<Rightarrow>
'b11 \<Rightarrow> 'b12 \<Rightarrow> 'b13 \<Rightarrow> 'b14 \<Rightarrow> 'b15 \<Rightarrow> 'b16 \<Rightarrow> 'b17 \<Rightarrow> 'b18 \<Rightarrow> 'b19 \<Rightarrow> 'b20 \<Rightarrow> 'a"
-bnf_codata some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
+codata_raw some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
and in_here: 'c = "'d \<times> 'b + 'e"
-bnf_codata some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
+codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
and in_here': 'c = "'d + 'e"
-bnf_codata some_killing'': 'a = "'b \<Rightarrow> 'c"
+codata_raw some_killing'': 'a = "'b \<Rightarrow> 'c"
and in_here'': 'c = "'d \<times> 'b + 'e"
-bnf_codata less_killing: 'a = "'b \<Rightarrow> 'c"
+codata_raw less_killing: 'a = "'b \<Rightarrow> '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 \<times> 'K5"
and K4': 'K4 = "'K5 + 'a list list list"
--- 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 \<times> 'list"
+data_raw mylist: 'list = "unit + 'a \<times> '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 \<times> 'trm +
string \<times> 'trm +
(string \<times> 'trm) fset \<times> 'trm"
-bnf_data par_lambda:
+data_raw par_lambda:
'trm = "'a +
'trm \<times> 'trm +
'a \<times> 'trm +
@@ -39,7 +39,7 @@
('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
*)
-bnf_data F1: 'b1 = "'a \<times> 'b1 + 'a \<times> 'b2"
+data_raw F1: 'b1 = "'a \<times> 'b1 + 'a \<times> '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 \<times> 'forest"
+data_raw tree: 'tree = "unit + 'a \<times> 'forest"
and forest: 'forest = "unit + 'tree \<times> 'forest"
(*
@@ -55,7 +55,7 @@
' a branch = Branch of 'a * 'a tree ('c = 'a * 'b)
*)
-bnf_data tree': 'tree = "unit + 'branch \<times> 'branch"
+data_raw tree': 'tree = "unit + 'branch \<times> 'branch"
and branch: 'branch = "'a \<times> 'tree"
(*
@@ -64,54 +64,54 @@
factor = C 'a | V 'b | Paren exp ('e = 'a + 'b + 'c)
*)
-bnf_data EXPR: 'E = "'T + 'T \<times> 'E"
+data_raw EXPR: 'E = "'T + 'T \<times> 'E"
and TERM: 'T = "'F + 'F \<times> 'T"
and FACTOR: 'F = "'a + 'b + 'E"
-bnf_data some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
+data_raw some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
and in_here: 'c = "'d \<times> 'b + 'e"
-bnf_data nofail1: 'a = "'a \<times> 'b + 'b"
-bnf_data nofail2: 'a = "('a \<times> 'b \<times> 'a \<times> 'b) list"
-bnf_data nofail3: 'a = "'b \<times> ('a \<times> 'b \<times> 'a \<times> 'b) fset"
-bnf_data nofail4: 'a = "('a \<times> ('a \<times> 'b \<times> 'a \<times> 'b) fset) list"
+data_raw nofail1: 'a = "'a \<times> 'b + 'b"
+data_raw nofail2: 'a = "('a \<times> 'b \<times> 'a \<times> 'b) list"
+data_raw nofail3: 'a = "'b \<times> ('a \<times> 'b \<times> 'a \<times> 'b) fset"
+data_raw nofail4: 'a = "('a \<times> ('a \<times> 'b \<times> 'a \<times> 'b) fset) list"
(*
-bnf_data fail: 'a = "'a \<times> 'b \<times> 'a \<times> 'b list"
-bnf_data fail: 'a = "'a \<times> 'b \<times> 'a \<times> 'b"
-bnf_data fail: 'a = "'a \<times> 'b + 'a"
-bnf_data fail: 'a = "'a \<times> 'b"
+data_raw fail: 'a = "'a \<times> 'b \<times> 'a \<times> 'b list"
+data_raw fail: 'a = "'a \<times> 'b \<times> 'a \<times> 'b"
+data_raw fail: 'a = "'a \<times> 'b + 'a"
+data_raw fail: 'a = "'a \<times> '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 \<times> 'L2"
+data_raw fail1: 'L1 = "'L2 list \<times> 'L2"
and fail2: 'L2 = "'L2 fset \<times> 'L3"
and fail2: 'L3 = "'L1"
-bnf_data fail1: 'L1 = "'L2 list \<times> 'L2"
+data_raw fail1: 'L1 = "'L2 list \<times> 'L2"
and fail2: 'L2 = "'L1 fset \<times> '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 \<times> '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
--- 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)
--- 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 \<times> 's"
+codata_raw stream: 's = "'a \<times> 's"
(* selectors for streams *)
definition "hdd as \<equiv> fst (stream_unf as)"
--- 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 \<times> 'tree listF"
+hide_const (open) Sublist.sub
+
+codata_raw treeFI: 'tree = "'a \<times> '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
--- 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 "\<odot>" 50) where
"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
-bnf_codata treeFsetI: 't = "'a \<times> 't fset"
+codata_raw treeFsetI: 't = "'a \<times> 't fset"
(* selectors for trees *)
definition "lab t \<equiv> fst (treeFsetI_unf t)"
--- 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;
--- 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));
--- 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));
--- 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;
--- 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;
--- 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);
--- /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;
--- /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;
--- 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
--- 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 \<le> ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
-
-definition
- strict_prefix_def: "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> (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 \<le> ys"
- unfolding prefix_def by blast
-
-lemma prefixE [elim?]:
- assumes "xs \<le> 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 \<noteq> 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 \<le> ys ==> xs \<noteq> 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 \<le> ys" and "xs \<noteq> ys"
- using assms unfolding strict_prefix_def by blast
-
-
-subsection {* Basic properties of prefixes *}
-
-theorem Nil_prefix [iff]: "[] \<le> xs"
- by (simp add: prefix_def)
-
-theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"
- by (induct xs) (simp_all add: prefix_def)
-
-lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
-proof
- assume "xs \<le> ys @ [y]"
- then obtain zs where zs: "ys @ [y] = xs @ zs" ..
- show "xs = ys @ [y] \<or> xs \<le> ys"
- by (metis append_Nil2 butlast_append butlast_snoc prefixI zs)
-next
- assume "xs = ys @ [y] \<or> xs \<le> ys"
- then show "xs \<le> ys @ [y]"
- by (metis order_eq_iff order_trans prefixI)
-qed
-
-lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
- by (auto simp add: prefix_def)
-
-lemma less_eq_list_code [code]:
- "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True"
- "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False"
- "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
- by simp_all
-
-lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
- by (induct xs) simp_all
-
-lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
- by (metis append_Nil2 append_self_conv order_eq_iff prefixI)
-
-lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
- by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI)
-
-lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
- by (auto simp add: prefix_def)
-
-theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
- by (cases xs) (auto simp add: prefix_def)
-
-theorem prefix_append:
- "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> 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 \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> 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 \<le> ys ==> length xs \<le> length ys"
- by (auto simp add: prefix_def)
-
-lemma prefix_same_cases:
- "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
- unfolding prefix_def by (metis append_eq_append_conv2)
-
-lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
- by (auto simp add: prefix_def)
-
-lemma take_is_prefix: "take n xs \<le> xs"
- unfolding prefix_def by (metis append_take_drop_id)
-
-lemma map_prefixI: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
- by (auto simp: prefix_def)
-
-lemma prefix_length_less: "xs < ys \<Longrightarrow> length xs < length ys"
- by (auto simp: strict_prefix_def prefix_def)
-
-lemma strict_prefix_simps [simp, code]:
- "xs < [] \<longleftrightarrow> False"
- "[] < x # xs \<longleftrightarrow> True"
- "x # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
- by (simp_all add: strict_prefix_def cong: conj_cong)
-
-lemma take_strict_prefix: "xs < ys \<Longrightarrow> 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: "\<not> ps \<le> ls"
- obtains
- (c1) "ps \<noteq> []" and "ls = []"
- | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> as \<le> xs"
- | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> 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 "\<not> as \<le> 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: "\<not> ps \<le> ls"
- and base: "\<And>x xs. P (x#xs) []"
- and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
- and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> 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: "\<not> ps \<le> (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 "\<parallel>" 50) where
- "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"
-
-lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
- unfolding parallel_def by blast
-
-lemma parallelE [elim]:
- assumes "xs \<parallel> ys"
- obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"
- using assms unfolding parallel_def by blast
-
-theorem prefix_cases:
- obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"
- unfolding parallel_def strict_prefix_def by blast
-
-theorem parallel_decomp:
- "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> 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 \<le> 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 \<le> xs @ [x]" by (simp add: strict_prefix_def)
- with snoc have False by blast
- then show ?thesis ..
- next
- assume "xs \<parallel> ys"
- with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> 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 \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
- apply (rule parallelI)
- apply (erule parallelE, erule conjE,
- induct rule: not_prefix_induct, simp+)+
- done
-
-lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y"
- by (simp add: parallel_append)
-
-lemma parallel_commute: "a \<parallel> b \<longleftrightarrow> b \<parallel> a"
- unfolding parallel_def by auto
-
-
-subsection {* Postfix order on lists *}
-
-definition
- postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where
- "(xs >>= ys) = (\<exists>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: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs"
- by (auto simp add: postfix_def)
-lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> x#xs >>= ys"
- by (auto simp add: postfix_def)
-lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys"
- by (auto simp add: postfix_def)
-
-lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys"
- by (auto simp add: postfix_def)
-lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys"
- by (auto simp add: postfix_def)
-
-lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> 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 \<longleftrightarrow> rev ys \<le> 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 \<Longrightarrow> xs >>= ys \<Longrightarrow> distinct ys"
- by (clarsimp elim!: postfixE)
-
-lemma postfix_map: "xs >>= ys \<Longrightarrow> 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 \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"
- by (clarsimp elim!: postfixE)
-
-lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y"
- by blast
-
-lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> y \<le> x"
- by blast
-
-lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
- unfolding parallel_def by simp
-
-lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"
- unfolding parallel_def by simp
-
-lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs"
- by auto
-
-lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
- by (metis Cons_prefix_Cons parallelE parallelI)
-
-lemma not_equal_is_parallel:
- assumes neq: "xs \<noteq> ys"
- and len: "length xs = length ys"
- shows "xs \<parallel> 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 \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
- show ?case
- proof (cases "a = b")
- case True
- then have "as \<noteq> 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
--- /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) \<le> ys \<equiv> prefixeq xs ys"
+definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> 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
--- /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 \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
+
+definition prefix :: "'a list => 'a list => bool" where
+ "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> 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 \<noteq> 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 \<noteq> 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 \<noteq> 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]) \<longleftrightarrow> xs = ys @ [y] \<or> prefixeq xs ys"
+proof
+ assume "prefixeq xs (ys @ [y])"
+ then obtain zs where zs: "ys @ [y] = xs @ zs" ..
+ show "xs = ys @ [y] \<or> prefixeq xs ys"
+ by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs)
+next
+ assume "xs = ys @ [y] \<or> 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 \<and> prefixeq xs ys)"
+ by (auto simp add: prefixeq_def)
+
+lemma prefixeq_code [code]:
+ "prefixeq [] xs \<longleftrightarrow> True"
+ "prefixeq (x # xs) [] \<longleftrightarrow> False"
+ "prefixeq (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> 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 \<Longrightarrow> prefixeq xs zs"
+ by (auto simp add: prefixeq_def)
+
+theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> prefixeq zs ys))"
+ by (cases xs) (auto simp add: prefixeq_def)
+
+theorem prefixeq_append:
+ "prefixeq xs (ys @ zs) = (prefixeq xs ys \<or> (\<exists>us. xs = ys @ us \<and> 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 \<le> length ys"
+ by (auto simp add: prefixeq_def)
+
+lemma prefixeq_same_cases:
+ "prefixeq (xs\<^isub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^isub>2 ys \<Longrightarrow> prefixeq xs\<^isub>1 xs\<^isub>2 \<or> prefixeq xs\<^isub>2 xs\<^isub>1"
+ unfolding prefixeq_def by (metis append_eq_append_conv2)
+
+lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> 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 \<Longrightarrow> prefixeq (map f xs) (map f ys)"
+ by (auto simp: prefixeq_def)
+
+lemma prefixeq_length_less: "prefix xs ys \<Longrightarrow> length xs < length ys"
+ by (auto simp: prefix_def prefixeq_def)
+
+lemma prefix_simps [simp, code]:
+ "prefix xs [] \<longleftrightarrow> False"
+ "prefix [] (x # xs) \<longleftrightarrow> True"
+ "prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefix xs ys"
+ by (simp_all add: prefix_def cong: conj_cong)
+
+lemma take_prefix: "prefix xs ys \<Longrightarrow> 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: "\<not> prefixeq ps ls"
+ obtains
+ (c1) "ps \<noteq> []" and "ls = []"
+ | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefixeq as xs"
+ | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> 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 "\<not> 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: "\<not> prefixeq ps ls"
+ and base: "\<And>x xs. P (x#xs) []"
+ and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
+ and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefixeq xs ys; P xs ys \<rbrakk> \<Longrightarrow> 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: "\<not> 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 "\<parallel>" 50) where
+ "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
+
+lemma parallelI [intro]: "\<not> prefixeq xs ys ==> \<not> prefixeq ys xs ==> xs \<parallel> ys"
+ unfolding parallel_def by blast
+
+lemma parallelE [elim]:
+ assumes "xs \<parallel> ys"
+ obtains "\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs"
+ using assms unfolding parallel_def by blast
+
+theorem prefixeq_cases:
+ obtains "prefixeq xs ys" | "prefix ys xs" | "xs \<parallel> ys"
+ unfolding parallel_def prefix_def by blast
+
+theorem parallel_decomp:
+ "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> 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 \<parallel> ys"
+ with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> 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 \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
+ apply (rule parallelI)
+ apply (erule parallelE, erule conjE,
+ induct rule: not_prefixeq_induct, simp+)+
+ done
+
+lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y"
+ by (simp add: parallel_append)
+
+lemma parallel_commute: "a \<parallel> b \<longleftrightarrow> b \<parallel> a"
+ unfolding parallel_def by auto
+
+
+subsection {* Suffix order on lists *}
+
+definition
+ suffixeq :: "'a list => 'a list => bool" where
+ "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)"
+
+definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+ "suffix xs ys \<equiv> \<exists>us. ys = us @ xs \<and> us \<noteq> []"
+
+lemma suffix_imp_suffixeq:
+ "suffix xs ys \<Longrightarrow> 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 \<Longrightarrow> suffix ys zs \<Longrightarrow> suffix xs zs"
+ by (auto simp: suffix_def)
+lemma suffixeq_trans: "\<lbrakk>suffixeq xs ys; suffixeq ys zs\<rbrakk> \<Longrightarrow> suffixeq xs zs"
+ by (auto simp add: suffixeq_def)
+lemma suffixeq_antisym: "\<lbrakk>suffixeq xs ys; suffixeq ys xs\<rbrakk> \<Longrightarrow> 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 \<noteq> [] \<Longrightarrow> 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 \<Longrightarrow> suffixeq xs (y#ys)"
+ by (auto simp add: suffixeq_def)
+lemma suffixeq_ConsD: "suffixeq (x#xs) ys \<Longrightarrow> suffixeq xs ys"
+ by (auto simp add: suffixeq_def)
+
+lemma suffixeq_appendI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (zs @ ys)"
+ by (auto simp add: suffixeq_def)
+lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \<Longrightarrow> suffixeq xs ys"
+ by (auto simp add: suffixeq_def)
+
+lemma suffix_set_subset:
+ "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffix_def)
+
+lemma suffixeq_set_subset:
+ "suffixeq xs ys \<Longrightarrow> set xs \<subseteq> 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 \<longleftrightarrow> 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 \<Longrightarrow> suffixeq xs ys \<Longrightarrow> distinct xs"
+ by (clarsimp elim!: suffixeqE)
+
+lemma suffixeq_map: "suffixeq xs ys \<Longrightarrow> 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 \<Longrightarrow> 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 \<noteq> 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 \<parallel> y \<Longrightarrow> \<not> prefixeq x y"
+ by blast
+
+lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefixeq y x"
+ by blast
+
+lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
+ unfolding parallel_def by simp
+
+lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"
+ unfolding parallel_def by simp
+
+lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs"
+ by auto
+
+lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
+ by (metis Cons_prefixeq_Cons parallelE parallelI)
+
+lemma not_equal_is_parallel:
+ assumes neq: "xs \<noteq> ys"
+ and len: "length xs = length ys"
+ shows "xs \<parallel> 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 \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
+ show ?case
+ proof (cases "a = b")
+ case True
+ then have "as \<noteq> 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 \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A"
+ unfolding suffix_def by auto
+
+
+subsection {* Embedding on lists *}
+
+inductive
+ emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+ for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
+where
+ emb_Nil [intro, simp]: "emb P [] ys"
+| emb_Cons [intro] : "emb P xs ys \<Longrightarrow> emb P xs (y#ys)"
+| emb_Cons2 [intro]: "P x y \<Longrightarrow> emb P xs ys \<Longrightarrow> 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 \<Longrightarrow> 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 "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> emb P xs vs"
+using assms
+proof (induct x\<equiv>"x#xs" y\<equiv>"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 "\<exists>us vs. zs = us @ vs \<and> emb P xs us \<and> 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 \<Longrightarrow> length xs \<le> length ys"
+ by (induct rule: emb.induct) auto
+
+(*FIXME: move*)
+definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
+ "transp_on P A \<equiv> \<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c"
+lemma transp_onI [Pure.intro]:
+ "(\<And>a b c. \<lbrakk>a \<in> A; b \<in> A; c \<in> A; P a b; P b c\<rbrakk> \<Longrightarrow> P a c) \<Longrightarrow> 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 \<in> lists A" and "ys \<in> lists A" and "zs \<in> 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 \<in> lists A` have "v \<in> A" by auto
+ moreover have "x \<in> A" and "y \<in> 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 \<Rightarrow> 'a list \<Rightarrow> bool" where
+ "sub xs ys \<equiv> emb (op =) xs ys"
+
+lemma sub_Cons2: "sub xs ys \<Longrightarrow> 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 \<Longrightarrow> \<not> sub xs ys"
+ by (metis emb_length linorder_not_less)
+
+lemma [code]:
+ "emb P [] ys \<longleftrightarrow> True"
+ "emb P (x#xs) [] \<longleftrightarrow> False"
+ by (simp_all)
+
+lemma sub_Cons': "sub (x#xs) ys \<Longrightarrow> 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 \<noteq> y \<Longrightarrow> 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) \<longleftrightarrow> 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 \<Longrightarrow> sub ys zs \<Longrightarrow> sub xs zs"
+ using transp_on_sub [unfolded transp_on_def] by blast
+
+lemma sub_append_le_same_iff: "sub (xs @ ys) ys \<longleftrightarrow> xs = []"
+ by (auto dest: emb_length)
+
+lemma emb_append_mono:
+ "\<lbrakk> emb P xs xs'; emb P ys ys' \<rbrakk> \<Longrightarrow> 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) \<longleftrightarrow> 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 \<longrightarrow> 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 \<Longrightarrow> sub xs (zs @ ys)"
+ by (induct zs) auto
+
+lemma sub_rev_drop_many: "sub xs ys \<Longrightarrow> 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 \<longleftrightarrow> (\<exists> 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
--- 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!]: "[] \<le> xs"
- | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"
- | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
+definition
+ "(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys"
definition
- "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+ "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
-instance proof qed
+instance ..
end
-lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
-by (induct rule: less_eq_list.induct) auto
-
-lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
-by (induct rule: less_eq_list.induct) (auto dest: le_list_length)
-
-lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys"
-by (metis le_list_length linorder_not_less)
-
-lemma le_list_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
-by (auto dest: le_list_length)
-
-lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
-by (induct zs) (auto intro: drop)
-
-lemma [code]: "[] <= xs \<longleftrightarrow> True"
-by(metis less_eq_list.empty)
-
-lemma [code]: "(x#xs) <= [] \<longleftrightarrow> 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 \<longrightarrow> 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 \<Longrightarrow> x # xs <= ys"
-using assms proof cases qed auto
-
-lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow>
- (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 \<le> zs @ ys \<longleftrightarrow> xs \<le> 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 \<longrightarrow> (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 \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def ..
next
fix xs :: "'a list"
- show "xs \<le> xs" by (induct xs) (auto intro!: less_eq_list.drop)
+ show "xs \<le> xs" by (simp add: less_eq_list_def)
next
fix xs ys :: "'a list"
- assume "xs <= ys"
- hence "ys <= xs \<longrightarrow> 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 \<longrightarrow> 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 \<longleftrightarrow> xs=[]"
-by (auto dest: le_list_length)
-
-lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 \<longleftrightarrow> xs \<noteq> []"
-by (metis empty order_less_le)
+ by (metis less_eq_list_def emb_Nil order_less_le)
-lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False"
-by (metis empty less_list_def)
+lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
+ by (metis emb_Nil less_eq_list_def less_list_def)
lemma less_list_drop: "xs < ys \<Longrightarrow> 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 \<longleftrightarrow> 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 \<Longrightarrow> 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 \<longleftrightarrow> xs < ys"
-by (metis le_list_take_many_iff less_list_def)
-
-
-subsection {* Appending elements *}
-
-lemma le_list_rev_take_iff[simp]: "xs @ zs \<le> ys @ zs \<longleftrightarrow> xs \<le> ys" (is "?L = ?R")
-proof
- { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"
- hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> 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 \<longleftrightarrow> xs < ys"
-by (unfold less_le) auto
-
-lemma le_list_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
-by (metis append_Nil2 empty le_list_append_mono)
-
-
-subsection {* Relation to standard list operations *}
-
-lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> 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 \<le> xs"
-by (induct xs) (auto intro: less_eq_list.drop)
-
-lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
-by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
-
-lemma "xs \<le> ys \<longleftrightarrow> (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
--- 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
--- 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 \<parallel> path"
with inv root'
have "\<And>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 \<le> 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
--- 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)
}
}
}