--- a/Admin/makebundle Fri Jun 04 19:36:41 2010 +0200
+++ b/Admin/makebundle Sat Jun 05 07:52:45 2010 +0200
@@ -2,11 +2,6 @@
#
# makebundle -- re-package with add-on components
-## global settings
-
-TMP="/var/tmp/isabelle-makebundle$$"
-
-
## diagnostics
PRG=$(basename "$0")
@@ -14,9 +9,10 @@
function usage()
{
echo
- echo "Usage: $PRG ARCHIVE COMPONENTS"
+ echo "Usage: $PRG ARCHIVE PLATFORM"
echo
- echo " Re-package Isabelle distribution with add-on components."
+ echo " Re-package Isabelle source distribution with add-on components"
+ echo " and logic images"
echo
exit 1
}
@@ -28,34 +24,37 @@
}
-## process command line
+## implicit and explicit arguments
-[ "$#" -lt 1 ] && usage
+TMP="/var/tmp/isabelle-makebundle$$"
+mkdir "$TMP" || fail "Cannot create directory $TMP"
+
+LOGICS="HOL HOL-Nominal HOLCF ZF"
+
+[ "$#" -ne 2 ] && usage
ARCHIVE="$1"; shift
+PLATFORM="$1"; shift
-declare -a COMPONENTS
-COMPONENTS=("$@")
+[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
## main
-mkdir "$TMP" || fail "Cannot create directory $TMP"
-
ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
-[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
tar -C "$TMP" -x -z -f "$ARCHIVE"
+
echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
-for COMPONENT in "${COMPONENTS[@]}"
+for CONTRIB in "$ARCHIVE_DIR"/contrib/*.tar.gz
do
- tar -C "$ISABELLE_HOME/contrib" -x -z -f "$COMPONENT"
- NAME="$(basename "$COMPONENT" .tar.gz)"
- [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $COMPONENT"
+ tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB"
+ NAME="$(basename "$CONTRIB" .tar.gz)"
+ [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB"
if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
echo "component $NAME"
@@ -65,9 +64,20 @@
fi
done
-tar -C "$TMP" -c -z \
- -f "${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle.tar.gz" \
- Isabelle "$ISABELLE_NAME"
+
+for LOGIC in $LOGICS
+do
+ LOGIC_ARCHIVE="$ARCHIVE_DIR/${LOGIC}_${PLATFORM}.tar.gz"
+ [ -f "$LOGIC_ARCHIVE" ] || fail "Bad logic archive: $LOGIC_ARCHIVE"
+ echo "logic $LOGIC"
+ tar -C "$ISABELLE_HOME" -x -z -f "$LOGIC_ARCHIVE"
+done
+
+
+BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
+
+echo "$(basename "$BUNDLE_ARCHIVE")"
+tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" Isabelle "$ISABELLE_NAME"
# clean up
--- a/src/HOL/Metis_Examples/BigO.thy Fri Jun 04 19:36:41 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Sat Jun 05 07:52:45 2010 +0200
@@ -880,25 +880,18 @@
(* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less
le_max_iff_disj min_max.le_supE min_max.sup_absorb2
min_max.sup_commute) *)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>A. k A \<le> f A"
-have 1: "\<And>(X1\<Colon>'b\<Colon>linordered_idom) X2. \<not> max X1 X2 < X1"
- by (metis linorder_not_less le_maxI1) (*sort inserted by hand*)
-assume 2: "(0\<Colon>'b) \<le> k x - g x"
-have 3: "\<not> k x - g x < (0\<Colon>'b)"
- by (metis 2 linorder_not_less)
-have 4: "\<And>X1 X2. min X1 (k X2) \<le> f X2"
- by (metis min_max.inf_le2 min_max.le_inf_iff min_max.le_iff_inf 0)
-have 5: "\<bar>g x - f x\<bar> = f x - g x"
- by (metis abs_minus_commute combine_common_factor mult_zero_right minus_add_cancel minus_zero abs_if diff_less_eq min_max.inf_commute 4 linorder_not_le min_max.le_iff_inf 3 diff_less_0_iff_less linorder_not_less)
-have 6: "max (0\<Colon>'b) (k x - g x) = k x - g x"
- by (metis min_max.le_iff_sup 2)
-assume 7: "\<not> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
-have 8: "\<not> k x - g x \<le> f x - g x"
- by (metis 5 abs_minus_commute 7 min_max.sup_commute 6)
-show "False"
- by (metis min_max.sup_commute min_max.inf_commute min_max.sup_inf_absorb min_max.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)
+proof -
+ fix x :: 'a
+ assume "\<forall>x\<Colon>'a. k x \<le> f x"
+ hence F1: "\<forall>x\<^isub>1\<Colon>'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2)
+ assume "(0\<Colon>'b) \<le> k x - g x"
+ hence F2: "max (0\<Colon>'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2)
+ have F3: "\<forall>x\<^isub>1\<Colon>'b. x\<^isub>1 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_le_iff le_less)
+ have "\<forall>(x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>2 \<or> max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>1" by (metis le_less le_max_iff_disj)
+ hence "\<forall>(x\<^isub>3\<Colon>'b) (x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. x\<^isub>1 - x\<^isub>2 \<le> x\<^isub>3 - x\<^isub>2 \<or> x\<^isub>3 \<le> x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE)
+ hence "k x - g x \<le> f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute)
+ hence "k x - g x \<le> \<bar>f x - g x\<bar>" by (metis F3 le_max_iff_disj min_max.sup_absorb2)
+ thus "max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>" by (metis F2 min_max.sup_commute)
next
show "\<And>x\<Colon>'a.
\<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>
--- a/src/HOL/Metis_Examples/set.thy Fri Jun 04 19:36:41 2010 +0200
+++ b/src/HOL/Metis_Examples/set.thy Sat Jun 05 07:52:45 2010 +0200
@@ -21,242 +21,164 @@
(*multiple versions of this example*)
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
-proof (neg_clausify)
-fix x
-assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
-assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
-assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
-have 6: "sup Y Z = X \<or> Y \<subseteq> X"
- by (metis 0)
-have 7: "sup Y Z = X \<or> Z \<subseteq> X"
- by (metis 1)
-have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
- by (metis 5)
-have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 2)
-have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 3)
-have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 4)
-have 12: "Z \<subseteq> X"
- by (metis Un_upper2 7)
-have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
- by (metis 8 Un_upper2)
-have 14: "Y \<subseteq> X"
- by (metis Un_upper1 6)
-have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 10 12)
-have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 9 12)
-have 17: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
- by (metis 11 12)
-have 18: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x"
- by (metis 17 14)
-have 19: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 15 14)
-have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 16 14)
-have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
- by (metis 13 Un_upper1)
-have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
- by (metis equalityI 21)
-have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 22 Un_least)
-have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
- by (metis 23 12)
-have 25: "sup Y Z = X"
- by (metis 24 14)
-have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
- by (metis Un_least 25)
-have 27: "Y \<subseteq> x"
- by (metis 20 25)
-have 28: "Z \<subseteq> x"
- by (metis 19 25)
-have 29: "\<not> X \<subseteq> x"
- by (metis 18 25)
-have 30: "X \<subseteq> x \<or> \<not> Y \<subseteq> x"
- by (metis 26 28)
-have 31: "X \<subseteq> x"
- by (metis 30 27)
-show "False"
- by (metis 31 29)
+proof -
+ have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>1 \<union> x\<^isub>2" by (metis Un_commute Un_upper2)
+ have F2a: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq)
+ have F2: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis F2a subset_Un_eq)
+ { assume "\<not> Z \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ moreover
+ { assume AA1: "Y \<union> Z \<noteq> X"
+ { assume "\<not> Y \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
+ moreover
+ { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
+ { assume "\<not> Z \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ moreover
+ { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
+ hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff)
+ hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2)
+ hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1)
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1) }
+ moreover
+ { assume "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
+ { assume "\<not> Y \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
+ moreover
+ { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
+ { assume "\<not> Z \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ moreover
+ { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
+ hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff)
+ hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2)
+ hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1)
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by blast }
+ moreover
+ { assume "\<not> Y \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
+ ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
qed
sledgehammer_params [isar_proof, isar_shrink_factor = 2]
lemma (*equal_union: *)
- "(X = Y \<union> Z) =
- (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
-proof (neg_clausify)
-fix x
-assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
-assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
-assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
-have 6: "sup Y Z = X \<or> Y \<subseteq> X"
- by (metis 0)
-have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 2)
-have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 4)
-have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
- by (metis 5 Un_upper2)
-have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 3 Un_upper2)
-have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
- by (metis 8 Un_upper2)
-have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 10 Un_upper1)
-have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
- by (metis 9 Un_upper1)
-have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
- by (metis equalityI 13 Un_least)
-have 15: "sup Y Z = X"
- by (metis 14 1 6)
-have 16: "Y \<subseteq> x"
- by (metis 7 Un_upper2 Un_upper1 15)
-have 17: "\<not> X \<subseteq> x"
- by (metis 11 Un_upper1 15)
-have 18: "X \<subseteq> x"
- by (metis Un_least 15 12 15 16)
-show "False"
- by (metis 18 17)
+ "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
+proof -
+ have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq)
+ { assume AA1: "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
+ { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
+ { assume "\<not> Z \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ moreover
+ { assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z"
+ hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1 Un_commute Un_upper2)
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1 Un_subset_iff) }
+ moreover
+ { assume "\<not> Y \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) }
+ moreover
+ { assume "\<not> Z \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ moreover
+ { assume "\<not> Y \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
+ moreover
+ { assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
+ { assume "\<not> Z \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ moreover
+ { assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z"
+ hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1 Un_commute Un_upper2)
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) }
+ ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
qed
sledgehammer_params [isar_proof, isar_shrink_factor = 3]
lemma (*equal_union: *)
- "(X = Y \<union> Z) =
- (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
-proof (neg_clausify)
-fix x
-assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
-assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
-assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
-have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 3)
-have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
- by (metis 5 Un_upper2)
-have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 2 Un_upper2)
-have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 6 Un_upper2 Un_upper1)
-have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
- by (metis equalityI 7 Un_upper1)
-have 11: "sup Y Z = X"
- by (metis 10 Un_least 1 0)
-have 12: "Z \<subseteq> x"
- by (metis 9 11)
-have 13: "X \<subseteq> x"
- by (metis Un_least 11 12 8 Un_upper1 11)
-show "False"
- by (metis 13 4 Un_upper2 Un_upper1 11)
+ "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
+proof -
+ have F1a: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq)
+ have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis F1a subset_Un_eq)
+ { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) }
+ moreover
+ { assume AA1: "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
+ { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) }
+ ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
qed
-(*Example included in TPHOLs paper*)
-
sledgehammer_params [isar_proof, isar_shrink_factor = 4]
lemma (*equal_union: *)
- "(X = Y \<union> Z) =
- (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
-proof (neg_clausify)
-fix x
-assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
-assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
-assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
-have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 4)
-have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 3 Un_upper2)
-have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 7 Un_upper1)
-have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
- by (metis equalityI 5 Un_upper2 Un_upper1 Un_least)
-have 10: "Y \<subseteq> x"
- by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
-have 11: "X \<subseteq> x"
- by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10)
-show "False"
- by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
-qed
+ "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
+proof -
+ have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq)
+ { assume "\<not> Y \<subseteq> X"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
+ moreover
+ { assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
+ { assume "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) }
+ ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
+qed
-declare [[ atp_problem_prefix = "set__equal_union" ]]
+sledgehammer_params [isar_proof, isar_shrink_factor = 1]
+
lemma (*equal_union: *)
- "(X = Y \<union> Z) =
- (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
-(*One shot proof: hand-reduced. Metis can't do the full proof any more.*)
+ "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
+lemma "(X = Y \<inter> Z) = (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
+by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym)
-declare [[ atp_problem_prefix = "set__equal_inter" ]]
-lemma "(X = Y \<inter> Z) =
- (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
-by (metis Int_greatest Int_lower1 Int_lower2 set_eq_subset)
-
-declare [[ atp_problem_prefix = "set__fixedpoint" ]]
-lemma fixedpoint:
- "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
+lemma fixedpoint: "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
by metis
-lemma (*fixedpoint:*)
- "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
-proof (neg_clausify)
-fix x xa
-assume 0: "f (g x) = x"
-assume 1: "\<And>y. y = x \<or> f (g y) \<noteq> y"
-assume 2: "\<And>x. g (f (xa x)) = xa x \<or> g (f x) \<noteq> x"
-assume 3: "\<And>x. g (f x) \<noteq> x \<or> xa x \<noteq> x"
-have 4: "\<And>X1. g (f X1) \<noteq> X1 \<or> g x \<noteq> X1"
- by (metis 3 1 2)
-show "False"
- by (metis 4 0)
+lemma (* fixedpoint: *) "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
+proof -
+ assume "\<exists>!x\<Colon>'a. f (g x) = x"
+ thus "\<exists>!y\<Colon>'b. g (f y) = y" by metis
qed
-declare [[ atp_problem_prefix = "set__singleton_example" ]]
-lemma (*singleton_example_2:*)
+lemma (* singleton_example_2: *)
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
by (metis Set.subsetI Union_upper insertCI set_eq_subset)
- --{*found by SPASS*}
-lemma (*singleton_example_2:*)
+lemma (* singleton_example_2: *)
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
lemma singleton_example_2:
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-proof (neg_clausify)
-assume 0: "\<And>x. \<not> S \<subseteq> {x}"
-assume 1: "\<And>x. x \<notin> S \<or> \<Union>S \<subseteq> x"
-have 2: "\<And>X3. X3 = \<Union>S \<or> \<not> X3 \<subseteq> \<Union>S \<or> X3 \<notin> S"
- by (metis set_eq_subset 1)
-have 3: "\<And>X3. S \<subseteq> insert (\<Union>S) X3"
- by (metis insert_iff Set.subsetI Union_upper 2 Set.subsetI)
-show "False"
- by (metis 3 0)
+proof -
+ assume "\<forall>x \<in> S. \<Union>S \<subseteq> x"
+ hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> \<Union>S \<and> x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis set_eq_subset)
+ hence "\<forall>x\<^isub>1. x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis Union_upper)
+ hence "\<forall>x\<^isub>1\<Colon>('a \<Rightarrow> bool) \<Rightarrow> bool. \<Union>S \<in> x\<^isub>1 \<longrightarrow> S \<subseteq> x\<^isub>1" by (metis subsetI)
+ hence "\<forall>x\<^isub>1\<Colon>('a \<Rightarrow> bool) \<Rightarrow> bool. S \<subseteq> insert (\<Union>S) x\<^isub>1" by (metis insert_iff)
+ thus "\<exists>z. S \<subseteq> {z}" by metis
qed
-
-
text {*
From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
293-314.
*}
-declare [[ atp_problem_prefix = "set__Bledsoe_Fung" ]]
-(*Notes: 1, the numbering doesn't completely agree with the paper.
-2, we must rename set variables to avoid type clashes.*)
+(* Notes: (1) The numbering doesn't completely agree with the paper.
+ (2) We must rename set variables to avoid type clashes. *)
lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"
"D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
"P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
@@ -265,13 +187,13 @@
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
"\<exists>A. a \<notin> A"
"(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m"
-apply (metis all_not_in_conv)+
-apply (metis mem_def)
-apply (metis insertCI singletonE zless_le)
-apply (metis Collect_def Collect_mem_eq)
-apply (metis Collect_def Collect_mem_eq)
-apply (metis DiffE)
-apply (metis pair_in_Id_conv)
-done
+ apply (metis all_not_in_conv)
+ apply (metis all_not_in_conv)
+ apply (metis mem_def)
+ apply (metis less_int_def singleton_iff)
+ apply (metis mem_def)
+ apply (metis mem_def)
+ apply (metis all_not_in_conv)
+by (metis pair_in_Id_conv)
end
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jun 04 19:36:41 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Sat Jun 05 07:52:45 2010 +0200
@@ -275,6 +275,7 @@
("% SZS output start Refutation", "% SZS output end Refutation")],
known_failures =
[(Unprovable, "Satisfiability detected"),
+ (Unprovable, "UNPROVABLE"),
(OutOfResources, "CANNOT PROVE"),
(OutOfResources, "Refutation not found")],
max_axiom_clauses = 60,
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 04 19:36:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat Jun 05 07:52:45 2010 +0200
@@ -409,9 +409,10 @@
(substs' |> map (fn (x, y) =>
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
Syntax.string_of_term ctxt (term_of y)))));
- in cterm_instantiate substs' i_th
- handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
- end;
+ in cterm_instantiate substs' i_th end
+ handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
+ | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
+ "\n(Perhaps you want to try \"metisFT\".)")
(* INFERENCE RULE: RESOLVE *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 04 19:36:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Jun 05 07:52:45 2010 +0200
@@ -457,7 +457,7 @@
end;
-val suppress_endtheory = Unsynchronized.ref false;
+val suppress_endtheory = Unsynchronized.ref false
fun clause_cache_endtheory thy =
if ! suppress_endtheory then NONE
@@ -478,21 +478,18 @@
(*** Converting a subgoal into negated conjecture clauses. ***)
fun neg_skolemize_tac ctxt =
- EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
-
-fun neg_skolemize_tac ctxt =
- EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
+ EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
val neg_clausify =
single #> Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf
fun neg_conjecture_clauses ctxt st0 n =
let
- val st = Seq.hd (neg_skolemize_tac ctxt n st0)
- val ({params, prems, ...}, _) = Subgoal.focus (Variable.set_body false ctxt) n st
- in
- (map neg_clausify prems, map (Term.dest_Free o Thm.term_of o #2) params)
- end
+ (* "Option" is thrown if the assumptions contain schematic variables. *)
+ val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
+ val ({params, prems, ...}, _) =
+ Subgoal.focus (Variable.set_body false ctxt) n st
+ in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
(*Conversion of a subgoal to conjecture clauses. Each clause has
leading !!-bound universal variables, to express generality. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 04 19:36:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Jun 05 07:52:45 2010 +0200
@@ -28,8 +28,11 @@
val neg_clausify_setup =
Method.setup @{binding neg_clausify}
- (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
- "conversion of goal to negated conjecture clauses"
+ (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac)
+ o tap (fn _ => legacy_feature "Old 'neg_clausify' method -- \
+ \rerun Sledgehammer to obtain a direct \
+ \proof"))
+ "conversion of goal to negated conjecture clauses (legacy)"
(** Attribute for converting a theorem into clauses **)
@@ -41,7 +44,9 @@
end))
val clausify_setup =
- Attrib.setup @{binding clausify} parse_clausify_attribute
+ Attrib.setup @{binding clausify}
+ (parse_clausify_attribute
+ o tap (fn _ => legacy_feature "Old 'clausify' attribute"))
"conversion of theorem to clauses"
(** Sledgehammer commands **)
@@ -226,7 +231,7 @@
let
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
- val _ = kill_atps () (* race w.r.t. other Sledgehammer invocations *)
+ val _ = kill_atps ()
val _ = priority "Sledgehammering..."
val _ = app (start_prover_thread params birth_time death_time i n
relevance_override minimize_command
@@ -249,8 +254,10 @@
in
case subgoal_count state of
0 => priority "No subgoal!"
- | n => priority (#2 (minimize_theorems (get_params thy override_params) i n
- state name_thms_pairs))
+ | n =>
+ (kill_atps ();
+ priority (#2 (minimize_theorems (get_params thy override_params) i n
+ state name_thms_pairs)))
end
val sledgehammerN = "sledgehammer"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jun 04 19:36:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sat Jun 05 07:52:45 2010 +0200
@@ -487,8 +487,8 @@
fun decode_lines ctxt full_types tfrees lines =
fst (fold_map (decode_line full_types tfrees) lines ctxt)
-fun aint_inference _ (Definition _) = true
- | aint_inference t (Inference (_, t', _)) = not (t aconv t')
+fun aint_actual_inference _ (Definition _) = true
+ | aint_actual_inference t (Inference (_, t', _)) = not (t aconv t')
(* No "real" literals means only type information (tfree_tcs, clsrel, or
clsarity). *)
@@ -510,7 +510,7 @@
if is_only_type_information t then
map (replace_deps_in_line (num, [])) lines
(* Is there a repetition? If so, replace later line by earlier one. *)
- else case take_prefix (aint_inference t) lines of
+ else case take_prefix (aint_actual_inference t) lines of
(_, []) => lines (*no repetition of proof line*)
| (pre, Inference (num', _, _) :: post) =>
pre @ map (replace_deps_in_line (num', [num])) post
@@ -523,7 +523,7 @@
if is_only_type_information t then
Inference (num, t, deps) :: lines
(* Is there a repetition? If so, replace later line by earlier one. *)
- else case take_prefix (aint_inference t) lines of
+ else case take_prefix (aint_actual_inference t) lines of
(* FIXME: Doesn't this code risk conflating proofs involving different
types?? *)
(_, []) => Inference (num, t, deps) :: lines
@@ -539,8 +539,8 @@
and delete_dep num lines =
fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
-(* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly,
- removing the offending lines often does the trick. *)
+(* ATPs sometimes reuse free variable names in the strangest ways. Removing
+ offending lines often does the trick. *)
fun is_bad_free frees (Free x) = not (member (op =) frees x)
| is_bad_free _ _ = false
@@ -549,8 +549,8 @@
$ t1 $ t2)) = (t1 aconv t2)
| is_trivial_formula t = false
-fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
- (j, line :: lines)
+fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
+ (j, line :: map (replace_deps_in_line (num, [])) lines)
| add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
(Inference (num, t, deps)) (j, lines) =
(j + 1,
@@ -639,6 +639,9 @@
fun smart_case_split [] facts = ByMetis facts
| smart_case_split proofs facts = CaseSplit (proofs, facts)
+val indent_size = 2
+val no_label = ("", ~1)
+
val raw_prefix = "X"
val assum_prefix = "A"
val fact_prefix = "F"
@@ -677,16 +680,12 @@
map2 (step_for_line thm_names) (length lines downto 1) lines
end
-val indent_size = 2
-val no_label = ("", ~1)
-
-fun no_show qs = not (member (op =) qs Show)
-
(* When redirecting proofs, we keep information about the labels seen so far in
the "backpatches" data structure. The first component indicates which facts
should be associated with forthcoming proof steps. The second component is a
- pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and
- "drop_ls" are those that should be dropped in a case split. *)
+ pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
+ become assumptions and "drop_ls" are the labels that should be dropped in a
+ case split. *)
type backpatches = (label * facts) list * (label list * label list)
fun used_labels_of_step (Have (_, _, _, by)) =
@@ -731,8 +730,15 @@
fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
let
+ (* The first pass outputs those steps that are independent of the negated
+ conjecture. The second pass flips the proof by contradiction to obtain a
+ direct proof, introducing case splits when an inference depends on
+ several facts that depend on the negated conjecture. *)
+ fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
- fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
+ val canonicalize_labels =
+ map (fn l => if member (op =) concl_ls l then hd concl_ls else l)
+ #> distinct (op =)
fun first_pass ([], contra) = ([], contra)
| first_pass ((step as Fix _) :: proof, contra) =
first_pass (proof, contra) |>> cons step
@@ -740,15 +746,19 @@
first_pass (proof, contra) |>> cons step
| first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
if member (op =) concl_ls l then
- first_pass (proof, contra ||> cons step)
+ first_pass (proof, contra ||> l = hd concl_ls ? cons step)
else
first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
- | first_pass ((step as Have (qs, l, t, ByMetis (ls, ss))) :: proof,
- contra) =
- if exists (member (op =) (fst contra)) ls then
- first_pass (proof, contra |>> cons l ||> cons step)
- else
- first_pass (proof, contra) |>> cons step
+ | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
+ let
+ val ls = canonicalize_labels ls
+ val step = Have (qs, l, t, ByMetis (ls, ss))
+ in
+ if exists (member (op =) (fst contra)) ls then
+ first_pass (proof, contra |>> cons l ||> cons step)
+ else
+ first_pass (proof, contra) |>> cons step
+ end
| first_pass _ = raise Fail "malformed proof"
val (proof_top, (contra_ls, contra_proof)) =
first_pass (proof, (concl_ls, []))
@@ -756,23 +766,23 @@
fun backpatch_labels patches ls =
fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
fun second_pass end_qs ([], assums, patches) =
- ([Have (end_qs, no_label,
- if length assums < length concl_ls then
- clause_for_literals thy (map (negate_term thy o fst) assums)
- else
- concl_t,
+ ([Have (end_qs, no_label, concl_t,
ByMetis (backpatch_labels patches (map snd assums)))], patches)
| second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
second_pass end_qs (proof, (t, l) :: assums, patches)
| second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
patches) =
if member (op =) (snd (snd patches)) l andalso
+ not (member (op =) (fst (snd patches)) l) andalso
not (AList.defined (op =) (fst patches) l) then
second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
else
(case List.partition (member (op =) contra_ls) ls of
([contra_l], co_ls) =>
- if no_show qs then
+ if member (op =) qs Show then
+ second_pass end_qs (proof, assums,
+ patches |>> cons (contra_l, (co_ls, ss)))
+ else
second_pass end_qs
(proof, assums,
patches |>> cons (contra_l, (l :: co_ls, ss)))
@@ -781,9 +791,6 @@
else
Have (qs, l, negate_term thy t,
ByMetis (backpatch_label patches l)))
- else
- second_pass end_qs (proof, assums,
- patches |>> cons (contra_l, (co_ls, ss)))
| (contra_ls as _ :: _, co_ls) =>
let
val proofs =
@@ -801,7 +808,11 @@
||> apsnd (union (op =) drop_ls))
|> fst |> SOME
end) contra_ls
- val facts = (co_ls, [])
+ val (assumes, facts) =
+ if member (op =) (fst (snd patches)) l then
+ ([Assume (l, negate_term thy t)], (l :: co_ls, ss))
+ else
+ ([], (co_ls, ss))
in
(case join_proofs proofs of
SOME (l, t, proofs, proof_tail) =>
@@ -812,6 +823,7 @@
[Have (case_split_qualifiers proofs @ end_qs, no_label,
concl_t, smart_case_split proofs facts)],
patches)
+ |>> append assumes
end
| _ => raise Fail "malformed proof")
| second_pass _ _ = raise Fail "malformed proof"
@@ -914,9 +926,11 @@
fun string_for_proof ctxt i n =
let
- fun fix_print_mode f =
- Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ())) f
+ fun fix_print_mode f x =
+ setmp_CRITICAL show_no_free_types true
+ (setmp_CRITICAL show_types true
+ (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ())) f)) x
fun do_indent ind = replicate_string (ind * indent_size) " "
fun do_free (s, T) =
maybe_quote s ^ " :: " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jun 04 19:36:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Jun 05 07:52:45 2010 +0200
@@ -91,7 +91,8 @@
end
val subscript = implode o map (prefix "\<^isub>") o explode
-val nat_subscript = subscript o string_of_int
+fun nat_subscript n =
+ n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
fun plain_string_from_xml_tree t =
Buffer.empty |> XML.add_content t |> Buffer.content
--- a/src/Pure/Isar/expression.ML Fri Jun 04 19:36:41 2010 +0200
+++ b/src/Pure/Isar/expression.ML Sat Jun 05 07:52:45 2010 +0200
@@ -732,18 +732,20 @@
prep_decl raw_import I raw_body (ProofContext.init_global thy);
val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
+ val extraTs =
+ subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
+ val _ =
+ if null extraTs then ()
+ else warning ("Additional type variable(s) in locale specification " ^
+ quote (Binding.str_of binding) ^ ": " ^
+ commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
+
val predicate_binding =
if Binding.is_empty raw_predicate_binding then binding
else raw_predicate_binding;
val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
define_preds predicate_binding parms text thy;
- val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
- val _ =
- if null extraTs then ()
- else warning ("Additional type variable(s) in locale specification " ^
- quote (Binding.str_of binding));
-
val a_satisfy = Element.satisfy_morphism a_axioms;
val b_satisfy = Element.satisfy_morphism b_axioms;
--- a/src/Pure/Isar/theory_target.ML Fri Jun 04 19:36:41 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML Sat Jun 05 07:52:45 2010 +0200
@@ -180,13 +180,35 @@
end;
-(* consts *)
+(* mixfix notation *)
+
+local
fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
if not is_locale then (NoSyn, NoSyn, mx)
else if not is_class then (NoSyn, mx, NoSyn)
else (mx, NoSyn, NoSyn);
+in
+
+fun prep_mixfix ctxt ta (b, extra_tfrees) mx =
+ let
+ val mx' =
+ if null extra_tfrees then mx
+ else
+ (warning
+ ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
+ commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
+ (if mx = NoSyn then ""
+ else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx)));
+ NoSyn);
+ in fork_mixfix ta mx' end;
+
+end;
+
+
+(* consts *)
+
fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
let
val b' = Morphism.binding phi b;
@@ -218,10 +240,14 @@
val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
val target_ctxt = Local_Theory.target_of lthy;
- val (mx1, mx2, mx3) = fork_mixfix ta mx;
val t' = Assumption.export_term lthy target_ctxt t;
val xs = map Free (rev (Variable.add_fixed target_ctxt t' []));
val u = fold_rev lambda xs t';
+
+ val extra_tfrees =
+ subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+ val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
+
val global_rhs =
singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
in
@@ -261,7 +287,7 @@
val params = type_params @ term_params;
val U = map Term.fastype_of params ---> T;
- val (mx1, mx2, mx3) = fork_mixfix ta mx;
+ val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
val (const, lthy') = lthy |>
(case Class_Target.instantiation_param lthy b of
SOME c' =>
@@ -299,10 +325,7 @@
val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
val T = Term.fastype_of rhs;
val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
- val extra_tfrees =
- fold_types (fold_atyps
- (fn TFree v => if member (op =) tfreesT v then I else insert (op =) v | _ => I)) rhs []
- |> sort_wrt #1;
+ val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
(*const*)
val ((lhs, local_def), lthy2) = lthy |> declare_const ta extra_tfrees xs ((b, T), mx);
--- a/src/Pure/old_goals.ML Fri Jun 04 19:36:41 2010 +0200
+++ b/src/Pure/old_goals.ML Sat Jun 05 07:52:45 2010 +0200
@@ -189,28 +189,28 @@
local
-fun print_vars_terms thy (n,thm) =
+fun print_vars_terms n thm =
let
- fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
- fun find_vars thy (Const (c, ty)) =
+ val thy = theory_of_thm thm
+ fun typed s ty =
+ " " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
+ fun find_vars (Const (c, ty)) =
if null (Term.add_tvarsT ty []) then I
- else insert (op =) (c ^ typed ty)
- | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
- | find_vars _ (Free _) = I
- | find_vars _ (Bound _) = I
- | find_vars thy (Abs (_, _, t)) = find_vars thy t
- | find_vars thy (t1 $ t2) =
- find_vars thy t1 #> find_vars thy t1;
+ else insert (op =) (typed c ty)
+ | find_vars (Var (xi, ty)) =
+ insert (op =) (typed (Term.string_of_vname xi) ty)
+ | find_vars (Free _) = I
+ | find_vars (Bound _) = I
+ | find_vars (Abs (_, _, t)) = find_vars t
+ | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
val prem = Logic.nth_prem (n, Thm.prop_of thm)
- val tms = find_vars thy prem []
- in
- (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
- end;
+ val tms = find_vars prem []
+ in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
in
fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
- handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
+ handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
end;