# HG changeset patch # User wenzelm # Date 1334429093 -7200 # Node ID 80ddf2016b6c82268dd27dd1318e8925d7e82ce8 # Parent 214bfaae738d68685ed949ba220befe42fa32a3c# Parent ffa6e10df0911679ba7d13be3019d5fc96b98e7c merged; diff -r ffa6e10df091 -r 80ddf2016b6c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Apr 14 20:10:10 2012 +0200 +++ b/src/HOL/IsaMakefile Sat Apr 14 20:44:53 2012 +0200 @@ -1027,7 +1027,7 @@ ex/Quicksort.thy ex/ROOT.ML \ ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \ ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \ - ex/Set_Algebras.thy ex/Simproc_Tests.thy ex/SVC_Oracle.thy \ + ex/Simproc_Tests.thy ex/SVC_Oracle.thy \ ex/sledgehammer_tactics.ML ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \ ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \ diff -r ffa6e10df091 -r 80ddf2016b6c src/HOL/TPTP/lib/Tools/tptp_graph --- a/src/HOL/TPTP/lib/Tools/tptp_graph Sat Apr 14 20:10:10 2012 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_graph Sat Apr 14 20:44:53 2012 +0200 @@ -10,25 +10,26 @@ #FIXME inline or move to settings DOT2TEX=dot2tex DOT=dot -SED=sed +PERL=perl PDFLATEX=pdflatex [ -n "$ISABELLE_PDFLATEX" ] && PDFLATEX=$ISABELLE_PDFLATEX DOT2TEX_VERSION="$($DOT2TEX -V 2> /dev/null)" -DOT_VERSION="$($DOT -V 2> /dev/null)" -SED_VERSION="$($SED --version | head -1 2> /dev/null)" +DOT_VERSION="$($DOT -V 2>&1 | grep Graphviz)" +PERL_VERSION="$($PERL -v | grep -e "v[0-9]\+." 2> /dev/null)" PDFLATEX_VERSION="$($PDFLATEX -version | head -1 2> /dev/null)" function check_deps() { #FIXME how well does this work across different platforms and/or versions of # the tools? - for DEP in DOT2TEX_VERSION DOT_VERSION SED_VERSION PDFLATEX_VERSION + for DEP in DOT2TEX DOT PERL PDFLATEX do - eval DEP_VAL=\$$DEP - if [ -z "$DEP_VAL" ]; then + eval DEP_VAL=\$${DEP} + eval DEP_VERSION=\$${DEP}_VERSION + if [ -z "$DEP_VERSION" ]; then echo "$DEP not installed" else - echo "$DEP_VAL" + echo "$DEP ($DEP_VAL) : $DEP_VERSION" fi done } @@ -53,7 +54,7 @@ KEEP_TEMP="" NON_EXEC="" -while getopts "dknX" OPT +while getopts "dnkX" OPT do #FIXME could add "quiet" mode to send stderr (and some stdout) to /dev/null case "$OPT" in @@ -106,7 +107,6 @@ "$ISABELLE_PROCESS" -e "$LOADER" Pure } - if [ "$OUTPUT_FORMAT" -eq 0 ]; then [ -z "$NON_EXEC" ] && generate_dot "$1" "$2" exit 0 @@ -114,14 +114,12 @@ ## set some essential variables -[ -z "$TMPDIR" ] && TMPDIR=/tmp WORKDIR="" while : do - WORKDIR="$TMPDIR/tptpgraph$RANDOM" - if [ ! -d "$WORKDIR" ]; then - break - fi + #FIXME not perfectly reliable method, but probably good enough + WORKDIR="${ISABELLE_TMP_PREFIX}-tptpgraph$RANDOM" + [ ! -d "$WORKDIR" ] && break done OUTPUT_FILENAME="$(basename "$2")" FILEDIR="$(cd "$(dirname "$2")"; cd "$(pwd -P)"; pwd)" @@ -136,7 +134,7 @@ if [ -z "$NON_EXEC" ]; then $DOT -Txdot "${FILENAME}.dot" \ | $DOT2TEX -f pgf -t raw --crop > "${FILENAME}.tex" - $SED -i 's/_/\\_/g' "${FILENAME}.tex" + $PERL -w -p -e 's/_/\\_/g' "${FILENAME}.tex" fi if [ "$OUTPUT_FORMAT" -eq 1 ]; then diff -r ffa6e10df091 -r 80ddf2016b6c src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Sat Apr 14 20:10:10 2012 +0200 +++ b/src/HOL/ex/ROOT.ML Sat Apr 14 20:44:53 2012 +0200 @@ -67,7 +67,6 @@ "Quicksort", "Birthday_Paradox", "List_to_Set_Comprehension_Examples", - "Set_Algebras", "Seq", "Simproc_Tests", "Executable_Relation" diff -r ffa6e10df091 -r 80ddf2016b6c src/HOL/ex/Set_Algebras.thy --- a/src/HOL/ex/Set_Algebras.thy Sat Apr 14 20:10:10 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,371 +0,0 @@ -(* Title: HOL/ex/Set_Algebras.thy - Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM -*) - -header {* Algebraic operations on sets *} - -theory Set_Algebras -imports Main Interpretation_with_Defs -begin - -text {* - This library lifts operations like addition and muliplication to - sets. It was designed to support asymptotic calculations. See the - comments at the top of theory @{text BigO}. -*} - -definition set_plus :: "'a::plus set \ 'a set \ 'a set" (infixl "\" 65) where - "A \ B = {c. \a\A. \b\B. c = a + b}" - -definition set_times :: "'a::times set \ 'a set \ 'a set" (infixl "\" 70) where - "A \ B = {c. \a\A. \b\B. c = a * b}" - -definition elt_set_plus :: "'a::plus \ 'a set \ 'a set" (infixl "+o" 70) where - "a +o B = {c. \b\B. c = a + b}" - -definition elt_set_times :: "'a::times \ 'a set \ 'a set" (infixl "*o" 80) where - "a *o B = {c. \b\B. c = a * b}" - -abbreviation (input) elt_set_eq :: "'a \ 'a set \ bool" (infix "=o" 50) where - "x =o A \ x \ A" - -interpretation set_add!: semigroup "set_plus :: 'a::semigroup_add set \ 'a set \ 'a set" - by default (force simp add: set_plus_def add.assoc) - -interpretation set_add!: abel_semigroup "set_plus :: 'a::ab_semigroup_add set \ 'a set \ 'a set" - by default (force simp add: set_plus_def add.commute) - -interpretation set_add!: monoid "set_plus :: 'a::monoid_add set \ 'a set \ 'a set" "{0}" - by default (simp_all add: set_plus_def) - -interpretation set_add!: comm_monoid "set_plus :: 'a::comm_monoid_add set \ 'a set \ 'a set" "{0}" - by default (simp add: set_plus_def) - -interpretation set_add!: monoid_add "set_plus :: 'a::monoid_add set \ 'a set \ 'a set" "{0}" - defines listsum_set is set_add.listsum - by default (simp_all add: set_add.assoc) - -interpretation - set_add!: comm_monoid_add "set_plus :: 'a::comm_monoid_add set \ 'a set \ 'a set" "{0}" - defines setsum_set is set_add.setsum - where "monoid_add.listsum set_plus {0::'a} = listsum_set" -proof - - show "class.comm_monoid_add (set_plus :: 'a set \ 'a set \ 'a set) {0}" - by default (simp_all add: set_add.commute) - then interpret set_add!: comm_monoid_add "set_plus :: 'a set \ 'a set \ 'a set" "{0}" . - show "monoid_add.listsum set_plus {0::'a} = listsum_set" - by (simp only: listsum_set_def) -qed - -interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \ 'a set \ 'a set" - by default (force simp add: set_times_def mult.assoc) - -interpretation - set_mult!: abel_semigroup "set_times :: 'a::ab_semigroup_mult set \ 'a set \ 'a set" - by default (force simp add: set_times_def mult.commute) - -interpretation set_mult!: monoid "set_times :: 'a::monoid_mult set \ 'a set \ 'a set" "{1}" - by default (simp_all add: set_times_def) - -interpretation - set_mult!: comm_monoid "set_times :: 'a::comm_monoid_mult set \ 'a set \ 'a set" "{1}" - by default (simp add: set_times_def) - -interpretation set_mult!: monoid_mult "{1}" "set_times :: 'a::monoid_mult set \ 'a set \ 'a set" - defines power_set is set_mult.power - by default (simp_all add: set_mult.assoc) - -interpretation - set_mult!: comm_monoid_mult "set_times :: 'a::comm_monoid_mult set \ 'a set \ 'a set" "{1}" - defines setprod_set is set_mult.setprod - where "power.power {1} set_times = power_set" -proof - - show "class.comm_monoid_mult (set_times :: 'a set \ 'a set \ 'a set) {1}" - by default (simp_all add: set_mult.commute) - then interpret set_mult!: comm_monoid_mult "set_times :: 'a set \ 'a set \ 'a set" "{1}" . - show "power.power {1} set_times = power_set" - by (simp add: power_set_def) -qed - -lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \ D" - by (auto simp add: set_plus_def) - -lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C" - by (auto simp add: elt_set_plus_def) - -lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \ (b +o D) = (a + b) +o (C \ D)" - apply (auto simp add: elt_set_plus_def set_plus_def add_ac) - apply (rule_tac x = "ba + bb" in exI) - apply (auto simp add: add_ac) - apply (rule_tac x = "aa + a" in exI) - apply (auto simp add: add_ac) - done - -lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = (a + b) +o C" - by (auto simp add: elt_set_plus_def add_assoc) - -lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \ C = a +o (B \ C)" - apply (auto simp add: elt_set_plus_def set_plus_def) - apply (blast intro: add_ac) - apply (rule_tac x = "a + aa" in exI) - apply (rule conjI) - apply (rule_tac x = "aa" in bexI) - apply auto - apply (rule_tac x = "ba" in bexI) - apply (auto simp add: add_ac) - done - -theorem set_plus_rearrange4: "C \ ((a::'a::comm_monoid_add) +o D) = a +o (C \ D)" - apply (auto intro!: simp add: elt_set_plus_def set_plus_def add_ac) - apply (rule_tac x = "aa + ba" in exI) - apply (auto simp add: add_ac) - done - -theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2 - set_plus_rearrange3 set_plus_rearrange4 - -lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D" - by (auto simp add: elt_set_plus_def) - -lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==> - C \ E <= D \ F" - by (auto simp add: set_plus_def) - -lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \ D" - by (auto simp add: elt_set_plus_def set_plus_def) - -lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==> - a +o D <= D \ C" - by (auto simp add: elt_set_plus_def set_plus_def add_ac) - -lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \ D" - apply (subgoal_tac "a +o B <= a +o D") - apply (erule order_trans) - apply (erule set_plus_mono3) - apply (erule set_plus_mono) - done - -lemma set_plus_mono_b: "C <= D ==> x : a +o C - ==> x : a +o D" - apply (frule set_plus_mono) - apply auto - done - -lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \ E ==> - x : D \ F" - apply (frule set_plus_mono2) - prefer 2 - apply force - apply assumption - done - -lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \ D" - apply (frule set_plus_mono3) - apply auto - done - -lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==> - x : a +o D ==> x : D \ C" - apply (frule set_plus_mono4) - apply auto - done - -lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C" - by (auto simp add: elt_set_plus_def) - -lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \ B" - apply (auto intro!: simp add: set_plus_def) - apply (rule_tac x = 0 in bexI) - apply (rule_tac x = x in bexI) - apply (auto simp add: add_ac) - done - -lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C" - by (auto simp add: elt_set_plus_def add_ac diff_minus) - -lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C" - apply (auto simp add: elt_set_plus_def add_ac diff_minus) - apply (subgoal_tac "a = (a + - b) + b") - apply (rule bexI, assumption, assumption) - apply (auto simp add: add_ac) - done - -lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)" - by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus, - assumption) - -lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \ D" - by (auto simp add: set_times_def) - -lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C" - by (auto simp add: elt_set_times_def) - -lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \ - (b *o D) = (a * b) *o (C \ D)" - apply (auto simp add: elt_set_times_def set_times_def) - apply (rule_tac x = "ba * bb" in exI) - apply (auto simp add: mult_ac) - apply (rule_tac x = "aa * a" in exI) - apply (auto simp add: mult_ac) - done - -lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) = - (a * b) *o C" - by (auto simp add: elt_set_times_def mult_assoc) - -lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \ C = - a *o (B \ C)" - apply (auto simp add: elt_set_times_def set_times_def) - apply (blast intro: mult_ac) - apply (rule_tac x = "a * aa" in exI) - apply (rule conjI) - apply (rule_tac x = "aa" in bexI) - apply auto - apply (rule_tac x = "ba" in bexI) - apply (auto simp add: mult_ac) - done - -theorem set_times_rearrange4: "C \ ((a::'a::comm_monoid_mult) *o D) = - a *o (C \ D)" - apply (auto intro!: simp add: elt_set_times_def set_times_def - mult_ac) - apply (rule_tac x = "aa * ba" in exI) - apply (auto simp add: mult_ac) - done - -theorems set_times_rearranges = set_times_rearrange set_times_rearrange2 - set_times_rearrange3 set_times_rearrange4 - -lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D" - by (auto simp add: elt_set_times_def) - -lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==> - C \ E <= D \ F" - by (auto simp add: set_times_def) - -lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \ D" - by (auto simp add: elt_set_times_def set_times_def) - -lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==> - a *o D <= D \ C" - by (auto simp add: elt_set_times_def set_times_def mult_ac) - -lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \ D" - apply (subgoal_tac "a *o B <= a *o D") - apply (erule order_trans) - apply (erule set_times_mono3) - apply (erule set_times_mono) - done - -lemma set_times_mono_b: "C <= D ==> x : a *o C - ==> x : a *o D" - apply (frule set_times_mono) - apply auto - done - -lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \ E ==> - x : D \ F" - apply (frule set_times_mono2) - prefer 2 - apply force - apply assumption - done - -lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \ D" - apply (frule set_times_mono3) - apply auto - done - -lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==> - x : a *o D ==> x : D \ C" - apply (frule set_times_mono4) - apply auto - done - -lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C" - by (auto simp add: elt_set_times_def) - -lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)= - (a * b) +o (a *o C)" - by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs) - -lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \ C) = - (a *o B) \ (a *o C)" - apply (auto simp add: set_plus_def elt_set_times_def ring_distribs) - apply blast - apply (rule_tac x = "b + bb" in exI) - apply (auto simp add: ring_distribs) - done - -lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \ D <= - a *o D \ C \ D" - apply (auto simp add: - elt_set_plus_def elt_set_times_def set_times_def - set_plus_def ring_distribs) - apply auto - done - -theorems set_times_plus_distribs = - set_times_plus_distrib - set_times_plus_distrib2 - -lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==> - - a : C" - by (auto simp add: elt_set_times_def) - -lemma set_neg_intro2: "(a::'a::ring_1) : C ==> - - a : (- 1) *o C" - by (auto simp add: elt_set_times_def) - -lemma set_plus_image: - fixes S T :: "'n::semigroup_add set" shows "S \ T = (\(x, y). x + y) ` (S \ T)" - unfolding set_plus_def by (fastforce simp: image_iff) - -lemma set_setsum_alt: - assumes fin: "finite I" - shows "setsum_set S I = {setsum s I |s. \i\I. s i \ S i}" - (is "_ = ?setsum I") -using fin -proof induct - case (insert x F) - have "setsum_set S (insert x F) = S x \ ?setsum F" - using insert.hyps by auto - also have "...= {s x + setsum s F |s. \ i\insert x F. s i \ S i}" - proof - - { - fix y s assume "y \ S x" "\i\F. s i \ S i" - then have "\s'. y + setsum s F = s' x + setsum s' F \ (\i\insert x F. s' i \ S i)" - using insert.hyps - by (intro exI[of _ "\i. if i \ F then s i else y"]) (auto simp add: set_plus_def) - } - then show ?thesis - unfolding set_plus_def by auto - qed - finally show ?case - using insert.hyps by auto -qed auto - -lemma setsum_set_cond_linear: - fixes f :: "('a::comm_monoid_add) set \ ('b::comm_monoid_add) set" - assumes [intro!]: "\A B. P A \ P B \ P (A \ B)" "P {0}" - and f: "\A B. P A \ P B \ f (A \ B) = f A \ f B" "f {0} = {0}" - assumes all: "\i. i \ I \ P (S i)" - shows "f (setsum_set S I) = setsum_set (f \ S) I" -proof cases - assume "finite I" from this all show ?thesis - proof induct - case (insert x F) - from `finite F` `\i. i \ insert x F \ P (S i)` have "P (setsum_set S F)" - by induct auto - with insert show ?case - by (simp, subst f) auto - qed (auto intro!: f) -qed (auto intro!: f) - -lemma setsum_set_linear: - fixes f :: "('a::comm_monoid_add) set => ('b::comm_monoid_add) set" - assumes "\A B. f(A) \ f(B) = f(A \ B)" "f {0} = {0}" - shows "f (setsum_set S I) = setsum_set (f \ S) I" - using setsum_set_cond_linear[of "\x. True" f I S] assms by auto - -end