# HG changeset patch # User haftmann # Date 1251991570 -7200 # Node ID 94f61caa546e2020d71b87a4e66291cffdc58fec # Parent 9da37876874db290f5da2c01ee339a4557d3fe0c# Parent d14762642cdde6cecadfb8473143994d787a1a70 merged diff -r d14762642cdd -r 94f61caa546e Admin/isatest/isatest-makeall --- a/Admin/isatest/isatest-makeall Thu Sep 03 15:39:02 2009 +0200 +++ b/Admin/isatest/isatest-makeall Thu Sep 03 17:26:10 2009 +0200 @@ -10,6 +10,8 @@ # max time until test is aborted (in sec) MAXTIME=28800 +PUBLISH_TEST=/home/isabelle-repository/repos/testtool/publish_test.py + ## diagnostics PRG="$(basename "$0")" @@ -120,6 +122,8 @@ TOOL="$ISABELLE_TOOL makeall $MFLAGS all" fi +IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT") + # main test loop log "starting [$@]" @@ -159,10 +163,16 @@ then # test log and cleanup echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 + if [ -x $PUBLISH_TEST ]; then + $PUBLISH_TEST -r $IDENT -s "SUCCESS" -a log $TESTLOG + fi gzip -f $TESTLOG else # test log echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 + if [ -x $PUBLISH_TEST ]; then + $PUBLISH_TEST -r $IDENT -s "FAIL" -a log $TESTLOG + fi # error log echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG diff -r d14762642cdd -r 94f61caa546e etc/components --- a/etc/components Thu Sep 03 15:39:02 2009 +0200 +++ b/etc/components Thu Sep 03 17:26:10 2009 +0200 @@ -13,5 +13,5 @@ #misc components src/Tools/Code src/HOL/Tools/ATP_Manager -src/HOL/Tools/Mirabelle +src/HOL/Mirabelle src/HOL/Library/Sum_Of_Squares diff -r d14762642cdd -r 94f61caa546e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Sep 03 15:39:02 2009 +0200 +++ b/src/HOL/IsaMakefile Thu Sep 03 17:26:10 2009 +0200 @@ -31,6 +31,7 @@ HOL-Matrix \ HOL-MetisExamples \ HOL-MicroJava \ + HOL-Mirabelle \ HOL-Modelcheck \ HOL-NanoJava \ HOL-Nominal-Examples \ @@ -940,7 +941,7 @@ HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz -$(LOG)/HOL-Matrix.gz: $(OUT)/HOL \ +$(LOG)/HOL-Matrix.gz: $(OUT)/HOL \ $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \ $(SRC)/Tools/Compute_Oracle/am_compiler.ML \ $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \ @@ -948,8 +949,8 @@ $(SRC)/Tools/Compute_Oracle/linker.ML \ $(SRC)/Tools/Compute_Oracle/am_ghc.ML \ $(SRC)/Tools/Compute_Oracle/am_sml.ML \ - $(SRC)/Tools/Compute_Oracle/compute.ML \ - Tools/ComputeFloat.thy Tools/float_arith.ML \ + $(SRC)/Tools/Compute_Oracle/compute.ML Matrix/ComputeFloat.thy \ + Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy Tools/float_arith.ML \ Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \ Matrix/document/root.tex Matrix/ROOT.ML Matrix/cplex/Cplex.thy \ Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML \ @@ -1119,6 +1120,20 @@ @cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples +## HOL-Mirabelle + +HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz + +$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/MirabelleTest.thy \ + Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML Mirabelle/ROOT.ML \ + Mirabelle/Tools/mirabelle_arith.ML \ + Mirabelle/Tools/mirabelle_metis.ML \ + Mirabelle/Tools/mirabelle_quickcheck.ML \ + Mirabelle/Tools/mirabelle_refute.ML \ + Mirabelle/Tools/mirabelle_sledgehammer.ML + @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle + + ## clean clean: @@ -1140,4 +1155,5 @@ $(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz \ $(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz \ $(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA \ - $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz + $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz \ + $(LOG)/HOL-Mirabelle.gz diff -r d14762642cdd -r 94f61caa546e src/HOL/Matrix/ComputeFloat.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Matrix/ComputeFloat.thy Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,568 @@ +(* Title: HOL/Tools/ComputeFloat.thy + Author: Steven Obua +*) + +header {* Floating Point Representation of the Reals *} + +theory ComputeFloat +imports Complex_Main +uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML") +begin + +definition + pow2 :: "int \ real" where + "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))" + +definition + float :: "int * int \ real" where + "float x = real (fst x) * pow2 (snd x)" + +lemma pow2_0[simp]: "pow2 0 = 1" +by (simp add: pow2_def) + +lemma pow2_1[simp]: "pow2 1 = 2" +by (simp add: pow2_def) + +lemma pow2_neg: "pow2 x = inverse (pow2 (-x))" +by (simp add: pow2_def) + +lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)" +proof - + have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith + have g: "! a b. a - -1 = a + (1::int)" by arith + have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)" + apply (auto, induct_tac n) + apply (simp_all add: pow2_def) + apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if]) + by (auto simp add: h) + show ?thesis + proof (induct a) + case (1 n) + from pos show ?case by (simp add: algebra_simps) + next + case (2 n) + show ?case + apply (auto) + apply (subst pow2_neg[of "- int n"]) + apply (subst pow2_neg[of "-1 - int n"]) + apply (auto simp add: g pos) + done + qed +qed + +lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)" +proof (induct b) + case (1 n) + show ?case + proof (induct n) + case 0 + show ?case by simp + next + case (Suc m) + show ?case by (auto simp add: algebra_simps pow2_add1 prems) + qed +next + case (2 n) + show ?case + proof (induct n) + case 0 + show ?case + apply (auto) + apply (subst pow2_neg[of "a + -1"]) + apply (subst pow2_neg[of "-1"]) + apply (simp) + apply (insert pow2_add1[of "-a"]) + apply (simp add: algebra_simps) + apply (subst pow2_neg[of "-a"]) + apply (simp) + done + case (Suc m) + have a: "int m - (a + -2) = 1 + (int m - a + 1)" by arith + have b: "int m - -2 = 1 + (int m + 1)" by arith + show ?case + apply (auto) + apply (subst pow2_neg[of "a + (-2 - int m)"]) + apply (subst pow2_neg[of "-2 - int m"]) + apply (auto simp add: algebra_simps) + apply (subst a) + apply (subst b) + apply (simp only: pow2_add1) + apply (subst pow2_neg[of "int m - a + 1"]) + apply (subst pow2_neg[of "int m + 1"]) + apply auto + apply (insert prems) + apply (auto simp add: algebra_simps) + done + qed +qed + +lemma "float (a, e) + float (b, e) = float (a + b, e)" +by (simp add: float_def algebra_simps) + +definition + int_of_real :: "real \ int" where + "int_of_real x = (SOME y. real y = x)" + +definition + real_is_int :: "real \ bool" where + "real_is_int x = (EX (u::int). x = real u)" + +lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))" +by (auto simp add: real_is_int_def int_of_real_def) + +lemma float_transfer: "real_is_int ((real a)*(pow2 c)) \ float (a, b) = float (int_of_real ((real a)*(pow2 c)), b - c)" +by (simp add: float_def real_is_int_def2 pow2_add[symmetric]) + +lemma pow2_int: "pow2 (int c) = 2^c" +by (simp add: pow2_def) + +lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)" +by (simp add: float_def pow2_int[symmetric] pow2_add[symmetric]) + +lemma real_is_int_real[simp]: "real_is_int (real (x::int))" +by (auto simp add: real_is_int_def int_of_real_def) + +lemma int_of_real_real[simp]: "int_of_real (real x) = x" +by (simp add: int_of_real_def) + +lemma real_int_of_real[simp]: "real_is_int x \ real (int_of_real x) = x" +by (auto simp add: int_of_real_def real_is_int_def) + +lemma real_is_int_add_int_of_real: "real_is_int a \ real_is_int b \ (int_of_real (a+b)) = (int_of_real a) + (int_of_real b)" +by (auto simp add: int_of_real_def real_is_int_def) + +lemma real_is_int_add[simp]: "real_is_int a \ real_is_int b \ real_is_int (a+b)" +apply (subst real_is_int_def2) +apply (simp add: real_is_int_add_int_of_real real_int_of_real) +done + +lemma int_of_real_sub: "real_is_int a \ real_is_int b \ (int_of_real (a-b)) = (int_of_real a) - (int_of_real b)" +by (auto simp add: int_of_real_def real_is_int_def) + +lemma real_is_int_sub[simp]: "real_is_int a \ real_is_int b \ real_is_int (a-b)" +apply (subst real_is_int_def2) +apply (simp add: int_of_real_sub real_int_of_real) +done + +lemma real_is_int_rep: "real_is_int x \ ?! (a::int). real a = x" +by (auto simp add: real_is_int_def) + +lemma int_of_real_mult: + assumes "real_is_int a" "real_is_int b" + shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)" +proof - + from prems have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto) + from prems have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto) + from a obtain a'::int where a':"a = real a'" by auto + from b obtain b'::int where b':"b = real b'" by auto + have r: "real a' * real b' = real (a' * b')" by auto + show ?thesis + apply (simp add: a' b') + apply (subst r) + apply (simp only: int_of_real_real) + done +qed + +lemma real_is_int_mult[simp]: "real_is_int a \ real_is_int b \ real_is_int (a*b)" +apply (subst real_is_int_def2) +apply (simp add: int_of_real_mult) +done + +lemma real_is_int_0[simp]: "real_is_int (0::real)" +by (simp add: real_is_int_def int_of_real_def) + +lemma real_is_int_1[simp]: "real_is_int (1::real)" +proof - + have "real_is_int (1::real) = real_is_int(real (1::int))" by auto + also have "\ = True" by (simp only: real_is_int_real) + ultimately show ?thesis by auto +qed + +lemma real_is_int_n1: "real_is_int (-1::real)" +proof - + have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto + also have "\ = True" by (simp only: real_is_int_real) + ultimately show ?thesis by auto +qed + +lemma real_is_int_number_of[simp]: "real_is_int ((number_of \ int \ real) x)" +proof - + have neg1: "real_is_int (-1::real)" + proof - + have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto + also have "\ = True" by (simp only: real_is_int_real) + ultimately show ?thesis by auto + qed + + { + fix x :: int + have "real_is_int ((number_of \ int \ real) x)" + unfolding number_of_eq + apply (induct x) + apply (induct_tac n) + apply (simp) + apply (simp) + apply (induct_tac n) + apply (simp add: neg1) + proof - + fix n :: nat + assume rn: "(real_is_int (of_int (- (int (Suc n)))))" + have s: "-(int (Suc (Suc n))) = -1 + - (int (Suc n))" by simp + show "real_is_int (of_int (- (int (Suc (Suc n)))))" + apply (simp only: s of_int_add) + apply (rule real_is_int_add) + apply (simp add: neg1) + apply (simp only: rn) + done + qed + } + note Abs_Bin = this + { + fix x :: int + have "? u. x = u" + apply (rule exI[where x = "x"]) + apply (simp) + done + } + then obtain u::int where "x = u" by auto + with Abs_Bin show ?thesis by auto +qed + +lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)" +by (simp add: int_of_real_def) + +lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)" +proof - + have 1: "(1::real) = real (1::int)" by auto + show ?thesis by (simp only: 1 int_of_real_real) +qed + +lemma int_of_real_number_of[simp]: "int_of_real (number_of b) = number_of b" +proof - + have "real_is_int (number_of b)" by simp + then have uu: "?! u::int. number_of b = real u" by (auto simp add: real_is_int_rep) + then obtain u::int where u:"number_of b = real u" by auto + have "number_of b = real ((number_of b)::int)" + by (simp add: number_of_eq real_of_int_def) + have ub: "number_of b = real ((number_of b)::int)" + by (simp add: number_of_eq real_of_int_def) + from uu u ub have unb: "u = number_of b" + by blast + have "int_of_real (number_of b) = u" by (simp add: u) + with unb show ?thesis by simp +qed + +lemma float_transfer_even: "even a \ float (a, b) = float (a div 2, b+1)" + apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified]) + apply (simp_all add: pow2_def even_def real_is_int_def algebra_simps) + apply (auto) +proof - + fix q::int + have a:"b - (-1\int) = (1\int) + b" by arith + show "(float (q, (b - (-1\int)))) = (float (q, ((1\int) + b)))" + by (simp add: a) +qed + +lemma int_div_zdiv: "int (a div b) = (int a) div (int b)" +by (rule zdiv_int) + +lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)" +by (rule zmod_int) + +lemma abs_div_2_less: "a \ 0 \ a \ -1 \ abs((a::int) div 2) < abs a" +by arith + +function norm_float :: "int \ int \ int \ int" where + "norm_float a b = (if a \ 0 \ even a then norm_float (a div 2) (b + 1) + else if a = 0 then (0, 0) else (a, b))" +by auto + +termination by (relation "measure (nat o abs o fst)") + (auto intro: abs_div_2_less) + +lemma norm_float: "float x = float (split norm_float x)" +proof - + { + fix a b :: int + have norm_float_pair: "float (a, b) = float (norm_float a b)" + proof (induct a b rule: norm_float.induct) + case (1 u v) + show ?case + proof cases + assume u: "u \ 0 \ even u" + with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto + with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even) + then show ?thesis + apply (subst norm_float.simps) + apply (simp add: ind) + done + next + assume "~(u \ 0 \ even u)" + then show ?thesis + by (simp add: prems float_def) + qed + qed + } + note helper = this + have "? a b. x = (a,b)" by auto + then obtain a b where "x = (a, b)" by blast + then show ?thesis by (simp add: helper) +qed + +lemma float_add_l0: "float (0, e) + x = x" + by (simp add: float_def) + +lemma float_add_r0: "x + float (0, e) = x" + by (simp add: float_def) + +lemma float_add: + "float (a1, e1) + float (a2, e2) = + (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1) + else float (a1*2^(nat (e1-e2))+a2, e2))" + apply (simp add: float_def algebra_simps) + apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric]) + done + +lemma float_add_assoc1: + "(x + float (y1, e1)) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x" + by simp + +lemma float_add_assoc2: + "(float (y1, e1) + x) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x" + by simp + +lemma float_add_assoc3: + "float (y1, e1) + (x + float (y2, e2)) = (float (y1, e1) + float (y2, e2)) + x" + by simp + +lemma float_add_assoc4: + "float (y1, e1) + (float (y2, e2) + x) = (float (y1, e1) + float (y2, e2)) + x" + by simp + +lemma float_mult_l0: "float (0, e) * x = float (0, 0)" + by (simp add: float_def) + +lemma float_mult_r0: "x * float (0, e) = float (0, 0)" + by (simp add: float_def) + +definition + lbound :: "real \ real" +where + "lbound x = min 0 x" + +definition + ubound :: "real \ real" +where + "ubound x = max 0 x" + +lemma lbound: "lbound x \ x" + by (simp add: lbound_def) + +lemma ubound: "x \ ubound x" + by (simp add: ubound_def) + +lemma float_mult: + "float (a1, e1) * float (a2, e2) = + (float (a1 * a2, e1 + e2))" + by (simp add: float_def pow2_add) + +lemma float_minus: + "- (float (a,b)) = float (-a, b)" + by (simp add: float_def) + +lemma zero_less_pow2: + "0 < pow2 x" +proof - + { + fix y + have "0 <= y \ 0 < pow2 y" + by (induct y, induct_tac n, simp_all add: pow2_add) + } + note helper=this + show ?thesis + apply (case_tac "0 <= x") + apply (simp add: helper) + apply (subst pow2_neg) + apply (simp add: helper) + done +qed + +lemma zero_le_float: + "(0 <= float (a,b)) = (0 <= a)" + apply (auto simp add: float_def) + apply (auto simp add: zero_le_mult_iff zero_less_pow2) + apply (insert zero_less_pow2[of b]) + apply (simp_all) + done + +lemma float_le_zero: + "(float (a,b) <= 0) = (a <= 0)" + apply (auto simp add: float_def) + apply (auto simp add: mult_le_0_iff) + apply (insert zero_less_pow2[of b]) + apply auto + done + +lemma float_abs: + "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))" + apply (auto simp add: abs_if) + apply (simp_all add: zero_le_float[symmetric, of a b] float_minus) + done + +lemma float_zero: + "float (0, b) = 0" + by (simp add: float_def) + +lemma float_pprt: + "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))" + by (auto simp add: zero_le_float float_le_zero float_zero) + +lemma pprt_lbound: "pprt (lbound x) = float (0, 0)" + apply (simp add: float_def) + apply (rule pprt_eq_0) + apply (simp add: lbound_def) + done + +lemma nprt_ubound: "nprt (ubound x) = float (0, 0)" + apply (simp add: float_def) + apply (rule nprt_eq_0) + apply (simp add: ubound_def) + done + +lemma float_nprt: + "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))" + by (auto simp add: zero_le_float float_le_zero float_zero) + +lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1" + by auto + +lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)" + by simp + +lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)" + by simp + +lemma mult_left_one: "1 * a = (a::'a::semiring_1)" + by simp + +lemma mult_right_one: "a * 1 = (a::'a::semiring_1)" + by simp + +lemma int_pow_0: "(a::int)^(Numeral0) = 1" + by simp + +lemma int_pow_1: "(a::int)^(Numeral1) = a" + by simp + +lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0" + by simp + +lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1" + by simp + +lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0" + by simp + +lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1" + by simp + +lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1" + by simp + +lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1" +proof - + have 1:"((-1)::nat) = 0" + by simp + show ?thesis by (simp add: 1) +qed + +lemma fst_cong: "a=a' \ fst (a,b) = fst (a',b)" + by simp + +lemma snd_cong: "b=b' \ snd (a,b) = snd (a,b')" + by simp + +lemma lift_bool: "x \ x=True" + by simp + +lemma nlift_bool: "~x \ x=False" + by simp + +lemma not_false_eq_true: "(~ False) = True" by simp + +lemma not_true_eq_false: "(~ True) = False" by simp + +lemmas binarith = + normalize_bin_simps + pred_bin_simps succ_bin_simps + add_bin_simps minus_bin_simps mult_bin_simps + +lemma int_eq_number_of_eq: + "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)" + by (rule eq_number_of_eq) + +lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" + by (simp only: iszero_number_of_Pls) + +lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))" + by simp + +lemma int_iszero_number_of_Bit0: "iszero ((number_of (Int.Bit0 w))::int) = iszero ((number_of w)::int)" + by simp + +lemma int_iszero_number_of_Bit1: "\ iszero ((number_of (Int.Bit1 w))::int)" + by simp + +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)" + unfolding neg_def number_of_is_id by simp + +lemma int_not_neg_number_of_Pls: "\ (neg (Numeral0::int))" + by simp + +lemma int_neg_number_of_Min: "neg (-1::int)" + by simp + +lemma int_neg_number_of_Bit0: "neg ((number_of (Int.Bit0 w))::int) = neg ((number_of w)::int)" + by simp + +lemma int_neg_number_of_Bit1: "neg ((number_of (Int.Bit1 w))::int) = neg ((number_of w)::int)" + by simp + +lemma int_le_number_of_eq: "(((number_of x)::int) \ number_of y) = (\ neg ((number_of (y + (uminus x)))::int))" + unfolding neg_def number_of_is_id by (simp add: not_less) + +lemmas intarithrel = + int_eq_number_of_eq + lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_Bit0 + lift_bool[OF int_iszero_number_of_Bit1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min] + int_neg_number_of_Bit0 int_neg_number_of_Bit1 int_le_number_of_eq + +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)" + by simp + +lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))" + by simp + +lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)" + by simp + +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)" + by simp + +lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym + +lemmas natarith = add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of + +lemmas powerarith = nat_number_of zpower_number_of_even + zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring] + zpower_Pls zpower_Min + +lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 + float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound + +(* for use with the compute oracle *) +lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false + +use "~~/src/HOL/Tools/float_arith.ML" + +end diff -r d14762642cdd -r 94f61caa546e src/HOL/Matrix/ComputeHOL.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Matrix/ComputeHOL.thy Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,191 @@ +theory ComputeHOL +imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle" +begin + +lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq) +lemma meta_eq_trivial: "x == y \ x == y" by simp +lemma meta_eq_imp_eq: "x == y \ x = y" by auto +lemma eq_trivial: "x = y \ x = y" by auto +lemma bool_to_true: "x :: bool \ x == True" by simp +lemma transmeta_1: "x = y \ y == z \ x = z" by simp +lemma transmeta_2: "x == y \ y = z \ x = z" by simp +lemma transmeta_3: "x == y \ y == z \ x = z" by simp + + +(**** compute_if ****) + +lemma If_True: "If True = (\ x y. x)" by ((rule ext)+,auto) +lemma If_False: "If False = (\ x y. y)" by ((rule ext)+, auto) + +lemmas compute_if = If_True If_False + +(**** compute_bool ****) + +lemma bool1: "(\ True) = False" by blast +lemma bool2: "(\ False) = True" by blast +lemma bool3: "(P \ True) = P" by blast +lemma bool4: "(True \ P) = P" by blast +lemma bool5: "(P \ False) = False" by blast +lemma bool6: "(False \ P) = False" by blast +lemma bool7: "(P \ True) = True" by blast +lemma bool8: "(True \ P) = True" by blast +lemma bool9: "(P \ False) = P" by blast +lemma bool10: "(False \ P) = P" by blast +lemma bool11: "(True \ P) = P" by blast +lemma bool12: "(P \ True) = True" by blast +lemma bool13: "(True \ P) = P" by blast +lemma bool14: "(P \ False) = (\ P)" by blast +lemma bool15: "(False \ P) = True" by blast +lemma bool16: "(False = False) = True" by blast +lemma bool17: "(True = True) = True" by blast +lemma bool18: "(False = True) = False" by blast +lemma bool19: "(True = False) = False" by blast + +lemmas compute_bool = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10 bool11 bool12 bool13 bool14 bool15 bool16 bool17 bool18 bool19 + + +(*** compute_pair ***) + +lemma compute_fst: "fst (x,y) = x" by simp +lemma compute_snd: "snd (x,y) = y" by simp +lemma compute_pair_eq: "((a, b) = (c, d)) = (a = c \ b = d)" by auto + +lemma prod_case_simp: "prod_case f (x,y) = f x y" by simp + +lemmas compute_pair = compute_fst compute_snd compute_pair_eq prod_case_simp + +(*** compute_option ***) + +lemma compute_the: "the (Some x) = x" by simp +lemma compute_None_Some_eq: "(None = Some x) = False" by auto +lemma compute_Some_None_eq: "(Some x = None) = False" by auto +lemma compute_None_None_eq: "(None = None) = True" by auto +lemma compute_Some_Some_eq: "(Some x = Some y) = (x = y)" by auto + +definition + option_case_compute :: "'b option \ 'a \ ('b \ 'a) \ 'a" +where + "option_case_compute opt a f = option_case a f opt" + +lemma option_case_compute: "option_case = (\ a f opt. option_case_compute opt a f)" + by (simp add: option_case_compute_def) + +lemma option_case_compute_None: "option_case_compute None = (\ a f. a)" + apply (rule ext)+ + apply (simp add: option_case_compute_def) + done + +lemma option_case_compute_Some: "option_case_compute (Some x) = (\ a f. f x)" + apply (rule ext)+ + apply (simp add: option_case_compute_def) + done + +lemmas compute_option_case = option_case_compute option_case_compute_None option_case_compute_Some + +lemmas compute_option = compute_the compute_None_Some_eq compute_Some_None_eq compute_None_None_eq compute_Some_Some_eq compute_option_case + +(**** compute_list_length ****) + +lemma length_cons:"length (x#xs) = 1 + (length xs)" + by simp + +lemma length_nil: "length [] = 0" + by simp + +lemmas compute_list_length = length_nil length_cons + +(*** compute_list_case ***) + +definition + list_case_compute :: "'b list \ 'a \ ('b \ 'b list \ 'a) \ 'a" +where + "list_case_compute l a f = list_case a f l" + +lemma list_case_compute: "list_case = (\ (a::'a) f (l::'b list). list_case_compute l a f)" + apply (rule ext)+ + apply (simp add: list_case_compute_def) + done + +lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\ (a::'a) f. a)" + apply (rule ext)+ + apply (simp add: list_case_compute_def) + done + +lemma list_case_compute_cons: "list_case_compute (u#v) = (\ (a::'a) f. (f (u::'b) v))" + apply (rule ext)+ + apply (simp add: list_case_compute_def) + done + +lemmas compute_list_case = list_case_compute list_case_compute_empty list_case_compute_cons + +(*** compute_list_nth ***) +(* Of course, you will need computation with nats for this to work \ *) + +lemma compute_list_nth: "((x#xs) ! n) = (if n = 0 then x else (xs ! (n - 1)))" + by (cases n, auto) + +(*** compute_list ***) + +lemmas compute_list = compute_list_case compute_list_length compute_list_nth + +(*** compute_let ***) + +lemmas compute_let = Let_def + +(***********************) +(* Everything together *) +(***********************) + +lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let + +ML {* +signature ComputeHOL = +sig + val prep_thms : thm list -> thm list + val to_meta_eq : thm -> thm + val to_hol_eq : thm -> thm + val symmetric : thm -> thm + val trans : thm -> thm -> thm +end + +structure ComputeHOL : ComputeHOL = +struct + +local +fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq)); +in +fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", []) + | rewrite_conv (eq :: eqs) ct = + Thm.instantiate (Thm.match (lhs_of eq, ct)) eq + handle Pattern.MATCH => rewrite_conv eqs ct; +end + +val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}]))) + +val eq_th = @{thm "HOL.eq_reflection"} +val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"} +val bool_to_true = @{thm "ComputeHOL.bool_to_true"} + +fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th] + +fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] + +fun prep_thms ths = map (convert_conditions o to_meta_eq) ths + +fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th] + +local + val trans_HOL = @{thm "HOL.trans"} + val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"} + val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"} + val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"} + fun tr [] th1 th2 = trans_HOL OF [th1, th2] + | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) +in + fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2 +end + +end +*} + +end diff -r d14762642cdd -r 94f61caa546e src/HOL/Matrix/ComputeNumeral.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Matrix/ComputeNumeral.thy Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,195 @@ +theory ComputeNumeral +imports ComputeHOL ComputeFloat +begin + +(* normalization of bit strings *) +lemmas bitnorm = normalize_bin_simps + +(* neg for bit strings *) +lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def) +lemma neg2: "neg Int.Min = True" apply (subst Int.Min_def) by auto +lemma neg3: "neg (Int.Bit0 x) = neg x" apply (simp add: neg_def) apply (subst Bit0_def) by auto +lemma neg4: "neg (Int.Bit1 x) = neg x" apply (simp add: neg_def) apply (subst Bit1_def) by auto +lemmas bitneg = neg1 neg2 neg3 neg4 + +(* iszero for bit strings *) +lemma iszero1: "iszero Int.Pls = True" by (simp add: Int.Pls_def iszero_def) +lemma iszero2: "iszero Int.Min = False" apply (subst Int.Min_def) apply (subst iszero_def) by simp +lemma iszero3: "iszero (Int.Bit0 x) = iszero x" apply (subst Int.Bit0_def) apply (subst iszero_def)+ by auto +lemma iszero4: "iszero (Int.Bit1 x) = False" apply (subst Int.Bit1_def) apply (subst iszero_def)+ apply simp by arith +lemmas bitiszero = iszero1 iszero2 iszero3 iszero4 + +(* lezero for bit strings *) +constdefs + "lezero x == (x \ 0)" +lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto +lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto +lemma lezero3: "lezero (Int.Bit0 x) = lezero x" unfolding Int.Bit0_def lezero_def by auto +lemma lezero4: "lezero (Int.Bit1 x) = neg x" unfolding Int.Bit1_def lezero_def neg_def by auto +lemmas bitlezero = lezero1 lezero2 lezero3 lezero4 + +(* equality for bit strings *) +lemmas biteq = eq_bin_simps + +(* x < y for bit strings *) +lemmas bitless = less_bin_simps + +(* x \ y for bit strings *) +lemmas bitle = le_bin_simps + +(* succ for bit strings *) +lemmas bitsucc = succ_bin_simps + +(* pred for bit strings *) +lemmas bitpred = pred_bin_simps + +(* unary minus for bit strings *) +lemmas bituminus = minus_bin_simps + +(* addition for bit strings *) +lemmas bitadd = add_bin_simps + +(* multiplication for bit strings *) +lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def) +lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min) +lemma multb0x: "(Int.Bit0 x) * y = Int.Bit0 (x * y)" by (rule mult_Bit0) +lemma multxb0: "x * (Int.Bit0 y) = Int.Bit0 (x * y)" unfolding Bit0_def by simp +lemma multb1: "(Int.Bit1 x) * (Int.Bit1 y) = Int.Bit1 (Int.Bit0 (x * y) + x + y)" + unfolding Bit0_def Bit1_def by (simp add: algebra_simps) +lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1 + +lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul + +constdefs + "nat_norm_number_of (x::nat) == x" + +lemma nat_norm_number_of: "nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)" + apply (simp add: nat_norm_number_of_def) + unfolding lezero_def iszero_def neg_def + apply (simp add: numeral_simps) + done + +(* Normalization of nat literals *) +lemma natnorm0: "(0::nat) = number_of (Int.Pls)" by auto +lemma natnorm1: "(1 :: nat) = number_of (Int.Bit1 Int.Pls)" by auto +lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of + +(* Suc *) +lemma natsuc: "Suc (number_of x) = (if neg x then 1 else number_of (Int.succ x))" by (auto simp add: number_of_is_id) + +(* Addition for nat *) +lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))" + unfolding nat_number_of_def number_of_is_id neg_def + by auto + +(* Subtraction for nat *) +lemma natsub: "(number_of x) - ((number_of y)::nat) = + (if neg x then 0 else (if neg y then number_of x else (nat_norm_number_of (number_of (x + (- y))))))" + unfolding nat_norm_number_of + by (auto simp add: number_of_is_id neg_def lezero_def iszero_def Let_def nat_number_of_def) + +(* Multiplication for nat *) +lemma natmul: "(number_of x) * ((number_of y)::nat) = + (if neg x then 0 else (if neg y then 0 else number_of (x * y)))" + unfolding nat_number_of_def number_of_is_id neg_def + by (simp add: nat_mult_distrib) + +lemma nateq: "(((number_of x)::nat) = (number_of y)) = ((lezero x \ lezero y) \ (x = y))" + by (auto simp add: iszero_def lezero_def neg_def number_of_is_id) + +lemma natless: "(((number_of x)::nat) < (number_of y)) = ((x < y) \ (\ (lezero y)))" + by (simp add: lezero_def numeral_simps not_le) + +lemma natle: "(((number_of x)::nat) \ (number_of y)) = (y < x \ lezero x)" + by (auto simp add: number_of_is_id lezero_def nat_number_of_def) + +fun natfac :: "nat \ nat" +where + "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))" + +lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps + +lemma number_eq: "(((number_of x)::'a::{number_ring, ordered_idom}) = (number_of y)) = (x = y)" + unfolding number_of_eq + apply simp + done + +lemma number_le: "(((number_of x)::'a::{number_ring, ordered_idom}) \ (number_of y)) = (x \ y)" + unfolding number_of_eq + apply simp + done + +lemma number_less: "(((number_of x)::'a::{number_ring, ordered_idom}) < (number_of y)) = (x < y)" + unfolding number_of_eq + apply simp + done + +lemma number_diff: "((number_of x)::'a::{number_ring, ordered_idom}) - number_of y = number_of (x + (- y))" + apply (subst diff_number_of_eq) + apply simp + done + +lemmas number_norm = number_of_Pls[symmetric] numeral_1_eq_1[symmetric] + +lemmas compute_numberarith = number_of_minus[symmetric] number_of_add[symmetric] number_diff number_of_mult[symmetric] number_norm number_eq number_le number_less + +lemma compute_real_of_nat_number_of: "real ((number_of v)::nat) = (if neg v then 0 else number_of v)" + by (simp only: real_of_nat_number_of number_of_is_id) + +lemma compute_nat_of_int_number_of: "nat ((number_of v)::int) = (number_of v)" + by simp + +lemmas compute_num_conversions = compute_real_of_nat_number_of compute_nat_of_int_number_of real_number_of + +lemmas zpowerarith = zpower_number_of_even + zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring] + zpower_Pls zpower_Min + +(* div, mod *) + +lemma adjust: "adjust b (q, r) = (if 0 \ r - b then (2 * q + 1, r - b) else (2 * q, r))" + by (auto simp only: adjust_def) + +lemma negateSnd: "negateSnd (q, r) = (q, -r)" + by (simp add: negateSnd_def) + +lemma divmod: "IntDiv.divmod a b = (if 0\a then + if 0\b then posDivAlg a b + else if a=0 then (0, 0) + else negateSnd (negDivAlg (-a) (-b)) + else + if 0 theory -> theory +end +*} + +end diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/MirabelleTest.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/MirabelleTest.thy Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,22 @@ +(* Title: MirabelleTest.thy + Author: Sascha Boehme +*) + +header {* Simple test theory for Mirabelle actions *} + +theory MirabelleTest +imports Main Mirabelle +uses + "Tools/mirabelle_arith.ML" + "Tools/mirabelle_metis.ML" + "Tools/mirabelle_quickcheck.ML" + "Tools/mirabelle_refute.ML" + "Tools/mirabelle_sledgehammer.ML" +begin + +(* + only perform type-checking of the actions, + any reasonable test would be too complicated +*) + +end diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/ROOT.ML Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,3 @@ +if String.isPrefix "polyml" ml_system +then use_thy "MirabelleTest" +else (); diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/Tools/mirabelle.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,192 @@ +(* Title: mirabelle.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +signature MIRABELLE = +sig + (* configuration *) + val logfile : string Config.T + val timeout : int Config.T + val start_line : int Config.T + val end_line : int Config.T + val setup : theory -> theory + + (* core *) + type action + val register : string * action -> theory -> theory + val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> + unit + + (* utility functions *) + val goal_thm_of : Proof.state -> thm + val can_apply : Time.time -> (Proof.context -> int -> tactic) -> + Proof.state -> bool + val theorems_in_proof_term : Thm.thm -> Thm.thm list + val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list + val get_setting : (string * string) list -> string * string -> string + val get_int_setting : (string * string) list -> string * int -> int + val cpu_time : ('a -> 'b) -> 'a -> 'b * int +end + + + +structure Mirabelle : MIRABELLE = +struct + +(* Mirabelle configuration *) + +val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" "" +val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30 +val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0 +val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1 + +val setup = setup1 #> setup2 #> setup3 #> setup4 + + + +(* Mirabelle core *) + +type action = {pre: Proof.state, post: Toplevel.state option, + timeout: Time.time, log: string -> unit} -> unit + +structure Actions = TheoryDataFun +( + type T = action Symtab.table + val empty = Symtab.empty + val copy = I + val extend = I + fun merge _ = Symtab.merge (K true) +) + +val register = Actions.map o Symtab.update_new + +local + +fun log thy s = + let fun append_to n = if n = "" then K () else File.append (Path.explode n) + in append_to (Config.get_thy thy logfile) (s ^ "\n") end + (* FIXME: with multithreading and parallel proofs enabled, we might need to + encapsulate this inside a critical section *) + +fun log_sep thy = log thy "------------------" + +fun log_exn thy name (exn : exn) = log thy ("Unhandled exception in action " ^ + quote name ^ ":\n" ^ PolyML.makestring exn) + +fun try_with f g x = SOME (g x) + handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; NONE) + +fun capture_exns thy name f x = (try_with (log_exn thy name) f x; log_sep thy) + +fun apply_actions thy info (pre, post, time) actions = + let + fun apply (name, action) = + {pre=pre, post=post, timeout=time, log=log thy} + |> capture_exns thy name action + in (log thy info; log_sep thy; List.app apply actions) end + +fun in_range _ _ NONE = true + | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) + +fun only_within_range thy pos f x = + let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line + in if in_range l r (Position.line_of pos) then f x else () end + +in + +fun basic_hook tr pre post = + let + val thy = Proof.theory_of pre + val pos = Toplevel.pos_of tr + val name = Toplevel.name_of tr + val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout)) + + val str0 = string_of_int o the_default 0 + val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) + val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):" + in + Actions.get thy + |> Symtab.dest + |> only_within_range thy pos (apply_actions thy info st) + end + +end + +val whitelist = ["apply", "by", "proof"] + +fun step_hook tr pre post = + (* FIXME: might require wrapping into "interruptible" *) + if can (Proof.assert_backward o Toplevel.proof_of) pre andalso + member (op =) whitelist (Toplevel.name_of tr) + then basic_hook tr (Toplevel.proof_of pre) (SOME post) + else () (* FIXME: add theory_hook here *) + + + +(* Mirabelle utility functions *) + +val goal_thm_of = snd o snd o Proof.get_goal + +fun can_apply time tac st = + let + val (ctxt, (facts, goal)) = Proof.get_goal st + val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt) + in + (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of + SOME (thm, _) => true + | NONE => false) + end + +local + +fun fold_body_thms f = + let + fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => + fn (x, seen) => + if Inttab.defined seen i then (x, seen) + else + let + val body' = Future.join body + val (x', seen') = app (n + (if name = "" then 0 else 1)) body' + (x, Inttab.update (i, ()) seen) + in (x' |> n = 0 ? f (name, prop, body'), seen') end) + in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end + +in + +fun theorems_in_proof_term thm = + let + val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm) + fun collect (s, _, _) = if s <> "" then insert (op =) s else I + fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE + fun resolve_thms names = map_filter (member_of names) all_thms + in + resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) + end + +end + +fun theorems_of_sucessful_proof state = + (case state of + NONE => [] + | SOME st => + if not (Toplevel.is_proof st) then [] + else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st))) + +fun get_setting settings (key, default) = + the_default default (AList.lookup (op =) settings key) + +fun get_int_setting settings (key, default) = + (case Option.map Int.fromString (AList.lookup (op =) settings key) of + SOME (SOME i) => i + | SOME NONE => error ("bad option: " ^ key) + | NONE => default) + +fun cpu_time f x = + let + val start = start_timing () + val result = Exn.capture (fn () => f x) () + val time = Time.toMilliseconds (#cpu (end_timing start)) + in (Exn.release result, time) end + +end diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/Tools/mirabelle_arith.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,16 @@ +(* Title: mirabelle_arith.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Arith : MIRABELLE_ACTION = +struct + +fun arith_action {pre, timeout, log, ...} = + if Mirabelle.can_apply timeout Arith_Data.arith_tac pre + then log "arith: succeeded" + else () + handle TimeLimit.TimeOut => log "arith: time out" + +fun invoke _ = Mirabelle.register ("arith", arith_action) + +end diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,27 @@ +(* Title: mirabelle_metis.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Metis : MIRABELLE_ACTION = +struct + +fun metis_action {pre, post, timeout, log} = + let + val thms = Mirabelle.theorems_of_sucessful_proof post + val names = map Thm.get_name thms + val add_info = if null names then I else suffix (":\n" ^ commas names) + + val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre)) + + fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts) + in + (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") + |> prefix "metis: " + |> add_info + |> log + end + handle TimeLimit.TimeOut => log "metis: time out" + +fun invoke _ = Mirabelle.register ("metis", metis_action) + +end diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,21 @@ +(* Title: mirabelle_quickcheck.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Quickcheck : MIRABELLE_ACTION = +struct + +fun quickcheck_action args {pre, timeout, log, ...} = + let + val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst + val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1 + in + (case TimeLimit.timeLimit timeout quickcheck pre of + NONE => log "quickcheck: no counterexample" + | SOME _ => log "quickcheck: counterexample found") + end + handle TimeLimit.TimeOut => log "quickcheck: time out" + +fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args) + +end diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/Tools/mirabelle_refute.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,39 @@ +(* Title: mirabelle_refute.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Refute : MIRABELLE_ACTION = +struct + + +(* FIXME: +fun refute_action args timeout {pre=st, ...} = + let + val subgoal = 0 + val thy = Proof.theory_of st + val thm = goal_thm_of st + + val refute = Refute.refute_subgoal thy args thm + val _ = TimeLimit.timeLimit timeout refute subgoal + in + val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) + val warn_log = Substring.full (the (Symtab.lookup tab "warning")) + + val r = + if Substring.isSubstring "model found" writ_log + then + if Substring.isSubstring "spurious" warn_log + then SOME "potential counterexample" + else SOME "real counterexample (bug?)" + else + if Substring.isSubstring "time limit" writ_log + then SOME "no counterexample (time out)" + else if Substring.isSubstring "Search terminated" writ_log + then SOME "no counterexample (normal termination)" + else SOME "no counterexample (unknown)" + in r end +*) + +fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*) + +end diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,107 @@ +(* Title: mirabelle_sledgehammer.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = +struct + +fun thms_of_name ctxt name = + let + val lex = OuterKeyword.get_lexicons + val get = maps (ProofContext.get_fact ctxt o fst) + in + Source.of_string name + |> Symbol.source {do_recover=false} + |> OuterLex.source {do_recover=SOME false} lex Position.start + |> OuterLex.source_proper + |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE + |> Source.exhaust + end + +fun safe init done f x = + let + val y = init x + val z = Exn.capture f y + val _ = done y + in Exn.release z end + +fun with_time true t = "succeeded (" ^ string_of_int t ^ ")" + | with_time false t = "failed (" ^ string_of_int t ^ ")" + +val proverK = "prover" +val keepK = "keep" +val metisK = "metis" + + +local + +fun init NONE = !AtpWrapper.destdir + | init (SOME path) = + let + (* Warning: we implicitly assume single-threaded execution here! *) + val old = !AtpWrapper.destdir + val _ = AtpWrapper.destdir := path + in old end + +fun done path = AtpWrapper.destdir := path + +fun run prover_name timeout st _ = + let + val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st)) + val atp_timeout = AtpManager.get_timeout () + val atp = prover atp_timeout NONE NONE prover_name 1 + val (success, (message, thm_names), _, _, _) = + TimeLimit.timeLimit timeout atp (Proof.get_goal st) + in (success, message, SOME thm_names) end + handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME []) + | TimeLimit.TimeOut => (false, "time out", NONE) + | ERROR msg => (false, "error: " ^ msg, NONE) + +in + +fun run_sledgehammer (args, st, timeout, log) = + let + val prover_name = + AList.lookup (op =) args proverK + |> the_default (hd (space_explode " " (AtpManager.get_atps ()))) + val dir = AList.lookup (op =) args keepK + val ((success, msg, thm_names), time) = + safe init done (Mirabelle.cpu_time (run prover_name timeout st)) dir + fun sh_log s = log ("sledgehammer: " ^ with_time success time ^ " [" ^ + prover_name ^ "]" ^ s) + val _ = if success then sh_log (":\n" ^ msg) else sh_log "" + in if success then thm_names else NONE end + +end + + +fun run_metis (args, st, timeout, log) thm_names = + let + fun get_thms ctxt = maps (thms_of_name ctxt) + fun metis thms ctxt = MetisTools.metis_tac ctxt thms + fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st + fun timed_metis thms = + uncurry with_time (Mirabelle.cpu_time apply_metis thms) + handle TimeLimit.TimeOut => "time out" + | ERROR msg => "error: " ^ msg + fun log_metis s = log ("metis (sledgehammer): " ^ s) + in + if not (AList.defined (op =) args metisK) then () + else if is_none thm_names then () + else + log "-----" + |> K (these thm_names) + |> get_thms (Proof.context_of st) + |> timed_metis + |> log_metis + end + + +fun sledgehammer_action args {pre, timeout, log, ...} = + run_sledgehammer (args, pre, timeout, log) + |> run_metis (args, pre, timeout, log) + +fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args) + +end + diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/doc/options.txt --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/doc/options.txt Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,6 @@ +Options for sledgehammer: + + * prover=NAME: name of the external prover to call + * keep=PATH: path where to keep temporary files created by sledgehammer + * metis=X: apply metis with the theorems found by sledgehammer (X may be any + non-empty string) diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/etc/settings --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/etc/settings Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,8 @@ +MIRABELLE_HOME="$COMPONENT" + +MIRABELLE_LOGIC=HOL +MIRABELLE_THEORY=Main +MIRABELLE_OUTPUT_PATH=/tmp/mirabelle +MIRABELLE_TIMEOUT=30 + +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/lib/Tools/mirabelle --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,88 @@ +#!/usr/bin/env bash +# +# Author: Sascha Boehme +# +# DESCRIPTION: testing tool for automated proof tools + + +PRG="$(basename "$0")" + +function print_action_names() { + TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML" + for NAME in $TOOLS + do + echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/ \1/' + done +} + +function usage() { + out="$MIRABELLE_OUTPUT_PATH" + timeout="$MIRABELLE_TIMEOUT" + echo + echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" + echo + echo " Options are:" + echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)" + echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" + echo " -O DIR output directory for test data (default $out)" + echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" + echo + echo " Apply the given actions (i.e., automated proof tools)" + echo " at all proof steps in the given theory files." + echo + echo " ACTIONS is a colon-separated list of actions, where each action is" + echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:" + print_action_names + echo + echo " FILES is a list of theory files, where each file is either NAME.thy" + echo " or NAME.thy[START:END] and START and END are numbers indicating the" + echo " range the given actions are to be applied." + echo + exit 1 +} + + +## process command line + +# options + +while getopts "L:T:O:t:?" OPT +do + case "$OPT" in + L) + MIRABELLE_LOGIC="$OPTARG" + ;; + T) + MIRABELLE_THEORY="$OPTARG" + ;; + O) + MIRABELLE_OUTPUT_PATH="$OPTARG" + ;; + t) + MIRABELLE_TIMEOUT="$OPTARG" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + +ACTIONS="$1" + +shift + + +# setup + +mkdir -p "$MIRABELLE_OUTPUT_PATH" + + +## main + +for FILE in "$@" +do + perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE" +done + diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,141 @@ +# +# Author: Jasmin Blanchette and Sascha Boehme +# +# Testing tool for automated proof tools. +# + +use File::Basename; + +# environment + +my $isabelle_home = $ENV{'ISABELLE_HOME'}; +my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; +my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; +my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; +my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; +my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; + +my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; + + +# arguments + +my $actions = $ARGV[0]; + +my $thy_file = $ARGV[1]; +my $start_line = "0"; +my $end_line = "~1"; +if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { + $thy_file = $1; + $start_line = $2; + $end_line = $3; +} +my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy"); +my $new_thy_name = $thy_name . "_Mirabelle"; +my $new_thy_file = $output_path . "/" . $new_thy_name . $ext; + + +# setup + +my $setup_thy_name = $thy_name . "_Setup"; +my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; +my $log_file = $output_path . "/" . $thy_name . ".log"; + +my @action_files; +my @action_names; +foreach (split(/:/, $actions)) { + if (m/([^[]*)/) { + push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\""; + push @action_names, $1; + } +} +my $tools = ""; +if ($#action_files >= 0) { + $tools = "uses " . join(" ", @action_files); +} + +open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; + +print SETUP_FILE < + Config.put_thy Mirabelle.timeout $timeout #> + Config.put_thy Mirabelle.start_line $start_line #> + Config.put_thy Mirabelle.end_line $end_line +*} + +END + +foreach (split(/:/, $actions)) { + if (m/([^[]*)(?:\[(.*)\])?/) { + my ($name, $settings_str) = ($1, $2 || ""); + $name =~ s/^([a-z])/\U$1/; + print SETUP_FILE "setup {* Mirabelle_$name.invoke ["; + my $sep = ""; + foreach (split(/,/, $settings_str)) { + if (m/\s*(.*)\s*=\s*(.*)\s*/) { + print SETUP_FILE "$sep(\"$1\", \"$2\")"; + $sep = ", "; + } + } + print SETUP_FILE "] *}\n"; + } +} + +print SETUP_FILE "\nend"; +close SETUP_FILE; + + +# modify target theory file + +open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; +my @lines = ; +close(OLD_FILE); + +my $thy_text = join("", @lines); +my $old_len = length($thy_text); +$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; +$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g; +die "No 'imports' found" if length($thy_text) == $old_len; + +open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; +print NEW_FILE $thy_text; +close(NEW_FILE); + +my $root_file = "$output_path/ROOT_$thy_name.ML"; +open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'"; +print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n"; +close(ROOT_FILE); + + +# run isabelle + +open(LOG_FILE, ">$log_file"); +print LOG_FILE "Run of $new_thy_file with:\n"; +foreach $name (@action_names) { + print LOG_FILE " $name\n"; +} +close(LOG_FILE); + +my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " . + "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n"; + + +# produce report + +if ($result == 0) { + system "perl -w \"$mirabelle_home/lib/scripts/report.pl\" \"$log_file\""; +} + + +# cleanup + +unlink $root_file; +unlink $setup_file; + +exit $result; diff -r d14762642cdd -r 94f61caa546e src/HOL/Mirabelle/lib/scripts/report.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/lib/scripts/report.pl Thu Sep 03 17:26:10 2009 +0200 @@ -0,0 +1,78 @@ +# +# Author: Sascha Boehme +# +# Reports for Mirabelle +# + +my $log_file = $ARGV[0]; + +open(FILE, "<$log_file") || die "Cannot open file '$log_file'"; +my @lines = ; +close(FILE); + +my $unhandled = 0; + +my $sh_calls = 0; +my $sh_succeeded = 0; +my $sh_time = 0; + +my $metis_calls = 0; +my $metis_succeeded = 0; +my $metis_time_out = 0; +my $metis_time = 0; + +foreach (@lines) { + if (m/^unhandled exception/) { + $unhandled++; + } + if (m/^sledgehammer:/) { + $sh_calls++; + } + if (m/^sledgehammer: succeeded \(([0-9]+)\)/) { + $sh_succeeded++; + $sh_time += $1; + } + if (m/^metis \(sledgehammer\):/) { + $metis_calls++; + } + if (m/^metis \(sledgehammer\): succeeded \(([0-9]+)\)/) { + $metis_succeeded++; + $metis_time += $1; + } + if (m/^metis \(sledgehammer\): time out/) { + $metis_time_out++; + } +} + +open(FILE, ">>$log_file") || die "Cannot open file '$log_file'"; + +print FILE "\n\n\n"; + +if ($unhandled > 0) { + print FILE "Number of unhandled exceptions: $unhandled\n\n"; +} + +if ($sh_calls > 0) { + my $percent = $sh_succeeded / $sh_calls * 100; + my $time = $sh_time / 1000; + my $avg_time = $time / $sh_succeeded; + print FILE "Total number of sledgehammer calls: $sh_calls\n"; + print FILE "Number of successful sledgehammer calls: $sh_succeeded\n"; + printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent; + printf FILE "Total time for successful sledgehammer calls: %.3f seconds\n", $time; + printf FILE "Average time for successful sledgehammer calls: %.3f seconds\n\n", $avg_time; +} + +if ($metis_calls > 0) { + my $percent = $metis_succeeded / $metis_calls * 100; + my $time = $metis_time / 1000; + my $avg_time = $time / $metis_succeeded; + print FILE "Total number of metis calls: $metis_calls\n"; + print FILE "Number of successful metis calls: $metis_succeeded\n"; + print FILE "Number of metis time outs: $metis_time_out\n"; + printf FILE "Percentage of successful metis calls: %.0f%%\n", $percent; + printf FILE "Total time for successful metis calls: %.3f seconds\n", $time; + printf FILE "Average time for successful metis calls: %.3f seconds\n", $avg_time; +} + +close(FILE); diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/ComputeFloat.thy --- a/src/HOL/Tools/ComputeFloat.thy Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,568 +0,0 @@ -(* Title: HOL/Tools/ComputeFloat.thy - Author: Steven Obua -*) - -header {* Floating Point Representation of the Reals *} - -theory ComputeFloat -imports Complex_Main -uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML") -begin - -definition - pow2 :: "int \ real" where - "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))" - -definition - float :: "int * int \ real" where - "float x = real (fst x) * pow2 (snd x)" - -lemma pow2_0[simp]: "pow2 0 = 1" -by (simp add: pow2_def) - -lemma pow2_1[simp]: "pow2 1 = 2" -by (simp add: pow2_def) - -lemma pow2_neg: "pow2 x = inverse (pow2 (-x))" -by (simp add: pow2_def) - -lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)" -proof - - have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith - have g: "! a b. a - -1 = a + (1::int)" by arith - have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)" - apply (auto, induct_tac n) - apply (simp_all add: pow2_def) - apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if]) - by (auto simp add: h) - show ?thesis - proof (induct a) - case (1 n) - from pos show ?case by (simp add: algebra_simps) - next - case (2 n) - show ?case - apply (auto) - apply (subst pow2_neg[of "- int n"]) - apply (subst pow2_neg[of "-1 - int n"]) - apply (auto simp add: g pos) - done - qed -qed - -lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)" -proof (induct b) - case (1 n) - show ?case - proof (induct n) - case 0 - show ?case by simp - next - case (Suc m) - show ?case by (auto simp add: algebra_simps pow2_add1 prems) - qed -next - case (2 n) - show ?case - proof (induct n) - case 0 - show ?case - apply (auto) - apply (subst pow2_neg[of "a + -1"]) - apply (subst pow2_neg[of "-1"]) - apply (simp) - apply (insert pow2_add1[of "-a"]) - apply (simp add: algebra_simps) - apply (subst pow2_neg[of "-a"]) - apply (simp) - done - case (Suc m) - have a: "int m - (a + -2) = 1 + (int m - a + 1)" by arith - have b: "int m - -2 = 1 + (int m + 1)" by arith - show ?case - apply (auto) - apply (subst pow2_neg[of "a + (-2 - int m)"]) - apply (subst pow2_neg[of "-2 - int m"]) - apply (auto simp add: algebra_simps) - apply (subst a) - apply (subst b) - apply (simp only: pow2_add1) - apply (subst pow2_neg[of "int m - a + 1"]) - apply (subst pow2_neg[of "int m + 1"]) - apply auto - apply (insert prems) - apply (auto simp add: algebra_simps) - done - qed -qed - -lemma "float (a, e) + float (b, e) = float (a + b, e)" -by (simp add: float_def algebra_simps) - -definition - int_of_real :: "real \ int" where - "int_of_real x = (SOME y. real y = x)" - -definition - real_is_int :: "real \ bool" where - "real_is_int x = (EX (u::int). x = real u)" - -lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))" -by (auto simp add: real_is_int_def int_of_real_def) - -lemma float_transfer: "real_is_int ((real a)*(pow2 c)) \ float (a, b) = float (int_of_real ((real a)*(pow2 c)), b - c)" -by (simp add: float_def real_is_int_def2 pow2_add[symmetric]) - -lemma pow2_int: "pow2 (int c) = 2^c" -by (simp add: pow2_def) - -lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)" -by (simp add: float_def pow2_int[symmetric] pow2_add[symmetric]) - -lemma real_is_int_real[simp]: "real_is_int (real (x::int))" -by (auto simp add: real_is_int_def int_of_real_def) - -lemma int_of_real_real[simp]: "int_of_real (real x) = x" -by (simp add: int_of_real_def) - -lemma real_int_of_real[simp]: "real_is_int x \ real (int_of_real x) = x" -by (auto simp add: int_of_real_def real_is_int_def) - -lemma real_is_int_add_int_of_real: "real_is_int a \ real_is_int b \ (int_of_real (a+b)) = (int_of_real a) + (int_of_real b)" -by (auto simp add: int_of_real_def real_is_int_def) - -lemma real_is_int_add[simp]: "real_is_int a \ real_is_int b \ real_is_int (a+b)" -apply (subst real_is_int_def2) -apply (simp add: real_is_int_add_int_of_real real_int_of_real) -done - -lemma int_of_real_sub: "real_is_int a \ real_is_int b \ (int_of_real (a-b)) = (int_of_real a) - (int_of_real b)" -by (auto simp add: int_of_real_def real_is_int_def) - -lemma real_is_int_sub[simp]: "real_is_int a \ real_is_int b \ real_is_int (a-b)" -apply (subst real_is_int_def2) -apply (simp add: int_of_real_sub real_int_of_real) -done - -lemma real_is_int_rep: "real_is_int x \ ?! (a::int). real a = x" -by (auto simp add: real_is_int_def) - -lemma int_of_real_mult: - assumes "real_is_int a" "real_is_int b" - shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)" -proof - - from prems have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto) - from prems have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto) - from a obtain a'::int where a':"a = real a'" by auto - from b obtain b'::int where b':"b = real b'" by auto - have r: "real a' * real b' = real (a' * b')" by auto - show ?thesis - apply (simp add: a' b') - apply (subst r) - apply (simp only: int_of_real_real) - done -qed - -lemma real_is_int_mult[simp]: "real_is_int a \ real_is_int b \ real_is_int (a*b)" -apply (subst real_is_int_def2) -apply (simp add: int_of_real_mult) -done - -lemma real_is_int_0[simp]: "real_is_int (0::real)" -by (simp add: real_is_int_def int_of_real_def) - -lemma real_is_int_1[simp]: "real_is_int (1::real)" -proof - - have "real_is_int (1::real) = real_is_int(real (1::int))" by auto - also have "\ = True" by (simp only: real_is_int_real) - ultimately show ?thesis by auto -qed - -lemma real_is_int_n1: "real_is_int (-1::real)" -proof - - have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto - also have "\ = True" by (simp only: real_is_int_real) - ultimately show ?thesis by auto -qed - -lemma real_is_int_number_of[simp]: "real_is_int ((number_of \ int \ real) x)" -proof - - have neg1: "real_is_int (-1::real)" - proof - - have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto - also have "\ = True" by (simp only: real_is_int_real) - ultimately show ?thesis by auto - qed - - { - fix x :: int - have "real_is_int ((number_of \ int \ real) x)" - unfolding number_of_eq - apply (induct x) - apply (induct_tac n) - apply (simp) - apply (simp) - apply (induct_tac n) - apply (simp add: neg1) - proof - - fix n :: nat - assume rn: "(real_is_int (of_int (- (int (Suc n)))))" - have s: "-(int (Suc (Suc n))) = -1 + - (int (Suc n))" by simp - show "real_is_int (of_int (- (int (Suc (Suc n)))))" - apply (simp only: s of_int_add) - apply (rule real_is_int_add) - apply (simp add: neg1) - apply (simp only: rn) - done - qed - } - note Abs_Bin = this - { - fix x :: int - have "? u. x = u" - apply (rule exI[where x = "x"]) - apply (simp) - done - } - then obtain u::int where "x = u" by auto - with Abs_Bin show ?thesis by auto -qed - -lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)" -by (simp add: int_of_real_def) - -lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)" -proof - - have 1: "(1::real) = real (1::int)" by auto - show ?thesis by (simp only: 1 int_of_real_real) -qed - -lemma int_of_real_number_of[simp]: "int_of_real (number_of b) = number_of b" -proof - - have "real_is_int (number_of b)" by simp - then have uu: "?! u::int. number_of b = real u" by (auto simp add: real_is_int_rep) - then obtain u::int where u:"number_of b = real u" by auto - have "number_of b = real ((number_of b)::int)" - by (simp add: number_of_eq real_of_int_def) - have ub: "number_of b = real ((number_of b)::int)" - by (simp add: number_of_eq real_of_int_def) - from uu u ub have unb: "u = number_of b" - by blast - have "int_of_real (number_of b) = u" by (simp add: u) - with unb show ?thesis by simp -qed - -lemma float_transfer_even: "even a \ float (a, b) = float (a div 2, b+1)" - apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified]) - apply (simp_all add: pow2_def even_def real_is_int_def algebra_simps) - apply (auto) -proof - - fix q::int - have a:"b - (-1\int) = (1\int) + b" by arith - show "(float (q, (b - (-1\int)))) = (float (q, ((1\int) + b)))" - by (simp add: a) -qed - -lemma int_div_zdiv: "int (a div b) = (int a) div (int b)" -by (rule zdiv_int) - -lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)" -by (rule zmod_int) - -lemma abs_div_2_less: "a \ 0 \ a \ -1 \ abs((a::int) div 2) < abs a" -by arith - -function norm_float :: "int \ int \ int \ int" where - "norm_float a b = (if a \ 0 \ even a then norm_float (a div 2) (b + 1) - else if a = 0 then (0, 0) else (a, b))" -by auto - -termination by (relation "measure (nat o abs o fst)") - (auto intro: abs_div_2_less) - -lemma norm_float: "float x = float (split norm_float x)" -proof - - { - fix a b :: int - have norm_float_pair: "float (a, b) = float (norm_float a b)" - proof (induct a b rule: norm_float.induct) - case (1 u v) - show ?case - proof cases - assume u: "u \ 0 \ even u" - with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto - with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even) - then show ?thesis - apply (subst norm_float.simps) - apply (simp add: ind) - done - next - assume "~(u \ 0 \ even u)" - then show ?thesis - by (simp add: prems float_def) - qed - qed - } - note helper = this - have "? a b. x = (a,b)" by auto - then obtain a b where "x = (a, b)" by blast - then show ?thesis by (simp add: helper) -qed - -lemma float_add_l0: "float (0, e) + x = x" - by (simp add: float_def) - -lemma float_add_r0: "x + float (0, e) = x" - by (simp add: float_def) - -lemma float_add: - "float (a1, e1) + float (a2, e2) = - (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1) - else float (a1*2^(nat (e1-e2))+a2, e2))" - apply (simp add: float_def algebra_simps) - apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric]) - done - -lemma float_add_assoc1: - "(x + float (y1, e1)) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x" - by simp - -lemma float_add_assoc2: - "(float (y1, e1) + x) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x" - by simp - -lemma float_add_assoc3: - "float (y1, e1) + (x + float (y2, e2)) = (float (y1, e1) + float (y2, e2)) + x" - by simp - -lemma float_add_assoc4: - "float (y1, e1) + (float (y2, e2) + x) = (float (y1, e1) + float (y2, e2)) + x" - by simp - -lemma float_mult_l0: "float (0, e) * x = float (0, 0)" - by (simp add: float_def) - -lemma float_mult_r0: "x * float (0, e) = float (0, 0)" - by (simp add: float_def) - -definition - lbound :: "real \ real" -where - "lbound x = min 0 x" - -definition - ubound :: "real \ real" -where - "ubound x = max 0 x" - -lemma lbound: "lbound x \ x" - by (simp add: lbound_def) - -lemma ubound: "x \ ubound x" - by (simp add: ubound_def) - -lemma float_mult: - "float (a1, e1) * float (a2, e2) = - (float (a1 * a2, e1 + e2))" - by (simp add: float_def pow2_add) - -lemma float_minus: - "- (float (a,b)) = float (-a, b)" - by (simp add: float_def) - -lemma zero_less_pow2: - "0 < pow2 x" -proof - - { - fix y - have "0 <= y \ 0 < pow2 y" - by (induct y, induct_tac n, simp_all add: pow2_add) - } - note helper=this - show ?thesis - apply (case_tac "0 <= x") - apply (simp add: helper) - apply (subst pow2_neg) - apply (simp add: helper) - done -qed - -lemma zero_le_float: - "(0 <= float (a,b)) = (0 <= a)" - apply (auto simp add: float_def) - apply (auto simp add: zero_le_mult_iff zero_less_pow2) - apply (insert zero_less_pow2[of b]) - apply (simp_all) - done - -lemma float_le_zero: - "(float (a,b) <= 0) = (a <= 0)" - apply (auto simp add: float_def) - apply (auto simp add: mult_le_0_iff) - apply (insert zero_less_pow2[of b]) - apply auto - done - -lemma float_abs: - "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))" - apply (auto simp add: abs_if) - apply (simp_all add: zero_le_float[symmetric, of a b] float_minus) - done - -lemma float_zero: - "float (0, b) = 0" - by (simp add: float_def) - -lemma float_pprt: - "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))" - by (auto simp add: zero_le_float float_le_zero float_zero) - -lemma pprt_lbound: "pprt (lbound x) = float (0, 0)" - apply (simp add: float_def) - apply (rule pprt_eq_0) - apply (simp add: lbound_def) - done - -lemma nprt_ubound: "nprt (ubound x) = float (0, 0)" - apply (simp add: float_def) - apply (rule nprt_eq_0) - apply (simp add: ubound_def) - done - -lemma float_nprt: - "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))" - by (auto simp add: zero_le_float float_le_zero float_zero) - -lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1" - by auto - -lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)" - by simp - -lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)" - by simp - -lemma mult_left_one: "1 * a = (a::'a::semiring_1)" - by simp - -lemma mult_right_one: "a * 1 = (a::'a::semiring_1)" - by simp - -lemma int_pow_0: "(a::int)^(Numeral0) = 1" - by simp - -lemma int_pow_1: "(a::int)^(Numeral1) = a" - by simp - -lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0" - by simp - -lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1" - by simp - -lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0" - by simp - -lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1" - by simp - -lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1" - by simp - -lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1" -proof - - have 1:"((-1)::nat) = 0" - by simp - show ?thesis by (simp add: 1) -qed - -lemma fst_cong: "a=a' \ fst (a,b) = fst (a',b)" - by simp - -lemma snd_cong: "b=b' \ snd (a,b) = snd (a,b')" - by simp - -lemma lift_bool: "x \ x=True" - by simp - -lemma nlift_bool: "~x \ x=False" - by simp - -lemma not_false_eq_true: "(~ False) = True" by simp - -lemma not_true_eq_false: "(~ True) = False" by simp - -lemmas binarith = - normalize_bin_simps - pred_bin_simps succ_bin_simps - add_bin_simps minus_bin_simps mult_bin_simps - -lemma int_eq_number_of_eq: - "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)" - by (rule eq_number_of_eq) - -lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" - by (simp only: iszero_number_of_Pls) - -lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))" - by simp - -lemma int_iszero_number_of_Bit0: "iszero ((number_of (Int.Bit0 w))::int) = iszero ((number_of w)::int)" - by simp - -lemma int_iszero_number_of_Bit1: "\ iszero ((number_of (Int.Bit1 w))::int)" - by simp - -lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)" - unfolding neg_def number_of_is_id by simp - -lemma int_not_neg_number_of_Pls: "\ (neg (Numeral0::int))" - by simp - -lemma int_neg_number_of_Min: "neg (-1::int)" - by simp - -lemma int_neg_number_of_Bit0: "neg ((number_of (Int.Bit0 w))::int) = neg ((number_of w)::int)" - by simp - -lemma int_neg_number_of_Bit1: "neg ((number_of (Int.Bit1 w))::int) = neg ((number_of w)::int)" - by simp - -lemma int_le_number_of_eq: "(((number_of x)::int) \ number_of y) = (\ neg ((number_of (y + (uminus x)))::int))" - unfolding neg_def number_of_is_id by (simp add: not_less) - -lemmas intarithrel = - int_eq_number_of_eq - lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_Bit0 - lift_bool[OF int_iszero_number_of_Bit1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min] - int_neg_number_of_Bit0 int_neg_number_of_Bit1 int_le_number_of_eq - -lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)" - by simp - -lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))" - by simp - -lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)" - by simp - -lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)" - by simp - -lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym - -lemmas natarith = add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of - -lemmas powerarith = nat_number_of zpower_number_of_even - zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring] - zpower_Pls zpower_Min - -lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 - float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound - -(* for use with the compute oracle *) -lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false - -use "~~/src/HOL/Tools/float_arith.ML" - -end diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/ComputeHOL.thy --- a/src/HOL/Tools/ComputeHOL.thy Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,191 +0,0 @@ -theory ComputeHOL -imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle" -begin - -lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq) -lemma meta_eq_trivial: "x == y \ x == y" by simp -lemma meta_eq_imp_eq: "x == y \ x = y" by auto -lemma eq_trivial: "x = y \ x = y" by auto -lemma bool_to_true: "x :: bool \ x == True" by simp -lemma transmeta_1: "x = y \ y == z \ x = z" by simp -lemma transmeta_2: "x == y \ y = z \ x = z" by simp -lemma transmeta_3: "x == y \ y == z \ x = z" by simp - - -(**** compute_if ****) - -lemma If_True: "If True = (\ x y. x)" by ((rule ext)+,auto) -lemma If_False: "If False = (\ x y. y)" by ((rule ext)+, auto) - -lemmas compute_if = If_True If_False - -(**** compute_bool ****) - -lemma bool1: "(\ True) = False" by blast -lemma bool2: "(\ False) = True" by blast -lemma bool3: "(P \ True) = P" by blast -lemma bool4: "(True \ P) = P" by blast -lemma bool5: "(P \ False) = False" by blast -lemma bool6: "(False \ P) = False" by blast -lemma bool7: "(P \ True) = True" by blast -lemma bool8: "(True \ P) = True" by blast -lemma bool9: "(P \ False) = P" by blast -lemma bool10: "(False \ P) = P" by blast -lemma bool11: "(True \ P) = P" by blast -lemma bool12: "(P \ True) = True" by blast -lemma bool13: "(True \ P) = P" by blast -lemma bool14: "(P \ False) = (\ P)" by blast -lemma bool15: "(False \ P) = True" by blast -lemma bool16: "(False = False) = True" by blast -lemma bool17: "(True = True) = True" by blast -lemma bool18: "(False = True) = False" by blast -lemma bool19: "(True = False) = False" by blast - -lemmas compute_bool = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10 bool11 bool12 bool13 bool14 bool15 bool16 bool17 bool18 bool19 - - -(*** compute_pair ***) - -lemma compute_fst: "fst (x,y) = x" by simp -lemma compute_snd: "snd (x,y) = y" by simp -lemma compute_pair_eq: "((a, b) = (c, d)) = (a = c \ b = d)" by auto - -lemma prod_case_simp: "prod_case f (x,y) = f x y" by simp - -lemmas compute_pair = compute_fst compute_snd compute_pair_eq prod_case_simp - -(*** compute_option ***) - -lemma compute_the: "the (Some x) = x" by simp -lemma compute_None_Some_eq: "(None = Some x) = False" by auto -lemma compute_Some_None_eq: "(Some x = None) = False" by auto -lemma compute_None_None_eq: "(None = None) = True" by auto -lemma compute_Some_Some_eq: "(Some x = Some y) = (x = y)" by auto - -definition - option_case_compute :: "'b option \ 'a \ ('b \ 'a) \ 'a" -where - "option_case_compute opt a f = option_case a f opt" - -lemma option_case_compute: "option_case = (\ a f opt. option_case_compute opt a f)" - by (simp add: option_case_compute_def) - -lemma option_case_compute_None: "option_case_compute None = (\ a f. a)" - apply (rule ext)+ - apply (simp add: option_case_compute_def) - done - -lemma option_case_compute_Some: "option_case_compute (Some x) = (\ a f. f x)" - apply (rule ext)+ - apply (simp add: option_case_compute_def) - done - -lemmas compute_option_case = option_case_compute option_case_compute_None option_case_compute_Some - -lemmas compute_option = compute_the compute_None_Some_eq compute_Some_None_eq compute_None_None_eq compute_Some_Some_eq compute_option_case - -(**** compute_list_length ****) - -lemma length_cons:"length (x#xs) = 1 + (length xs)" - by simp - -lemma length_nil: "length [] = 0" - by simp - -lemmas compute_list_length = length_nil length_cons - -(*** compute_list_case ***) - -definition - list_case_compute :: "'b list \ 'a \ ('b \ 'b list \ 'a) \ 'a" -where - "list_case_compute l a f = list_case a f l" - -lemma list_case_compute: "list_case = (\ (a::'a) f (l::'b list). list_case_compute l a f)" - apply (rule ext)+ - apply (simp add: list_case_compute_def) - done - -lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\ (a::'a) f. a)" - apply (rule ext)+ - apply (simp add: list_case_compute_def) - done - -lemma list_case_compute_cons: "list_case_compute (u#v) = (\ (a::'a) f. (f (u::'b) v))" - apply (rule ext)+ - apply (simp add: list_case_compute_def) - done - -lemmas compute_list_case = list_case_compute list_case_compute_empty list_case_compute_cons - -(*** compute_list_nth ***) -(* Of course, you will need computation with nats for this to work \ *) - -lemma compute_list_nth: "((x#xs) ! n) = (if n = 0 then x else (xs ! (n - 1)))" - by (cases n, auto) - -(*** compute_list ***) - -lemmas compute_list = compute_list_case compute_list_length compute_list_nth - -(*** compute_let ***) - -lemmas compute_let = Let_def - -(***********************) -(* Everything together *) -(***********************) - -lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let - -ML {* -signature ComputeHOL = -sig - val prep_thms : thm list -> thm list - val to_meta_eq : thm -> thm - val to_hol_eq : thm -> thm - val symmetric : thm -> thm - val trans : thm -> thm -> thm -end - -structure ComputeHOL : ComputeHOL = -struct - -local -fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq)); -in -fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", []) - | rewrite_conv (eq :: eqs) ct = - Thm.instantiate (Thm.match (lhs_of eq, ct)) eq - handle Pattern.MATCH => rewrite_conv eqs ct; -end - -val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}]))) - -val eq_th = @{thm "HOL.eq_reflection"} -val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"} -val bool_to_true = @{thm "ComputeHOL.bool_to_true"} - -fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th] - -fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] - -fun prep_thms ths = map (convert_conditions o to_meta_eq) ths - -fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th] - -local - val trans_HOL = @{thm "HOL.trans"} - val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"} - val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"} - val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"} - fun tr [] th1 th2 = trans_HOL OF [th1, th2] - | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) -in - fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2 -end - -end -*} - -end diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/ComputeNumeral.thy --- a/src/HOL/Tools/ComputeNumeral.thy Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,195 +0,0 @@ -theory ComputeNumeral -imports ComputeHOL ComputeFloat -begin - -(* normalization of bit strings *) -lemmas bitnorm = normalize_bin_simps - -(* neg for bit strings *) -lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def) -lemma neg2: "neg Int.Min = True" apply (subst Int.Min_def) by auto -lemma neg3: "neg (Int.Bit0 x) = neg x" apply (simp add: neg_def) apply (subst Bit0_def) by auto -lemma neg4: "neg (Int.Bit1 x) = neg x" apply (simp add: neg_def) apply (subst Bit1_def) by auto -lemmas bitneg = neg1 neg2 neg3 neg4 - -(* iszero for bit strings *) -lemma iszero1: "iszero Int.Pls = True" by (simp add: Int.Pls_def iszero_def) -lemma iszero2: "iszero Int.Min = False" apply (subst Int.Min_def) apply (subst iszero_def) by simp -lemma iszero3: "iszero (Int.Bit0 x) = iszero x" apply (subst Int.Bit0_def) apply (subst iszero_def)+ by auto -lemma iszero4: "iszero (Int.Bit1 x) = False" apply (subst Int.Bit1_def) apply (subst iszero_def)+ apply simp by arith -lemmas bitiszero = iszero1 iszero2 iszero3 iszero4 - -(* lezero for bit strings *) -constdefs - "lezero x == (x \ 0)" -lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto -lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto -lemma lezero3: "lezero (Int.Bit0 x) = lezero x" unfolding Int.Bit0_def lezero_def by auto -lemma lezero4: "lezero (Int.Bit1 x) = neg x" unfolding Int.Bit1_def lezero_def neg_def by auto -lemmas bitlezero = lezero1 lezero2 lezero3 lezero4 - -(* equality for bit strings *) -lemmas biteq = eq_bin_simps - -(* x < y for bit strings *) -lemmas bitless = less_bin_simps - -(* x \ y for bit strings *) -lemmas bitle = le_bin_simps - -(* succ for bit strings *) -lemmas bitsucc = succ_bin_simps - -(* pred for bit strings *) -lemmas bitpred = pred_bin_simps - -(* unary minus for bit strings *) -lemmas bituminus = minus_bin_simps - -(* addition for bit strings *) -lemmas bitadd = add_bin_simps - -(* multiplication for bit strings *) -lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def) -lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min) -lemma multb0x: "(Int.Bit0 x) * y = Int.Bit0 (x * y)" by (rule mult_Bit0) -lemma multxb0: "x * (Int.Bit0 y) = Int.Bit0 (x * y)" unfolding Bit0_def by simp -lemma multb1: "(Int.Bit1 x) * (Int.Bit1 y) = Int.Bit1 (Int.Bit0 (x * y) + x + y)" - unfolding Bit0_def Bit1_def by (simp add: algebra_simps) -lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1 - -lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul - -constdefs - "nat_norm_number_of (x::nat) == x" - -lemma nat_norm_number_of: "nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)" - apply (simp add: nat_norm_number_of_def) - unfolding lezero_def iszero_def neg_def - apply (simp add: numeral_simps) - done - -(* Normalization of nat literals *) -lemma natnorm0: "(0::nat) = number_of (Int.Pls)" by auto -lemma natnorm1: "(1 :: nat) = number_of (Int.Bit1 Int.Pls)" by auto -lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of - -(* Suc *) -lemma natsuc: "Suc (number_of x) = (if neg x then 1 else number_of (Int.succ x))" by (auto simp add: number_of_is_id) - -(* Addition for nat *) -lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))" - unfolding nat_number_of_def number_of_is_id neg_def - by auto - -(* Subtraction for nat *) -lemma natsub: "(number_of x) - ((number_of y)::nat) = - (if neg x then 0 else (if neg y then number_of x else (nat_norm_number_of (number_of (x + (- y))))))" - unfolding nat_norm_number_of - by (auto simp add: number_of_is_id neg_def lezero_def iszero_def Let_def nat_number_of_def) - -(* Multiplication for nat *) -lemma natmul: "(number_of x) * ((number_of y)::nat) = - (if neg x then 0 else (if neg y then 0 else number_of (x * y)))" - unfolding nat_number_of_def number_of_is_id neg_def - by (simp add: nat_mult_distrib) - -lemma nateq: "(((number_of x)::nat) = (number_of y)) = ((lezero x \ lezero y) \ (x = y))" - by (auto simp add: iszero_def lezero_def neg_def number_of_is_id) - -lemma natless: "(((number_of x)::nat) < (number_of y)) = ((x < y) \ (\ (lezero y)))" - by (simp add: lezero_def numeral_simps not_le) - -lemma natle: "(((number_of x)::nat) \ (number_of y)) = (y < x \ lezero x)" - by (auto simp add: number_of_is_id lezero_def nat_number_of_def) - -fun natfac :: "nat \ nat" -where - "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))" - -lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps - -lemma number_eq: "(((number_of x)::'a::{number_ring, ordered_idom}) = (number_of y)) = (x = y)" - unfolding number_of_eq - apply simp - done - -lemma number_le: "(((number_of x)::'a::{number_ring, ordered_idom}) \ (number_of y)) = (x \ y)" - unfolding number_of_eq - apply simp - done - -lemma number_less: "(((number_of x)::'a::{number_ring, ordered_idom}) < (number_of y)) = (x < y)" - unfolding number_of_eq - apply simp - done - -lemma number_diff: "((number_of x)::'a::{number_ring, ordered_idom}) - number_of y = number_of (x + (- y))" - apply (subst diff_number_of_eq) - apply simp - done - -lemmas number_norm = number_of_Pls[symmetric] numeral_1_eq_1[symmetric] - -lemmas compute_numberarith = number_of_minus[symmetric] number_of_add[symmetric] number_diff number_of_mult[symmetric] number_norm number_eq number_le number_less - -lemma compute_real_of_nat_number_of: "real ((number_of v)::nat) = (if neg v then 0 else number_of v)" - by (simp only: real_of_nat_number_of number_of_is_id) - -lemma compute_nat_of_int_number_of: "nat ((number_of v)::int) = (number_of v)" - by simp - -lemmas compute_num_conversions = compute_real_of_nat_number_of compute_nat_of_int_number_of real_number_of - -lemmas zpowerarith = zpower_number_of_even - zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring] - zpower_Pls zpower_Min - -(* div, mod *) - -lemma adjust: "adjust b (q, r) = (if 0 \ r - b then (2 * q + 1, r - b) else (2 * q, r))" - by (auto simp only: adjust_def) - -lemma negateSnd: "negateSnd (q, r) = (q, -r)" - by (simp add: negateSnd_def) - -lemma divmod: "IntDiv.divmod a b = (if 0\a then - if 0\b then posDivAlg a b - else if a=0 then (0, 0) - else negateSnd (negDivAlg (-a) (-b)) - else - if 0 theory -> theory -end -*} - -end diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,185 +0,0 @@ -(* Title: mirabelle.ML - Author: Jasmin Blanchette and Sascha Boehme -*) - -signature MIRABELLE = -sig - type action - val register : string * action -> theory -> theory - - val logfile : string Config.T - val timeout : int Config.T - val start_line : int Config.T - val end_line : int Config.T - - val goal_thm_of : Proof.state -> thm - val can_apply : Time.time -> (Proof.context -> int -> tactic) -> - Proof.state -> bool - val theorems_in_proof_term : Thm.thm -> Thm.thm list - val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list - val get_setting : (string * string) list -> string * string -> string - val get_int_setting : (string * string) list -> string * int -> int -end - - - -signature MIRABELLE_EXT = -sig - include MIRABELLE - val setup : theory -> theory - val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> - unit -end - - - -structure Mirabelle : MIRABELLE_EXT = -struct - -(* Mirabelle core *) - -type action = {pre: Proof.state, post: Toplevel.state option, - timeout: Time.time, log: string -> unit} -> unit - -structure Actions = TheoryDataFun -( - type T = action Symtab.table - val empty = Symtab.empty - val copy = I - val extend = I - fun merge _ = Symtab.merge (K true) -) - -val register = Actions.map o Symtab.update_new - -val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" "" -val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30 -val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0 -val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1 - -val setup = setup1 #> setup2 #> setup3 #> setup4 - -local - -fun log thy s = - let fun append_to n = if n = "" then K () else File.append (Path.explode n) - in append_to (Config.get_thy thy logfile) (s ^ "\n") end - (* FIXME: with multithreading and parallel proofs enabled, we might need to - encapsulate this inside a critical section *) - -fun log_block thy msg = log thy (msg ^ "\n------------------") -fun log_action thy name msg = log_block thy (name ^ ": " ^ msg) - -fun capture_exns logf f x = - let - fun f' x = f x - handle TimeLimit.TimeOut => logf "time out" - | ERROR msg => logf ("error: " ^ msg) - in (case try f' x of NONE => logf "exception" | _ => ()) end - -fun apply_actions thy info (pre, post, time) actions = - let - val _ = log_block thy info - fun apply (name, action) = - let val st = {pre=pre, post=post, timeout=time, log=log_action thy name} - in capture_exns (log_action thy name) action st end - in List.app apply actions end - -fun in_range _ _ NONE = true - | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) - -fun only_within_range thy pos f x = - let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line - in if in_range l r (Position.line_of pos) then f x else () end - -in - -fun basic_hook tr pre post = - let - val thy = Proof.theory_of pre - val pos = Toplevel.pos_of tr - val name = Toplevel.name_of tr - val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout)) - - val str0 = string_of_int o the_default 0 - val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) - val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):" - in - Actions.get thy - |> Symtab.dest - |> only_within_range thy pos (apply_actions thy info st) - end - -end - -val blacklist = ["disable_pr", "enable_pr", "done", ".", "using", "txt"] - -fun step_hook tr pre post = - (* FIXME: might require wrapping into "interruptible" *) - if can (Proof.assert_backward o Toplevel.proof_of) pre andalso - not (member (op =) blacklist (Toplevel.name_of tr)) - then basic_hook tr (Toplevel.proof_of pre) (SOME post) - else () (* FIXME: add theory_hook here *) - - - -(* Mirabelle utility functions *) - -val goal_thm_of = snd o snd o Proof.get_goal - -fun can_apply time tac st = - let - val (ctxt, (facts, goal)) = Proof.get_goal st - val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt) - in - (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of - SOME (thm, _) => true - | NONE => false) - end - -local - -fun fold_body_thms f = - let - fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => - fn (x, seen) => - if Inttab.defined seen i then (x, seen) - else - let - val body' = Future.join body - val (x', seen') = app (n + (if name = "" then 0 else 1)) body' - (x, Inttab.update (i, ()) seen) - in (x' |> n = 0 ? f (name, prop, body'), seen') end) - in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end - -in - -fun theorems_in_proof_term thm = - let - val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm) - fun collect (s, _, _) = if s <> "" then insert (op =) s else I - fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE - fun resolve_thms names = map_filter (member_of names) all_thms - in - resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) - end - -end - -fun theorems_of_sucessful_proof state = - (case state of - NONE => [] - | SOME st => - if not (Toplevel.is_proof st) then [] - else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st))) - -fun get_setting settings (key, default) = - the_default default (AList.lookup (op =) settings key) - -fun get_int_setting settings (key, default) = - (case Option.map Int.fromString (AList.lookup (op =) settings key) of - SOME (SOME i) => i - | SOME NONE => error ("bad option: " ^ key) - | NONE => default) - -end diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: mirabelle_arith.ML - Author: Jasmin Blanchette and Sascha Boehme -*) - -structure Mirabelle_Arith : MIRABELLE_ACTION = -struct - -fun arith_action {pre, timeout, log, ...} = - if Mirabelle.can_apply timeout Arith_Data.arith_tac pre - then log "succeeded" - else () - -fun invoke _ = Mirabelle.register ("arith", arith_action) - -end diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ -(* Title: mirabelle_metis.ML - Author: Jasmin Blanchette and Sascha Boehme -*) - -structure Mirabelle_Metis : MIRABELLE_ACTION = -struct - -fun metis_action {pre, post, timeout, log} = - let - val thms = Mirabelle.theorems_of_sucessful_proof post - val names = map Thm.get_name thms - val add_info = if null names then I else suffix (":\n" ^ commas names) - - val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre)) - - fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts) - in - (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") - |> add_info - |> log - end - -fun invoke _ = Mirabelle.register ("metis", metis_action) - -end diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ -(* Title: mirabelle_quickcheck.ML - Author: Jasmin Blanchette and Sascha Boehme -*) - -structure Mirabelle_Quickcheck : MIRABELLE_ACTION = -struct - -fun quickcheck_action limit args {pre=st, ...} = - let - val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst - val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1 - in - (case TimeLimit.timeLimit limit quickcheck st of - NONE => SOME "no counterexample" - | SOME _ => SOME "counterexample found") - end - -fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args) - -end diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -(* Title: mirabelle_refute.ML - Author: Jasmin Blanchette and Sascha Boehme -*) - -structure Mirabelle_Refute : MIRABELLE_ACTION = -struct - - -(* FIXME: -fun refute_action args timeout {pre=st, ...} = - let - val subgoal = 0 - val thy = Proof.theory_of st - val thm = goal_thm_of st - - val refute = Refute.refute_subgoal thy args thm - val _ = TimeLimit.timeLimit timeout refute subgoal - in - val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) - val warn_log = Substring.full (the (Symtab.lookup tab "warning")) - - val r = - if Substring.isSubstring "model found" writ_log - then - if Substring.isSubstring "spurious" warn_log - then SOME "potential counterexample" - else SOME "real counterexample (bug?)" - else - if Substring.isSubstring "time limit" writ_log - then SOME "no counterexample (time out)" - else if Substring.isSubstring "Search terminated" writ_log - then SOME "no counterexample (normal termination)" - else SOME "no counterexample (unknown)" - in r end -*) - -fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*) - -end diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,84 +0,0 @@ -(* Title: mirabelle_sledgehammer.ML - Author: Jasmin Blanchette and Sascha Boehme -*) - -structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = -struct - -fun thms_of_name ctxt name = - let - val lex = OuterKeyword.get_lexicons - val get = maps (ProofContext.get_fact ctxt o fst) - in - Source.of_string name - |> Symbol.source {do_recover=false} - |> OuterLex.source {do_recover=SOME false} lex Position.start - |> OuterLex.source_proper - |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE - |> Source.exhaust - end - -fun safe init done f x = - let - val y = init x - val z = Exn.capture f y - val _ = done y - in Exn.release z end - -val proverK = "prover" -val keepK = "keep" -val metisK = "metis" - -fun sledgehammer_action args {pre=st, timeout, log, ...} = - let - val prover_name = - AList.lookup (op =) args proverK - |> the_default (hd (space_explode " " (AtpManager.get_atps ()))) - - val thy = Proof.theory_of st - - val prover = the (AtpManager.get_prover prover_name thy) - val atp_timeout = AtpManager.get_timeout () - - (* run sledgehammer *) - fun init NONE = !AtpWrapper.destdir - | init (SOME path) = - let - (* Warning: we implicitly assume single-threaded execution here! *) - val old = !AtpWrapper.destdir - val _ = AtpWrapper.destdir := path - in old end - fun done path = AtpWrapper.destdir := path - fun sh _ = - let - val atp = prover atp_timeout NONE NONE prover_name 1 - val (success, (message, thm_names), _, _, _) = - TimeLimit.timeLimit timeout atp (Proof.get_goal st) - in (success, message, SOME thm_names) end - handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME []) - val (success, message, thm_names) = safe init done sh - (AList.lookup (op =) args keepK) - val _ = - if success then log (quote prover_name ^ " succeeded:\n" ^ message) - else log (prover_name ^ " failed") - - (* try metis *) - fun get_thms ctxt = maps (thms_of_name ctxt) - fun metis thms ctxt = MetisTools.metis_tac ctxt thms - fun log_metis s = - log ("applying metis: " ^ s) - fun apply_metis thms = - if Mirabelle.can_apply timeout (metis thms) st - then "succeeded" else "failed" - val _ = - if not (AList.defined (op =) args metisK) then () - else - these thm_names - |> get_thms (Proof.context_of st) - |> apply_metis - |> log_metis - in () end - -fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args) - -end diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/Mirabelle/doc/options.txt --- a/src/HOL/Tools/Mirabelle/doc/options.txt Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -Options for sledgehammer: - - * prover=NAME: name of the external prover to call - * keep=PATH: path where to keep temporary files created by sledgehammer - * metis=X: apply metis with the theorems found by sledgehammer (X may be any - non-empty string) diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/Mirabelle/etc/settings --- a/src/HOL/Tools/Mirabelle/etc/settings Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -MIRABELLE_HOME="$COMPONENT" - -MIRABELLE_LOGIC=HOL -MIRABELLE_THEORY=Main -MIRABELLE_OUTPUT_PATH=/tmp/mirabelle -MIRABELLE_TIMEOUT=30 - -ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,88 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Sascha Boehme -# -# DESCRIPTION: testing tool for automated proof tools - - -PRG="$(basename "$0")" - -function print_action_names() { - TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML" - for NAME in $TOOLS - do - echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/ \1/' - done -} - -function usage() { - out="$MIRABELLE_OUTPUT_PATH" - timeout="$MIRABELLE_TIMEOUT" - echo - echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" - echo - echo " Options are:" - echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)" - echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" - echo " -O DIR output directory for test data (default $out)" - echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" - echo - echo " Apply the given actions (i.e., automated proof tools)" - echo " at all proof steps in the given theory files." - echo - echo " ACTIONS is a colon-separated list of actions, where each action is" - echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:" - print_action_names - echo - echo " FILES is a list of theory files, where each file is either NAME.thy" - echo " or NAME.thy[START:END] and START and END are numbers indicating the" - echo " range the given actions are to be applied." - echo - exit 1 -} - - -## process command line - -# options - -while getopts "L:T:O:t:?" OPT -do - case "$OPT" in - L) - MIRABELLE_LOGIC="$OPTARG" - ;; - T) - MIRABELLE_THEORY="$OPTARG" - ;; - O) - MIRABELLE_OUTPUT_PATH="$OPTARG" - ;; - t) - MIRABELLE_TIMEOUT="$OPTARG" - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - -ACTIONS="$1" - -shift - - -# setup - -mkdir -p "$MIRABELLE_OUTPUT_PATH" - - -## main - -for FILE in "$@" -do - perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE" -done - diff -r d14762642cdd -r 94f61caa546e src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Thu Sep 03 15:39:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,135 +0,0 @@ -# -# Author: Jasmin Blanchette and Sascha Boehme -# -# Testing tool for automated proof tools. -# - -use File::Basename; - -# environment - -my $isabelle_home = $ENV{'ISABELLE_HOME'}; -my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; -my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; -my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; -my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; -my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; - -my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; - - -# arguments - -my $actions = $ARGV[0]; - -my $thy_file = $ARGV[1]; -my $start_line = "0"; -my $end_line = "~1"; -if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { - $thy_file = $1; - $start_line = $2; - $end_line = $3; -} -my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy"); -my $new_thy_name = $thy_name . "_Mirabelle"; -my $new_thy_file = $output_path . "/" . $new_thy_name . $ext; - - -# setup - -my $setup_thy_name = $thy_name . "_Setup"; -my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; -my $log_file = $output_path . "/" . $thy_name . ".log"; - -my @action_files; -my @action_names; -foreach (split(/:/, $actions)) { - if (m/([^[]*)/) { - push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\""; - push @action_names, $1; - } -} -my $tools = ""; -if ($#action_files >= 0) { - $tools = "uses " . join(" ", @action_files); -} - -open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; - -print SETUP_FILE < - Config.put_thy Mirabelle.timeout $timeout #> - Config.put_thy Mirabelle.start_line $start_line #> - Config.put_thy Mirabelle.end_line $end_line -*} - -END - -foreach (split(/:/, $actions)) { - if (m/([^[]*)(?:\[(.*)\])?/) { - my ($name, $settings_str) = ($1, $2 || ""); - $name =~ s/^([a-z])/\U$1/; - print SETUP_FILE "setup {* Mirabelle_$name.invoke ["; - my $sep = ""; - foreach (split(/,/, $settings_str)) { - if (m/\s*(.*)\s*=\s*(.*)\s*/) { - print SETUP_FILE "$sep(\"$1\", \"$2\")"; - $sep = ", "; - } - } - print SETUP_FILE "] *}\n"; - } -} - -print SETUP_FILE "\nend"; -close SETUP_FILE; - - -# modify target theory file - -open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; -my @lines = ; -close(OLD_FILE); - -my $thy_text = join("", @lines); -my $old_len = length($thy_text); -$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; -$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g; -die "No 'imports' found" if length($thy_text) == $old_len; - -open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; -print NEW_FILE $thy_text; -close(NEW_FILE); - -my $root_file = "$output_path/ROOT_$thy_name.ML"; -open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'"; -print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n"; -close(ROOT_FILE); - - -# run isabelle - -open(LOG_FILE, ">$log_file"); -print LOG_FILE "Run of $new_thy_file with:\n"; -foreach $name (@action_names) { - print LOG_FILE " $name\n"; -} -close(LOG_FILE); - -my $r = system "\"$ENV{'ISABELLE_PROCESS'}\" " . - "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n"; - - -# cleanup - -unlink $root_file; -unlink $setup_file; - -exit $r; - diff -r d14762642cdd -r 94f61caa546e src/Pure/General/swing_thread.scala --- a/src/Pure/General/swing_thread.scala Thu Sep 03 15:39:02 2009 +0200 +++ b/src/Pure/General/swing_thread.scala Thu Sep 03 17:26:10 2009 +0200 @@ -13,36 +13,43 @@ object Swing_Thread { + /* checks */ + + def assert() = Predef.assert(SwingUtilities.isEventDispatchThread()) + def require() = Predef.require(SwingUtilities.isEventDispatchThread()) + + /* main dispatch queue */ def now[A](body: => A): A = { var result: Option[A] = None - if (SwingUtilities.isEventDispatchThread) { result = Some(body) } + if (SwingUtilities.isEventDispatchThread()) { result = Some(body) } else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) result.get } def later(body: => Unit) { - if (SwingUtilities.isEventDispatchThread) body + if (SwingUtilities.isEventDispatchThread()) body else SwingUtilities.invokeLater(new Runnable { def run = body }) } /* delayed actions */ - // turn multiple invocations into single action within time span - def delay(time_span: Int)(action: => Unit): () => Unit = + private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit = { val listener = new ActionListener { override def actionPerformed(e: ActionEvent) { action } } val timer = new Timer(time_span, listener) - def invoke() - { - if (!timer.isRunning()) { - timer.setRepeats(false) - timer.start() - } - } + timer.setRepeats(false) + + def invoke() { if (first) timer.start() else timer.restart() } invoke _ } + + // delayed action after first invocation + def delay_first = delayed_action(true) _ + + // delayed action after last invocation + def delay_last = delayed_action(false) _ } diff -r d14762642cdd -r 94f61caa546e src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Sep 03 15:39:02 2009 +0200 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Sep 03 17:26:10 2009 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/ML/ml_compiler_polyml-5.3.ML Author: Makarius -Advanced runtime compilation for Poly/ML 5.3 (SVN 773). +Advanced runtime compilation for Poly/ML 5.3 (SVN 839). *) signature ML_COMPILER = @@ -74,8 +74,8 @@ (* input *) val location_props = - Markup.markup (Markup.position |> Markup.properties - (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))) ""; + op ^ (YXML.output_markup (Markup.position |> Markup.properties + (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos)))); val input = toks |> maps (fn tok => let