--- a/NEWS Tue Jan 27 22:39:41 2009 -0800
+++ b/NEWS Wed Jan 28 06:03:46 2009 -0800
@@ -193,6 +193,8 @@
*** HOL ***
+* Theory "Reflection" now resides in HOL/Library.
+
* Entry point to Word library now simply named "Word". INCOMPATIBILITY.
* Made source layout more coherent with logical distribution
--- a/src/HOL/ATP_Linkup.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/ATP_Linkup.thy Wed Jan 28 06:03:46 2009 -0800
@@ -7,7 +7,7 @@
header {* The Isabelle-ATP Linkup *}
theory ATP_Linkup
-imports Divides Record Hilbert_Choice
+imports Divides Record Hilbert_Choice Plain
uses
"Tools/polyhash.ML"
"Tools/res_clause.ML"
--- a/src/HOL/Dense_Linear_Order.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Dense_Linear_Order.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1,10 +1,12 @@
-(* Author: Amine Chaieb, TU Muenchen *)
+(* Title : HOL/Dense_Linear_Order.thy
+ Author : Amine Chaieb, TU Muenchen
+*)
header {* Dense linear order without endpoints
and a quantifier elimination procedure in Ferrante and Rackoff style *}
theory Dense_Linear_Order
-imports Plain Groebner_Basis
+imports Plain Groebner_Basis Main
uses
"~~/src/HOL/Tools/Qelim/langford_data.ML"
"~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
--- a/src/HOL/Equiv_Relations.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Equiv_Relations.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1,12 +1,11 @@
-(* ID: $Id$
- Authors: Lawrence C Paulson, Cambridge University Computer Laboratory
+(* Authors: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
*)
header {* Equivalence Relations in Higher-Order Set Theory *}
theory Equiv_Relations
-imports Finite_Set Relation
+imports Finite_Set Relation Plain
begin
subsection {* Equivalence relations *}
--- a/src/HOL/GCD.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/GCD.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/GCD.thy
- ID: $Id$
Author: Christophe Tabacznyj and Lawrence C Paulson
Copyright 1996 University of Cambridge
*)
@@ -7,7 +6,7 @@
header {* The Greatest Common Divisor *}
theory GCD
-imports Plain Presburger
+imports Plain Presburger Main
begin
text {*
--- a/src/HOL/Hilbert_Choice.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Hilbert_Choice.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/Hilbert_Choice.thy
- ID: $Id$
Author: Lawrence C Paulson
Copyright 2001 University of Cambridge
*)
@@ -7,7 +6,7 @@
header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
theory Hilbert_Choice
-imports Nat Wellfounded
+imports Nat Wellfounded Plain
uses ("Tools/meson.ML") ("Tools/specification_package.ML")
begin
--- a/src/HOL/IntDiv.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/IntDiv.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1,82 +1,69 @@
(* Title: HOL/IntDiv.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
*)
-header{*The Division Operators div and mod; the Divides Relation dvd*}
+header{* The Division Operators div and mod *}
theory IntDiv
imports Int Divides FunDef
begin
-constdefs
- quorem :: "(int*int) * (int*int) => bool"
+definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
--{*definition of quotient and remainder*}
- [code]: "quorem == %((a,b), (q,r)).
- a = b*q + r &
- (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
+ [code]: "divmod_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
+ (if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0))"
- adjust :: "[int, int*int] => int*int"
+definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
--{*for the division algorithm*}
- [code]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
- else (2*q, r)"
+ [code]: "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
+ else (2 * q, r))"
text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
-function
- posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
-where
- "posDivAlg a b =
- (if (a<b | b\<le>0) then (0,a)
- else adjust b (posDivAlg a (2*b)))"
+function posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
+ "posDivAlg a b = (if a < b \<or> b \<le> 0 then (0, a)
+ else adjust b (posDivAlg a (2 * b)))"
by auto
-termination by (relation "measure (%(a,b). nat(a - b + 1))") auto
+termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))") auto
text{*algorithm for the case @{text "a<0, b>0"}*}
-function
- negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
-where
- "negDivAlg a b =
- (if (0\<le>a+b | b\<le>0) then (-1,a+b)
- else adjust b (negDivAlg a (2*b)))"
+function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
+ "negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0 then (-1, a + b)
+ else adjust b (negDivAlg a (2 * b)))"
by auto
-termination by (relation "measure (%(a,b). nat(- a - b))") auto
+termination by (relation "measure (\<lambda>(a, b). nat (- a - b))") auto
text{*algorithm for the general case @{term "b\<noteq>0"}*}
-constdefs
- negateSnd :: "int*int => int*int"
- [code]: "negateSnd == %(q,r). (q,-r)"
+definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
+ [code inline]: "negateSnd = apsnd uminus"
-definition
- divAlg :: "int \<times> int \<Rightarrow> int \<times> int"
+definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--{*The full division algorithm considers all possible signs for a, b
including the special case @{text "a=0, b<0"} because
@{term negDivAlg} requires @{term "a<0"}.*}
-where
- "divAlg = (\<lambda>(a, b). (if 0\<le>a then
- if 0\<le>b then posDivAlg a b
- else if a=0 then (0, 0)
+ "divmod a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
+ else if a = 0 then (0, 0)
else negateSnd (negDivAlg (-a) (-b))
else
- if 0<b then negDivAlg a b
- else negateSnd (posDivAlg (-a) (-b))))"
+ if 0 < b then negDivAlg a b
+ else negateSnd (posDivAlg (-a) (-b)))"
instantiation int :: Divides.div
begin
definition
- div_def: "a div b = fst (divAlg (a, b))"
+ div_def: "a div b = fst (divmod a b)"
definition
- mod_def: "a mod b = snd (divAlg (a, b))"
+ mod_def: "a mod b = snd (divmod a b)"
instance ..
end
-lemma divAlg_mod_div:
- "divAlg (p, q) = (p div q, p mod q)"
+lemma divmod_mod_div:
+ "divmod p q = (p div q, p mod q)"
by (auto simp add: div_def mod_def)
text{*
@@ -97,7 +84,7 @@
fun negateSnd (q,r:int) = (q,~r);
- fun divAlg (a,b) = if 0\<le>a then
+ fun divmod (a,b) = if 0\<le>a then
if b>0 then posDivAlg (a,b)
else if a=0 then (0,0)
else negateSnd (negDivAlg (~a,~b))
@@ -131,9 +118,9 @@
auto)
lemma unique_quotient:
- "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b \<noteq> 0 |]
+ "[| divmod_rel a b (q, r); divmod_rel a b (q', r'); b \<noteq> 0 |]
==> q = q'"
-apply (simp add: quorem_def linorder_neq_iff split: split_if_asm)
+apply (simp add: divmod_rel_def linorder_neq_iff split: split_if_asm)
apply (blast intro: order_antisym
dest: order_eq_refl [THEN unique_quotient_lemma]
order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
@@ -141,10 +128,10 @@
lemma unique_remainder:
- "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b \<noteq> 0 |]
+ "[| divmod_rel a b (q, r); divmod_rel a b (q', r'); b \<noteq> 0 |]
==> r = r'"
apply (subgoal_tac "q = q'")
- apply (simp add: quorem_def)
+ apply (simp add: divmod_rel_def)
apply (blast intro: unique_quotient)
done
@@ -171,10 +158,10 @@
text{*Correctness of @{term posDivAlg}: it computes quotients correctly*}
theorem posDivAlg_correct:
assumes "0 \<le> a" and "0 < b"
- shows "quorem ((a, b), posDivAlg a b)"
+ shows "divmod_rel a b (posDivAlg a b)"
using prems apply (induct a b rule: posDivAlg.induct)
apply auto
-apply (simp add: quorem_def)
+apply (simp add: divmod_rel_def)
apply (subst posDivAlg_eqn, simp add: right_distrib)
apply (case_tac "a < b")
apply simp_all
@@ -200,10 +187,10 @@
It doesn't work if a=0 because the 0/b equals 0, not -1*)
lemma negDivAlg_correct:
assumes "a < 0" and "b > 0"
- shows "quorem ((a, b), negDivAlg a b)"
+ shows "divmod_rel a b (negDivAlg a b)"
using prems apply (induct a b rule: negDivAlg.induct)
apply (auto simp add: linorder_not_le)
-apply (simp add: quorem_def)
+apply (simp add: divmod_rel_def)
apply (subst negDivAlg_eqn, assumption)
apply (case_tac "a + b < (0\<Colon>int)")
apply simp_all
@@ -215,8 +202,8 @@
subsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
(*the case a=0*)
-lemma quorem_0: "b \<noteq> 0 ==> quorem ((0,b), (0,0))"
-by (auto simp add: quorem_def linorder_neq_iff)
+lemma divmod_rel_0: "b \<noteq> 0 ==> divmod_rel 0 b (0, 0)"
+by (auto simp add: divmod_rel_def linorder_neq_iff)
lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
by (subst posDivAlg.simps, auto)
@@ -227,26 +214,26 @@
lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)"
by (simp add: negateSnd_def)
-lemma quorem_neg: "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)"
-by (auto simp add: split_ifs quorem_def)
+lemma divmod_rel_neg: "divmod_rel (-a) (-b) qr ==> divmod_rel a b (negateSnd qr)"
+by (auto simp add: split_ifs divmod_rel_def)
-lemma divAlg_correct: "b \<noteq> 0 ==> quorem ((a,b), divAlg (a, b))"
-by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg
+lemma divmod_correct: "b \<noteq> 0 ==> divmod_rel a b (divmod a b)"
+by (force simp add: linorder_neq_iff divmod_rel_0 divmod_def divmod_rel_neg
posDivAlg_correct negDivAlg_correct)
text{*Arbitrary definitions for division by zero. Useful to simplify
certain equations.*}
lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
-by (simp add: div_def mod_def divAlg_def posDivAlg.simps)
+by (simp add: div_def mod_def divmod_def posDivAlg.simps)
text{*Basic laws about division and remainder*}
lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
apply (case_tac "b = 0", simp)
-apply (cut_tac a = a and b = b in divAlg_correct)
-apply (auto simp add: quorem_def div_def mod_def)
+apply (cut_tac a = a and b = b in divmod_correct)
+apply (auto simp add: divmod_rel_def div_def mod_def)
done
lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
@@ -288,16 +275,16 @@
*}
lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
-apply (cut_tac a = a and b = b in divAlg_correct)
-apply (auto simp add: quorem_def mod_def)
+apply (cut_tac a = a and b = b in divmod_correct)
+apply (auto simp add: divmod_rel_def mod_def)
done
lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1, standard]
and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard]
lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
-apply (cut_tac a = a and b = b in divAlg_correct)
-apply (auto simp add: quorem_def div_def mod_def)
+apply (cut_tac a = a and b = b in divmod_correct)
+apply (auto simp add: divmod_rel_def div_def mod_def)
done
lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1, standard]
@@ -307,47 +294,47 @@
subsection{*General Properties of div and mod*}
-lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))"
+lemma divmod_rel_div_mod: "b \<noteq> 0 ==> divmod_rel a b (a div b, a mod b)"
apply (cut_tac a = a and b = b in zmod_zdiv_equality)
-apply (force simp add: quorem_def linorder_neq_iff)
+apply (force simp add: divmod_rel_def linorder_neq_iff)
done
-lemma quorem_div: "[| quorem((a,b),(q,r)); b \<noteq> 0 |] ==> a div b = q"
-by (simp add: quorem_div_mod [THEN unique_quotient])
+lemma divmod_rel_div: "[| divmod_rel a b (q, r); b \<noteq> 0 |] ==> a div b = q"
+by (simp add: divmod_rel_div_mod [THEN unique_quotient])
-lemma quorem_mod: "[| quorem((a,b),(q,r)); b \<noteq> 0 |] ==> a mod b = r"
-by (simp add: quorem_div_mod [THEN unique_remainder])
+lemma divmod_rel_mod: "[| divmod_rel a b (q, r); b \<noteq> 0 |] ==> a mod b = r"
+by (simp add: divmod_rel_div_mod [THEN unique_remainder])
lemma div_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a div b = 0"
-apply (rule quorem_div)
-apply (auto simp add: quorem_def)
+apply (rule divmod_rel_div)
+apply (auto simp add: divmod_rel_def)
done
lemma div_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a div b = 0"
-apply (rule quorem_div)
-apply (auto simp add: quorem_def)
+apply (rule divmod_rel_div)
+apply (auto simp add: divmod_rel_def)
done
lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a div b = -1"
-apply (rule quorem_div)
-apply (auto simp add: quorem_def)
+apply (rule divmod_rel_div)
+apply (auto simp add: divmod_rel_def)
done
(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*)
lemma mod_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a mod b = a"
-apply (rule_tac q = 0 in quorem_mod)
-apply (auto simp add: quorem_def)
+apply (rule_tac q = 0 in divmod_rel_mod)
+apply (auto simp add: divmod_rel_def)
done
lemma mod_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a mod b = a"
-apply (rule_tac q = 0 in quorem_mod)
-apply (auto simp add: quorem_def)
+apply (rule_tac q = 0 in divmod_rel_mod)
+apply (auto simp add: divmod_rel_def)
done
lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a mod b = a+b"
-apply (rule_tac q = "-1" in quorem_mod)
-apply (auto simp add: quorem_def)
+apply (rule_tac q = "-1" in divmod_rel_mod)
+apply (auto simp add: divmod_rel_def)
done
text{*There is no @{text mod_neg_pos_trivial}.*}
@@ -356,15 +343,15 @@
(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
apply (case_tac "b = 0", simp)
-apply (simp add: quorem_div_mod [THEN quorem_neg, simplified,
- THEN quorem_div, THEN sym])
+apply (simp add: divmod_rel_div_mod [THEN divmod_rel_neg, simplified,
+ THEN divmod_rel_div, THEN sym])
done
(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
apply (case_tac "b = 0", simp)
-apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod],
+apply (subst divmod_rel_div_mod [THEN divmod_rel_neg, simplified, THEN divmod_rel_mod],
auto)
done
@@ -372,22 +359,22 @@
subsection{*Laws for div and mod with Unary Minus*}
lemma zminus1_lemma:
- "quorem((a,b),(q,r))
- ==> quorem ((-a,b), (if r=0 then -q else -q - 1),
- (if r=0 then 0 else b-r))"
-by (force simp add: split_ifs quorem_def linorder_neq_iff right_diff_distrib)
+ "divmod_rel a b (q, r)
+ ==> divmod_rel (-a) b (if r=0 then -q else -q - 1,
+ if r=0 then 0 else b-r)"
+by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_diff_distrib)
lemma zdiv_zminus1_eq_if:
"b \<noteq> (0::int)
==> (-a) div b =
(if a mod b = 0 then - (a div b) else - (a div b) - 1)"
-by (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_div])
+by (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_div])
lemma zmod_zminus1_eq_if:
"(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))"
apply (case_tac "b = 0", simp)
-apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod])
+apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod])
done
lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
@@ -420,91 +407,91 @@
apply (simp add: right_diff_distrib)
done
-lemma self_quotient: "[| quorem((a,a),(q,r)); a \<noteq> (0::int) |] ==> q = 1"
-apply (simp add: split_ifs quorem_def linorder_neq_iff)
+lemma self_quotient: "[| divmod_rel a a (q, r); a \<noteq> (0::int) |] ==> q = 1"
+apply (simp add: split_ifs divmod_rel_def linorder_neq_iff)
apply (rule order_antisym, safe, simp_all)
apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+
done
-lemma self_remainder: "[| quorem((a,a),(q,r)); a \<noteq> (0::int) |] ==> r = 0"
+lemma self_remainder: "[| divmod_rel a a (q, r); a \<noteq> (0::int) |] ==> r = 0"
apply (frule self_quotient, assumption)
-apply (simp add: quorem_def)
+apply (simp add: divmod_rel_def)
done
lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
-by (simp add: quorem_div_mod [THEN self_quotient])
+by (simp add: divmod_rel_div_mod [THEN self_quotient])
(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
lemma zmod_self [simp]: "a mod a = (0::int)"
apply (case_tac "a = 0", simp)
-apply (simp add: quorem_div_mod [THEN self_remainder])
+apply (simp add: divmod_rel_div_mod [THEN self_remainder])
done
subsection{*Computation of Division and Remainder*}
lemma zdiv_zero [simp]: "(0::int) div b = 0"
-by (simp add: div_def divAlg_def)
+by (simp add: div_def divmod_def)
lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
-by (simp add: div_def divAlg_def)
+by (simp add: div_def divmod_def)
lemma zmod_zero [simp]: "(0::int) mod b = 0"
-by (simp add: mod_def divAlg_def)
+by (simp add: mod_def divmod_def)
lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1"
-by (simp add: div_def divAlg_def)
+by (simp add: div_def divmod_def)
lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
-by (simp add: mod_def divAlg_def)
+by (simp add: mod_def divmod_def)
text{*a positive, b positive *}
lemma div_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a div b = fst (posDivAlg a b)"
-by (simp add: div_def divAlg_def)
+by (simp add: div_def divmod_def)
lemma mod_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a mod b = snd (posDivAlg a b)"
-by (simp add: mod_def divAlg_def)
+by (simp add: mod_def divmod_def)
text{*a negative, b positive *}
lemma div_neg_pos: "[| a < 0; 0 < b |] ==> a div b = fst (negDivAlg a b)"
-by (simp add: div_def divAlg_def)
+by (simp add: div_def divmod_def)
lemma mod_neg_pos: "[| a < 0; 0 < b |] ==> a mod b = snd (negDivAlg a b)"
-by (simp add: mod_def divAlg_def)
+by (simp add: mod_def divmod_def)
text{*a positive, b negative *}
lemma div_pos_neg:
"[| 0 < a; b < 0 |] ==> a div b = fst (negateSnd (negDivAlg (-a) (-b)))"
-by (simp add: div_def divAlg_def)
+by (simp add: div_def divmod_def)
lemma mod_pos_neg:
"[| 0 < a; b < 0 |] ==> a mod b = snd (negateSnd (negDivAlg (-a) (-b)))"
-by (simp add: mod_def divAlg_def)
+by (simp add: mod_def divmod_def)
text{*a negative, b negative *}
lemma div_neg_neg:
"[| a < 0; b \<le> 0 |] ==> a div b = fst (negateSnd (posDivAlg (-a) (-b)))"
-by (simp add: div_def divAlg_def)
+by (simp add: div_def divmod_def)
lemma mod_neg_neg:
"[| a < 0; b \<le> 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))"
-by (simp add: mod_def divAlg_def)
+by (simp add: mod_def divmod_def)
text {*Simplify expresions in which div and mod combine numerical constants*}
-lemma quoremI:
+lemma divmod_relI:
"\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk>
- \<Longrightarrow> quorem ((a, b), (q, r))"
- unfolding quorem_def by simp
+ \<Longrightarrow> divmod_rel a b (q, r)"
+ unfolding divmod_rel_def by simp
-lemmas quorem_div_eq = quoremI [THEN quorem_div, THEN eq_reflection]
-lemmas quorem_mod_eq = quoremI [THEN quorem_mod, THEN eq_reflection]
+lemmas divmod_rel_div_eq = divmod_relI [THEN divmod_rel_div, THEN eq_reflection]
+lemmas divmod_rel_mod_eq = divmod_relI [THEN divmod_rel_mod, THEN eq_reflection]
lemmas arithmetic_simps =
arith_simps
add_special
@@ -548,10 +535,10 @@
*}
simproc_setup binary_int_div ("number_of m div number_of n :: int") =
- {* K (divmod_proc (@{thm quorem_div_eq})) *}
+ {* K (divmod_proc (@{thm divmod_rel_div_eq})) *}
simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
- {* K (divmod_proc (@{thm quorem_mod_eq})) *}
+ {* K (divmod_proc (@{thm divmod_rel_mod_eq})) *}
(* The following 8 lemmas are made unnecessary by the above simprocs: *)
@@ -718,18 +705,18 @@
text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
lemma zmult1_lemma:
- "[| quorem((b,c),(q,r)); c \<noteq> 0 |]
- ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
-by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
+ "[| divmod_rel b c (q, r); c \<noteq> 0 |]
+ ==> divmod_rel (a * b) c (a*q + a*r div c, a*r mod c)"
+by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib)
lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
apply (case_tac "c = 0", simp)
-apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
+apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_div])
done
lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
apply (case_tac "c = 0", simp)
-apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
+apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
done
lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c"
@@ -760,20 +747,20 @@
text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
lemma zadd1_lemma:
- "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c \<noteq> 0 |]
- ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
-by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
+ "[| divmod_rel a c (aq, ar); divmod_rel b c (bq, br); c \<noteq> 0 |]
+ ==> divmod_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
+by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib)
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
lemma zdiv_zadd1_eq:
"(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
+apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div)
done
lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
+apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_mod)
done
instance int :: ring_div
@@ -785,6 +772,33 @@
by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
qed auto
+lemma posDivAlg_div_mod:
+ assumes "k \<ge> 0"
+ and "l \<ge> 0"
+ shows "posDivAlg k l = (k div l, k mod l)"
+proof (cases "l = 0")
+ case True then show ?thesis by (simp add: posDivAlg.simps)
+next
+ case False with assms posDivAlg_correct
+ have "divmod_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
+ by simp
+ from divmod_rel_div [OF this `l \<noteq> 0`] divmod_rel_mod [OF this `l \<noteq> 0`]
+ show ?thesis by simp
+qed
+
+lemma negDivAlg_div_mod:
+ assumes "k < 0"
+ and "l > 0"
+ shows "negDivAlg k l = (k div l, k mod l)"
+proof -
+ from assms have "l \<noteq> 0" by simp
+ from assms negDivAlg_correct
+ have "divmod_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
+ by simp
+ from divmod_rel_div [OF this `l \<noteq> 0`] divmod_rel_mod [OF this `l \<noteq> 0`]
+ show ?thesis by simp
+qed
+
lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
by (rule div_add_self1) (* already declared [simp] *)
@@ -862,21 +876,21 @@
add1_zle_eq pos_mod_bound)
done
-lemma zmult2_lemma: "[| quorem ((a,b), (q,r)); b \<noteq> 0; 0 < c |]
- ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
-by (auto simp add: mult_ac quorem_def linorder_neq_iff
+lemma zmult2_lemma: "[| divmod_rel a b (q, r); b \<noteq> 0; 0 < c |]
+ ==> divmod_rel a (b * c) (q div c, b*(q mod c) + r)"
+by (auto simp add: mult_ac divmod_rel_def linorder_neq_iff
zero_less_mult_iff right_distrib [symmetric]
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
apply (case_tac "b = 0", simp)
-apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div])
+apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_div])
done
lemma zmod_zmult2_eq:
"(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
apply (case_tac "b = 0", simp)
-apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod])
+apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_mod])
done
@@ -1360,7 +1374,7 @@
apply (subst split_div, auto)
apply (subst split_zdiv, auto)
apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
-apply (auto simp add: IntDiv.quorem_def of_nat_mult)
+apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
done
lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
@@ -1368,7 +1382,7 @@
apply (subst split_zmod, auto)
apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia
in unique_remainder)
-apply (auto simp add: IntDiv.quorem_def of_nat_mult)
+apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
done
text{*Suggested by Matthias Daum*}
@@ -1429,7 +1443,7 @@
lemma of_int_num [code]:
"of_int k = (if k = 0 then 0 else if k < 0 then
- of_int (- k) else let
- (l, m) = divAlg (k, 2);
+ (l, m) = divmod k 2;
l' = of_int l
in if m = 0 then l' + l' else l' + l' + 1)"
proof -
@@ -1457,7 +1471,7 @@
show "x * of_int 2 = x + x"
unfolding int2 of_int_add right_distrib by simp
qed
- from aux1 show ?thesis by (auto simp add: divAlg_mod_div Let_def aux2 aux3)
+ from aux1 show ?thesis by (auto simp add: divmod_mod_div Let_def aux2 aux3)
qed
end
--- a/src/HOL/IsaMakefile Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/IsaMakefile Wed Jan 28 06:03:46 2009 -0800
@@ -331,10 +331,11 @@
Library/Binomial.thy Library/Eval_Witness.thy \
Library/Code_Index.thy Library/Code_Char.thy \
Library/Code_Char_chr.thy Library/Code_Integer.thy \
- Library/Numeral_Type.thy \
+ Library/Numeral_Type.thy Library/Reflection.thy \
Library/Boolean_Algebra.thy Library/Countable.thy \
Library/RBT.thy Library/Univ_Poly.thy \
- Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML
+ Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
+ Library/reify_data.ML Library/reflection.ML
@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
@@ -809,14 +810,14 @@
ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
- ex/Quickcheck_Examples.thy ex/Reflection.thy ex/reflection_data.ML \
+ ex/Quickcheck_Examples.thy \
ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
ex/Reflected_Presburger.thy ex/coopertac.ML \
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
ex/Subarray.thy ex/Sublist.thy \
ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy \
ex/Unification.thy ex/document/root.bib \
- ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy \
+ ex/document/root.tex ex/Meson_Test.thy ex/set.thy \
ex/svc_funcs.ML ex/svc_test.thy \
ex/ImperativeQuicksort.thy \
ex/BigO_Complex.thy \
@@ -968,7 +969,7 @@
HOL-Word: HOL $(OUT)/HOL-Word
-$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Infinite_Set.thy \
+$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML \
Library/Boolean_Algebra.thy \
Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy \
Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy \
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Jan 28 06:03:46 2009 -0800
@@ -56,10 +56,10 @@
and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
definition divmod_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
- [code del]: "divmod_aux = divmod"
+ [code del]: "divmod_aux = Divides.divmod"
lemma [code]:
- "divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
+ "Divides.divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
unfolding divmod_aux_def divmod_div_mod by simp
lemma divmod_aux_code [code]:
--- a/src/HOL/Library/Library.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Library/Library.thy Wed Jan 28 06:03:46 2009 -0800
@@ -35,6 +35,7 @@
Quicksort
Quotient
Ramsey
+ Reflection
RBT
State_Monad
Univ_Poly
--- a/src/HOL/Library/Nat_Infinity.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Library/Nat_Infinity.thy Wed Jan 28 06:03:46 2009 -0800
@@ -8,17 +8,6 @@
imports Plain "~~/src/HOL/Presburger"
begin
-text {* FIXME: move to Nat.thy *}
-
-instantiation nat :: bot
-begin
-
-definition bot_nat :: nat where
- "bot_nat = 0"
-
-instance proof
-qed (simp add: bot_nat_def)
-
subsection {* Type definition *}
text {*
@@ -26,8 +15,6 @@
infinity.
*}
-end
-
datatype inat = Fin nat | Infty
notation (xsymbols)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Reflection.thy Wed Jan 28 06:03:46 2009 -0800
@@ -0,0 +1,45 @@
+(* Title: HOL/Library/Reflection.thy
+ Author: Amine Chaieb, TU Muenchen
+*)
+
+header {* Generic reflection and reification *}
+
+theory Reflection
+imports Main
+uses "reify_data.ML" ("reflection.ML")
+begin
+
+setup {* Reify_Data.setup *}
+
+lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
+ by (blast intro: ext)
+
+use "reflection.ML"
+
+method_setup reify = {* fn src =>
+ Method.syntax (Attrib.thms --
+ Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
+ (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
+*} "partial automatic reification"
+
+method_setup reflection = {*
+let
+ fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
+ val onlyN = "only";
+ val rulesN = "rules";
+ val any_keyword = keyword onlyN || keyword rulesN;
+ val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+ val terms = thms >> map (term_of o Drule.dest_term);
+ fun optional scan = Scan.optional scan [];
+in fn src =>
+ Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #>
+ (fn (((eqs,ths),to), ctxt) =>
+ let
+ val (ceqs,cths) = Reify_Data.get ctxt
+ val corr_thms = ths@cths
+ val raw_eqs = eqs@ceqs
+ in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to)
+ end) end
+*} "reflection method"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/reflection.ML Wed Jan 28 06:03:46 2009 -0800
@@ -0,0 +1,327 @@
+(* Title: HOL/Library/reflection.ML
+ Author: Amine Chaieb, TU Muenchen
+
+A trial for automatical reification.
+*)
+
+signature REFLECTION =
+sig
+ val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
+ val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
+ val gen_reflection_tac: Proof.context -> (cterm -> thm)
+ -> thm list -> thm list -> term option -> int -> tactic
+end;
+
+structure Reflection : REFLECTION =
+struct
+
+val ext2 = @{thm ext2};
+val nth_Cons_0 = @{thm nth_Cons_0};
+val nth_Cons_Suc = @{thm nth_Cons_Suc};
+
+ (* Make a congruence rule out of a defining equation for the interpretation *)
+ (* th is one defining equation of f, i.e.
+ th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)
+ (* Cp is a constructor pattern and P is a pattern *)
+
+ (* The result is:
+ [|?A1 = f ?t1 ; .. ; ?An= f ?tn |] ==> P (?A1, .., ?An) = f (Cp ?t1 .. ?tn) *)
+ (* + the a list of names of the A1 .. An, Those are fresh in the ctxt*)
+
+
+fun mk_congeq ctxt fs th =
+ let
+ val (f as Const(fN,fT)) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
+ |> fst |> strip_comb |> fst
+ val thy = ProofContext.theory_of ctxt
+ val cert = Thm.cterm_of thy
+ val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt
+ val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
+ fun add_fterms (t as t1 $ t2) =
+ if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
+ else add_fterms t1 #> add_fterms t2
+ | add_fterms (t as Abs(xn,xT,t')) =
+ if exists_Const (fn (c, _) => c = fN) t then (fn _ => [t]) else (fn _ => [])
+ | add_fterms _ = I
+ val fterms = add_fterms rhs []
+ val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt'
+ val tys = map fastype_of fterms
+ val vs = map Free (xs ~~ tys)
+ val env = fterms ~~ vs
+ (* FIXME!!!!*)
+ fun replace_fterms (t as t1 $ t2) =
+ (case AList.lookup (op aconv) env t of
+ SOME v => v
+ | NONE => replace_fterms t1 $ replace_fterms t2)
+ | replace_fterms t = (case AList.lookup (op aconv) env t of
+ SOME v => v
+ | NONE => t)
+
+ fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t)))
+ | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
+ fun tryext x = (x RS ext2 handle THM _ => x)
+ val cong = (Goal.prove ctxt'' [] (map mk_def env)
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
+ (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x))
+ THEN rtac th' 1)) RS sym
+
+ val (cong' :: vars') =
+ Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)
+ val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars'
+
+ in (vs', cong') end;
+ (* congs is a list of pairs (P,th) where th is a theorem for *)
+ (* [| f p1 = A1; ...; f pn = An|] ==> f (C p1 .. pn) = P *)
+val FWD = curry (op OF);
+
+ (* da is the decomposition for atoms, ie. it returns ([],g) where g
+ returns the right instance f (AtC n) = t , where AtC is the Atoms
+ constructor and n is the number of the atom corresponding to t *)
+
+(* Generic decomp for reification : matches the actual term with the
+rhs of one cong rule. The result of the matching guides the
+proof synthesis: The matches of the introduced Variables A1 .. An are
+processed recursively
+ The rest is instantiated in the cong rule,i.e. no reification is needed *)
+
+exception REIF of string;
+
+val bds = ref ([]: (typ * ((term list) * (term list))) list);
+
+fun index_of t =
+ let
+ val tt = HOLogic.listT (fastype_of t)
+ in
+ (case AList.lookup Type.could_unify (!bds) tt of
+ NONE => error "index_of : type not found in environements!"
+ | SOME (tbs,tats) =>
+ let
+ val i = find_index_eq t tats
+ val j = find_index_eq t tbs
+ in (if j= ~1 then
+ if i= ~1
+ then (bds := AList.update Type.could_unify (tt,(tbs,tats@[t])) (!bds) ;
+ length tbs + length tats)
+ else i else j)
+ end)
+ end;
+
+fun dest_listT (Type ("List.list", [T])) = T;
+
+fun decomp_genreif da cgns (t,ctxt) =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val cert = cterm_of thy
+ fun tryabsdecomp (s,ctxt) =
+ (case s of
+ Abs(xn,xT,ta) =>
+ (let
+ val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt
+ val (xn,ta) = variant_abs (xn,xT,ta)
+ val x = Free(xn,xT)
+ val _ = (case AList.lookup Type.could_unify (!bds) (HOLogic.listT xT)
+ of NONE => error "tryabsdecomp: Type not found in the Environement"
+ | SOME (bsT,atsT) =>
+ (bds := AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) (!bds)))
+ in ([(ta, ctxt')] ,
+ fn [th] => ((let val (bsT,asT) = the(AList.lookup Type.could_unify (!bds) (HOLogic.listT xT))
+ in (bds := AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) (!bds))
+ end) ;
+ hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI])))
+ end)
+ | _ => da (s,ctxt))
+ in
+ (case cgns of
+ [] => tryabsdecomp (t,ctxt)
+ | ((vns,cong)::congs) => ((let
+ val cert = cterm_of thy
+ val certy = ctyp_of thy
+ val (tyenv, tmenv) =
+ Pattern.match thy
+ ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
+ (Envir.type_env (Envir.empty 0), Vartab.empty)
+ val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
+ val (fts,its) =
+ (map (snd o snd) fnvs,
+ map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
+ val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
+ in (fts ~~ (replicate (length fts) ctxt), FWD (instantiate (ctyenv, its) cong))
+ end)
+ handle MATCH => decomp_genreif da congs (t,ctxt)))
+ end;
+
+ (* looks for the atoms equation and instantiates it with the right number *)
+
+
+fun mk_decompatom eqs (t,ctxt) =
+let
+ val tT = fastype_of t
+ fun isat eq =
+ let
+ val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
+ in exists_Const
+ (fn (n,ty) => n="List.nth"
+ andalso
+ AList.defined Type.could_unify (!bds) (domain_type ty)) rhs
+ andalso Type.could_unify (fastype_of rhs, tT)
+ end
+ fun get_nths t acc =
+ case t of
+ Const("List.nth",_)$vs$n => insert (fn ((a,_),(b,_)) => a aconv b) (t,(vs,n)) acc
+ | t1$t2 => get_nths t1 (get_nths t2 acc)
+ | Abs(_,_,t') => get_nths t' acc
+ | _ => acc
+
+ fun
+ tryeqs [] = error "Can not find the atoms equation"
+ | tryeqs (eq::eqs) = ((
+ let
+ val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
+ val nths = get_nths rhs []
+ val (vss,ns) = fold_rev (fn (_,(vs,n)) => fn (vss,ns) =>
+ (insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([],[])
+ val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt
+ val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt'
+ val thy = ProofContext.theory_of ctxt''
+ val cert = cterm_of thy
+ val certT = ctyp_of thy
+ val vsns_map = vss ~~ vsns
+ val xns_map = (fst (split_list nths)) ~~ xns
+ val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
+ val rhs_P = subst_free subst rhs
+ val (tyenv, tmenv) = Pattern.match
+ thy (rhs_P, t)
+ (Envir.type_env (Envir.empty 0), Vartab.empty)
+ val sbst = Envir.subst_vars (tyenv, tmenv)
+ val sbsT = Envir.typ_subst_TVars tyenv
+ val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
+ (Vartab.dest tyenv)
+ val tml = Vartab.dest tmenv
+ val t's = map (fn xn => snd (valOf (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*)
+ val subst_ns = map (fn (Const _ $ vs $ n, Var (xn0,T)) =>
+ (cert n, snd (valOf (AList.lookup (op =) tml xn0))
+ |> (index_of #> HOLogic.mk_nat #> cert)))
+ subst
+ val subst_vs =
+ let
+ fun ty (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = (certT T, certT (sbsT T))
+ fun h (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) =
+ let
+ val cns = sbst (Const("List.list.Cons", T --> lT --> lT))
+ val lT' = sbsT lT
+ val (bsT,asT) = the (AList.lookup Type.could_unify (!bds) lT)
+ val vsn = valOf (AList.lookup (op =) vsns_map vs)
+ val cvs = cert (fold_rev (fn x => fn xs => cns$x$xs) bsT (Free (vsn, lT')))
+ in (cert vs, cvs) end
+ in map h subst end
+ val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t))
+ (fold (AList.delete (fn (((a: string),_),(b,_)) => a = b))
+ (map (fn n => (n,0)) xns) tml)
+ val substt =
+ let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[]))
+ in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts) end
+ val th = (instantiate (subst_ty, substt) eq) RS sym
+ in hd (Variable.export ctxt'' ctxt [th]) end)
+ handle MATCH => tryeqs eqs)
+in ([], fn _ => tryeqs (filter isat eqs))
+end;
+
+ (* Generic reification procedure: *)
+ (* creates all needed cong rules and then just uses the theorem synthesis *)
+
+ fun mk_congs ctxt raw_eqs =
+ let
+ val fs = fold_rev (fn eq =>
+ insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop
+ |> HOLogic.dest_eq |> fst |> strip_comb
+ |> fst)) raw_eqs []
+ val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> tl)
+ union ts) fs []
+ val _ = bds := AList.make (fn _ => ([],[])) tys
+ val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt
+ val thy = ProofContext.theory_of ctxt'
+ val cert = cterm_of thy
+ val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t)))))
+ (tys ~~ vs)
+ val is_Var = can dest_Var
+ fun insteq eq vs =
+ let
+ val subst = map (fn (v as Var(n,t)) => (cert v, (valOf o valOf) (AList.lookup (op =) vstys t)))
+ (filter is_Var vs)
+ in Thm.instantiate ([],subst) eq
+ end
+ val eqs = map (fn eq => eq |> prop_of |> HOLogic.dest_Trueprop
+ |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl
+ |> (insteq eq)) raw_eqs
+ val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs)
+in ps ~~ (Variable.export ctxt' ctxt congs)
+end
+
+fun partition P [] = ([],[])
+ | partition P (x::xs) =
+ let val (yes,no) = partition P xs
+ in if P x then (x::yes,no) else (yes, x::no) end
+
+fun rearrange congs =
+let
+ fun P (_, th) =
+ let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th
+ in can dest_Var l end
+ val (yes,no) = partition P congs
+ in no @ yes end
+
+
+
+fun genreif ctxt raw_eqs t =
+ let
+ val congs = rearrange (mk_congs ctxt raw_eqs)
+ val th = divide_and_conquer (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt)
+ fun is_listVar (Var (_,t)) = can dest_listT t
+ | is_listVar _ = false
+ val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
+ |> strip_comb |> snd |> filter is_listVar
+ val cert = cterm_of (ProofContext.theory_of ctxt)
+ val cvs = map (fn (v as Var(n,t)) => (cert v, the (AList.lookup Type.could_unify (!bds) t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
+ val th' = instantiate ([], cvs) th
+ val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
+ val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
+ (fn _ => simp_tac (local_simpset_of ctxt) 1)
+ val _ = bds := []
+in FWD trans [th'',th']
+end
+
+
+fun genreflect ctxt conv corr_thms raw_eqs t =
+let
+ val reifth = genreif ctxt raw_eqs t
+ fun trytrans [] = error "No suitable correctness theorem found"
+ | trytrans (th::ths) =
+ (FWD trans [reifth, th RS sym] handle THM _ => trytrans ths)
+ val th = trytrans corr_thms
+ val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th
+ val rth = conv ft
+in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
+ (simplify (HOL_basic_ss addsimps [rth]) th)
+end
+
+fun genreify_tac ctxt eqs to i = (fn st =>
+ let
+ val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1))
+ val t = (case to of NONE => P | SOME x => x)
+ val th = (genreif ctxt eqs t) RS ssubst
+ in rtac th i st
+ end);
+
+ (* Reflection calls reification and uses the correctness *)
+ (* theorem assumed to be the dead of the list *)
+fun gen_reflection_tac ctxt conv corr_thms raw_eqs to i = (fn st =>
+ let
+ val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1));
+ val t = the_default P to;
+ val th = genreflect ctxt conv corr_thms raw_eqs t
+ RS ssubst;
+ in (rtac th i THEN TRY(rtac TrueI i)) st end);
+
+fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv;
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/reify_data.ML Wed Jan 28 06:03:46 2009 -0800
@@ -0,0 +1,39 @@
+(* Title: HOL/Library/reflection_data.ML
+ Author: Amine Chaieb, TU Muenchen
+
+Data for the reification and reflection methods.
+*)
+
+signature REIFY_DATA =
+sig
+ val get: Proof.context -> thm list * thm list
+ val add: attribute
+ val del: attribute
+ val radd: attribute
+ val rdel: attribute
+ val setup: theory -> theory
+end;
+
+structure Reify_Data : REIFY_DATA =
+struct
+
+structure Data = GenericDataFun
+(
+ type T = thm list * thm list;
+ val empty = ([], []);
+ val extend = I;
+ fun merge _ = pairself Thm.merge_thms;
+);
+
+val get = Data.get o Context.Proof;
+
+val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
+val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
+val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
+val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
+
+val setup = Attrib.add_attributes
+ [("reify", Attrib.add_del_args add del, "Reify data"),
+ ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
+
+end;
--- a/src/HOL/Lubs.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Lubs.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1,5 +1,4 @@
(* Title : Lubs.thy
- ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
*)
@@ -7,7 +6,7 @@
header{*Definitions of Upper Bounds and Least Upper Bounds*}
theory Lubs
-imports Plain
+imports Plain Main
begin
text{*Thanks to suggestions by James Margetson*}
--- a/src/HOL/Nat.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Nat.thy Wed Jan 28 06:03:46 2009 -0800
@@ -425,6 +425,17 @@
end
+instantiation nat :: bot
+begin
+
+definition bot_nat :: nat where
+ "bot_nat = 0"
+
+instance proof
+qed (simp add: bot_nat_def)
+
+end
+
subsubsection {* Introduction properties *}
lemma lessI [iff]: "n < Suc n"
--- a/src/HOL/Parity.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Parity.thy Wed Jan 28 06:03:46 2009 -0800
@@ -5,7 +5,7 @@
header {* Even and Odd for int and nat *}
theory Parity
-imports Plain Presburger
+imports Plain Presburger Main
begin
class even_odd =
--- a/src/HOL/Polynomial.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Polynomial.thy Wed Jan 28 06:03:46 2009 -0800
@@ -6,7 +6,7 @@
header {* Univariate Polynomials *}
theory Polynomial
-imports Plain SetInterval
+imports Plain SetInterval Main
begin
subsection {* Definition of type @{text poly} *}
--- a/src/HOL/Recdef.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Recdef.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1,12 +1,11 @@
(* Title: HOL/Recdef.thy
- ID: $Id$
Author: Konrad Slind and Markus Wenzel, TU Muenchen
*)
header {* TFL: recursive function definitions *}
theory Recdef
-imports FunDef
+imports FunDef Plain
uses
("Tools/TFL/casesplit.ML")
("Tools/TFL/utils.ML")
--- a/src/HOL/Relation_Power.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Relation_Power.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/Relation_Power.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 1996 TU Muenchen
*)
@@ -7,7 +6,7 @@
header{*Powers of Relations and Functions*}
theory Relation_Power
-imports Power Transitive_Closure
+imports Power Transitive_Closure Plain
begin
instance
--- a/src/HOL/Ring_and_Field.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1091,6 +1091,9 @@
"sgn (a * b) = sgn a * sgn b"
by (auto simp add: sgn_if zero_less_mult_iff)
+lemma abs_sgn: "abs k = k * sgn k"
+ unfolding sgn_if abs_if by auto
+
end
class ordered_field = field + ordered_idom
--- a/src/HOL/Tools/ComputeNumeral.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/Tools/ComputeNumeral.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1,5 +1,5 @@
theory ComputeNumeral
-imports ComputeHOL "~~/src/HOL/Real/Float"
+imports ComputeHOL Float
begin
(* normalization of bit strings *)
@@ -151,18 +151,18 @@
by (auto simp only: adjust_def)
lemma negateSnd: "negateSnd (q, r) = (q, -r)"
- by (auto simp only: negateSnd_def)
+ by (simp add: negateSnd_def)
-lemma divAlg: "divAlg (a, b) = (if 0\<le>a then
+lemma divmod: "IntDiv.divmod a b = (if 0\<le>a then
if 0\<le>b then posDivAlg a b
else if a=0 then (0, 0)
else negateSnd (negDivAlg (-a) (-b))
else
if 0<b then negDivAlg a b
else negateSnd (posDivAlg (-a) (-b)))"
- by (auto simp only: divAlg_def)
+ by (auto simp only: IntDiv.divmod_def)
-lemmas compute_div_mod = div_def mod_def divAlg adjust negateSnd posDivAlg.simps negDivAlg.simps
+lemmas compute_div_mod = div_def mod_def divmod adjust negateSnd posDivAlg.simps negDivAlg.simps
--- a/src/HOL/ex/ROOT.ML Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/ex/ROOT.ML Wed Jan 28 06:03:46 2009 -0800
@@ -63,7 +63,6 @@
"Dense_Linear_Order_Ex",
"PresburgerEx",
"Reflected_Presburger",
- "Reflection",
"ReflectionEx",
"BinEx",
"Sqrt",
--- a/src/HOL/ex/Reflection.thy Tue Jan 27 22:39:41 2009 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(*
- ID: $Id$
- Author: Amine Chaieb, TU Muenchen
-*)
-
-header {* Generic reflection and reification *}
-
-theory Reflection
-imports Main
- uses "reflection_data.ML" ("reflection.ML")
-begin
-
-setup {* Reify_Data.setup*}
-
-
-lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
- by (blast intro: ext)
-
-use "reflection.ML"
-
-method_setup reify = {*
- fn src =>
- Method.syntax (Attrib.thms --
- Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
- (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
-*} "partial automatic reification"
-
-method_setup reflection = {*
-let
-fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
-val onlyN = "only";
-val rulesN = "rules";
-val any_keyword = keyword onlyN || keyword rulesN;
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-val terms = thms >> map (term_of o Drule.dest_term);
-fun optional scan = Scan.optional scan [];
-in
-fn src =>
- Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #>
- (fn (((eqs,ths),to), ctxt) =>
- let
- val (ceqs,cths) = Reify_Data.get ctxt
- val corr_thms = ths@cths
- val raw_eqs = eqs@ceqs
- in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to)
- end) end
-*} "reflection method"
-end
--- a/src/HOL/ex/ReflectionEx.thy Tue Jan 27 22:39:41 2009 -0800
+++ b/src/HOL/ex/ReflectionEx.thy Wed Jan 28 06:03:46 2009 -0800
@@ -1,9 +1,9 @@
-(*
- ID: $Id$
+(* Title: HOL/ex/ReflectionEx.thy
Author: Amine Chaieb, TU Muenchen
*)
header {* Examples for generic reflection and reification *}
+
theory ReflectionEx
imports Reflection
begin
--- a/src/HOL/ex/reflection.ML Tue Jan 27 22:39:41 2009 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,325 +0,0 @@
-(* Author: Amine Chaieb, TU Muenchen
-
-A trial for automatical reification.
-*)
-
-signature REFLECTION =
-sig
- val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
- val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
- val gen_reflection_tac: Proof.context -> (cterm -> thm)
- -> thm list -> thm list -> term option -> int -> tactic
-end;
-
-structure Reflection : REFLECTION =
-struct
-
-val ext2 = thm "ext2";
-val nth_Cons_0 = thm "nth_Cons_0";
-val nth_Cons_Suc = thm "nth_Cons_Suc";
-
- (* Make a congruence rule out of a defining equation for the interpretation *)
- (* th is one defining equation of f, i.e.
- th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)
- (* Cp is a constructor pattern and P is a pattern *)
-
- (* The result is:
- [|?A1 = f ?t1 ; .. ; ?An= f ?tn |] ==> P (?A1, .., ?An) = f (Cp ?t1 .. ?tn) *)
- (* + the a list of names of the A1 .. An, Those are fresh in the ctxt*)
-
-
-fun mk_congeq ctxt fs th =
- let
- val (f as Const(fN,fT)) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
- |> fst |> strip_comb |> fst
- val thy = ProofContext.theory_of ctxt
- val cert = Thm.cterm_of thy
- val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt
- val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
- fun add_fterms (t as t1 $ t2) =
- if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
- else add_fterms t1 #> add_fterms t2
- | add_fterms (t as Abs(xn,xT,t')) =
- if exists_Const (fn (c, _) => c = fN) t then (fn _ => [t]) else (fn _ => [])
- | add_fterms _ = I
- val fterms = add_fterms rhs []
- val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt'
- val tys = map fastype_of fterms
- val vs = map Free (xs ~~ tys)
- val env = fterms ~~ vs
- (* FIXME!!!!*)
- fun replace_fterms (t as t1 $ t2) =
- (case AList.lookup (op aconv) env t of
- SOME v => v
- | NONE => replace_fterms t1 $ replace_fterms t2)
- | replace_fterms t = (case AList.lookup (op aconv) env t of
- SOME v => v
- | NONE => t)
-
- fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t)))
- | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
- fun tryext x = (x RS ext2 handle THM _ => x)
- val cong = (Goal.prove ctxt'' [] (map mk_def env)
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
- (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x))
- THEN rtac th' 1)) RS sym
-
- val (cong' :: vars') =
- Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)
- val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars'
-
- in (vs', cong') end;
- (* congs is a list of pairs (P,th) where th is a theorem for *)
- (* [| f p1 = A1; ...; f pn = An|] ==> f (C p1 .. pn) = P *)
-val FWD = curry (op OF);
-
- (* da is the decomposition for atoms, ie. it returns ([],g) where g
- returns the right instance f (AtC n) = t , where AtC is the Atoms
- constructor and n is the number of the atom corresponding to t *)
-
-(* Generic decomp for reification : matches the actual term with the
-rhs of one cong rule. The result of the matching guides the
-proof synthesis: The matches of the introduced Variables A1 .. An are
-processed recursively
- The rest is instantiated in the cong rule,i.e. no reification is needed *)
-
-exception REIF of string;
-
-val bds = ref ([]: (typ * ((term list) * (term list))) list);
-
-fun index_of t =
- let
- val tt = HOLogic.listT (fastype_of t)
- in
- (case AList.lookup Type.could_unify (!bds) tt of
- NONE => error "index_of : type not found in environements!"
- | SOME (tbs,tats) =>
- let
- val i = find_index_eq t tats
- val j = find_index_eq t tbs
- in (if j= ~1 then
- if i= ~1
- then (bds := AList.update Type.could_unify (tt,(tbs,tats@[t])) (!bds) ;
- length tbs + length tats)
- else i else j)
- end)
- end;
-
-fun dest_listT (Type ("List.list", [T])) = T;
-
-fun decomp_genreif da cgns (t,ctxt) =
- let
- val thy = ProofContext.theory_of ctxt
- val cert = cterm_of thy
- fun tryabsdecomp (s,ctxt) =
- (case s of
- Abs(xn,xT,ta) =>
- (let
- val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt
- val (xn,ta) = variant_abs (xn,xT,ta)
- val x = Free(xn,xT)
- val _ = (case AList.lookup Type.could_unify (!bds) (HOLogic.listT xT)
- of NONE => error "tryabsdecomp: Type not found in the Environement"
- | SOME (bsT,atsT) =>
- (bds := AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) (!bds)))
- in ([(ta, ctxt')] ,
- fn [th] => ((let val (bsT,asT) = the(AList.lookup Type.could_unify (!bds) (HOLogic.listT xT))
- in (bds := AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) (!bds))
- end) ;
- hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI])))
- end)
- | _ => da (s,ctxt))
- in
- (case cgns of
- [] => tryabsdecomp (t,ctxt)
- | ((vns,cong)::congs) => ((let
- val cert = cterm_of thy
- val certy = ctyp_of thy
- val (tyenv, tmenv) =
- Pattern.match thy
- ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
- (Envir.type_env (Envir.empty 0), Vartab.empty)
- val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
- val (fts,its) =
- (map (snd o snd) fnvs,
- map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
- val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
- in (fts ~~ (replicate (length fts) ctxt), FWD (instantiate (ctyenv, its) cong))
- end)
- handle MATCH => decomp_genreif da congs (t,ctxt)))
- end;
-
- (* looks for the atoms equation and instantiates it with the right number *)
-
-
-fun mk_decompatom eqs (t,ctxt) =
-let
- val tT = fastype_of t
- fun isat eq =
- let
- val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
- in exists_Const
- (fn (n,ty) => n="List.nth"
- andalso
- AList.defined Type.could_unify (!bds) (domain_type ty)) rhs
- andalso Type.could_unify (fastype_of rhs, tT)
- end
- fun get_nths t acc =
- case t of
- Const("List.nth",_)$vs$n => insert (fn ((a,_),(b,_)) => a aconv b) (t,(vs,n)) acc
- | t1$t2 => get_nths t1 (get_nths t2 acc)
- | Abs(_,_,t') => get_nths t' acc
- | _ => acc
-
- fun
- tryeqs [] = error "Can not find the atoms equation"
- | tryeqs (eq::eqs) = ((
- let
- val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
- val nths = get_nths rhs []
- val (vss,ns) = fold_rev (fn (_,(vs,n)) => fn (vss,ns) =>
- (insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([],[])
- val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt
- val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt'
- val thy = ProofContext.theory_of ctxt''
- val cert = cterm_of thy
- val certT = ctyp_of thy
- val vsns_map = vss ~~ vsns
- val xns_map = (fst (split_list nths)) ~~ xns
- val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
- val rhs_P = subst_free subst rhs
- val (tyenv, tmenv) = Pattern.match
- thy (rhs_P, t)
- (Envir.type_env (Envir.empty 0), Vartab.empty)
- val sbst = Envir.subst_vars (tyenv, tmenv)
- val sbsT = Envir.typ_subst_TVars tyenv
- val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
- (Vartab.dest tyenv)
- val tml = Vartab.dest tmenv
- val t's = map (fn xn => snd (valOf (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*)
- val subst_ns = map (fn (Const _ $ vs $ n, Var (xn0,T)) =>
- (cert n, snd (valOf (AList.lookup (op =) tml xn0))
- |> (index_of #> HOLogic.mk_nat #> cert)))
- subst
- val subst_vs =
- let
- fun ty (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = (certT T, certT (sbsT T))
- fun h (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) =
- let
- val cns = sbst (Const("List.list.Cons", T --> lT --> lT))
- val lT' = sbsT lT
- val (bsT,asT) = the (AList.lookup Type.could_unify (!bds) lT)
- val vsn = valOf (AList.lookup (op =) vsns_map vs)
- val cvs = cert (fold_rev (fn x => fn xs => cns$x$xs) bsT (Free (vsn, lT')))
- in (cert vs, cvs) end
- in map h subst end
- val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t))
- (fold (AList.delete (fn (((a: string),_),(b,_)) => a = b))
- (map (fn n => (n,0)) xns) tml)
- val substt =
- let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[]))
- in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts) end
- val th = (instantiate (subst_ty, substt) eq) RS sym
- in hd (Variable.export ctxt'' ctxt [th]) end)
- handle MATCH => tryeqs eqs)
-in ([], fn _ => tryeqs (filter isat eqs))
-end;
-
- (* Generic reification procedure: *)
- (* creates all needed cong rules and then just uses the theorem synthesis *)
-
- fun mk_congs ctxt raw_eqs =
- let
- val fs = fold_rev (fn eq =>
- insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop
- |> HOLogic.dest_eq |> fst |> strip_comb
- |> fst)) raw_eqs []
- val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> tl)
- union ts) fs []
- val _ = bds := AList.make (fn _ => ([],[])) tys
- val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt
- val thy = ProofContext.theory_of ctxt'
- val cert = cterm_of thy
- val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t)))))
- (tys ~~ vs)
- val is_Var = can dest_Var
- fun insteq eq vs =
- let
- val subst = map (fn (v as Var(n,t)) => (cert v, (valOf o valOf) (AList.lookup (op =) vstys t)))
- (filter is_Var vs)
- in Thm.instantiate ([],subst) eq
- end
- val eqs = map (fn eq => eq |> prop_of |> HOLogic.dest_Trueprop
- |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl
- |> (insteq eq)) raw_eqs
- val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs)
-in ps ~~ (Variable.export ctxt' ctxt congs)
-end
-
-fun partition P [] = ([],[])
- | partition P (x::xs) =
- let val (yes,no) = partition P xs
- in if P x then (x::yes,no) else (yes, x::no) end
-
-fun rearrange congs =
-let
- fun P (_, th) =
- let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th
- in can dest_Var l end
- val (yes,no) = partition P congs
- in no @ yes end
-
-
-
-fun genreif ctxt raw_eqs t =
- let
- val congs = rearrange (mk_congs ctxt raw_eqs)
- val th = divide_and_conquer (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt)
- fun is_listVar (Var (_,t)) = can dest_listT t
- | is_listVar _ = false
- val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
- |> strip_comb |> snd |> filter is_listVar
- val cert = cterm_of (ProofContext.theory_of ctxt)
- val cvs = map (fn (v as Var(n,t)) => (cert v, the (AList.lookup Type.could_unify (!bds) t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
- val th' = instantiate ([], cvs) th
- val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
- val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
- (fn _ => simp_tac (local_simpset_of ctxt) 1)
- val _ = bds := []
-in FWD trans [th'',th']
-end
-
-
-fun genreflect ctxt conv corr_thms raw_eqs t =
-let
- val reifth = genreif ctxt raw_eqs t
- fun trytrans [] = error "No suitable correctness theorem found"
- | trytrans (th::ths) =
- (FWD trans [reifth, th RS sym] handle THM _ => trytrans ths)
- val th = trytrans corr_thms
- val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th
- val rth = conv ft
-in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
- (simplify (HOL_basic_ss addsimps [rth]) th)
-end
-
-fun genreify_tac ctxt eqs to i = (fn st =>
- let
- val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1))
- val t = (case to of NONE => P | SOME x => x)
- val th = (genreif ctxt eqs t) RS ssubst
- in rtac th i st
- end);
-
- (* Reflection calls reification and uses the correctness *)
- (* theorem assumed to be the dead of the list *)
-fun gen_reflection_tac ctxt conv corr_thms raw_eqs to i = (fn st =>
- let
- val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1));
- val t = the_default P to;
- val th = genreflect ctxt conv corr_thms raw_eqs t
- RS ssubst;
- in (rtac th i THEN TRY(rtac TrueI i)) st end);
-
-fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv;
-end
--- a/src/HOL/ex/reflection_data.ML Tue Jan 27 22:39:41 2009 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* Title: HOL/ex/reflection_data.ML
- ID: $Id$
- Author: Amine Chaieb, TU Muenchen
-
-Data for the reification and reflection methods.
-*)
-
-signature REIFY_DATA =
-sig
- type entry = thm list * thm list
- val get: Proof.context -> entry
- val del: attribute
- val add: attribute
- val setup: theory -> theory
-end;
-
-structure Reify_Data : REIFY_DATA =
-struct
-
-type entry = thm list * thm list;
-
-structure Data = GenericDataFun
-(
- type T = entry
- val empty = ([], [])
- val extend = I
- fun merge _ = pairself Thm.merge_thms
-);
-
-val get = Data.get o Context.Proof;
-
-val add = Thm.declaration_attribute (fn th => fn context =>
- context |> Data.map (apfst (Thm.add_thm th)))
-
-val del = Thm.declaration_attribute (fn th => fn context =>
- context |> Data.map (apfst (Thm.del_thm th)))
-
-val radd = Thm.declaration_attribute (fn th => fn context =>
- context |> Data.map (apsnd (Thm.add_thm th)))
-
-val rdel = Thm.declaration_attribute (fn th => fn context =>
- context |> Data.map (apsnd (Thm.del_thm th)))
-
-(* concrete syntax *)
-(*
-local
-fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
-
-val constsN = "consts";
-val addN = "add";
-val delN = "del";
-val any_keyword = keyword constsN || keyword addN || keyword delN;
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-val terms = thms >> map (term_of o Drule.dest_term);
-
-fun optional scan = Scan.optional scan [];
-
-in
-val att_syntax = Attrib.syntax
- ((Scan.lift (Args.$$$ "del") |-- thms) >> del ||
- optional (keyword addN |-- thms) >> add)
-end;
-*)
-
-(* theory setup *)
- val setup =
- Attrib.add_attributes [("reify", Attrib.add_del_args add del, "Reify data"),
- ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
-end;
--- a/src/Pure/General/swing.scala Tue Jan 27 22:39:41 2009 -0800
+++ b/src/Pure/General/swing.scala Wed Jan 28 06:03:46 2009 -0800
@@ -10,9 +10,13 @@
object Swing
{
- def now(body: => Unit) =
- SwingUtilities.invokeAndWait(new Runnable { def run = body })
+ def now(body: => Unit) {
+ if (SwingUtilities.isEventDispatchThread) body
+ else SwingUtilities.invokeAndWait(new Runnable { def run = body })
+ }
- def later(body: => Unit) =
- SwingUtilities.invokeLater(new Runnable { def run = body })
+ def later(body: => Unit) {
+ if (SwingUtilities.isEventDispatchThread) body
+ else SwingUtilities.invokeLater(new Runnable { def run = body })
+ }
}
--- a/src/Pure/Tools/isabelle_process.scala Tue Jan 27 22:39:41 2009 -0800
+++ b/src/Pure/Tools/isabelle_process.scala Wed Jan 28 06:03:46 2009 -0800
@@ -118,10 +118,10 @@
/* process information */
- private var proc: Process = null
- private var closing = false
- private var pid: String = null
- private var the_session: String = null
+ @volatile private var proc: Process = null
+ @volatile private var closing = false
+ @volatile private var pid: String = null
+ @volatile private var the_session: String = null
def session = the_session