# HG changeset patch # User haftmann # Date 1233146184 -3600 # Node ID f2584b0c76b5466ce88005b7358a97bd453cfad1 # Parent 8b0c1397868e7b46bc8d6066654e5562be216347# Parent 881f328dfbb35614643408c743bf88ceb055283d merged diff -r 8b0c1397868e -r f2584b0c76b5 NEWS --- a/NEWS Wed Jan 28 11:36:45 2009 +0100 +++ b/NEWS Wed Jan 28 13:36:24 2009 +0100 @@ -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 diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/ATP_Linkup.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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" diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Dense_Linear_Order.thy --- a/src/HOL/Dense_Linear_Order.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Dense_Linear_Order.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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" diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Equiv_Relations.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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 *} diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/GCD.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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 {* diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Hilbert_Choice.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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 diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/IntDiv.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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 \ int \ int \ int \ bool" where --{*definition of quotient and remainder*} - [code]: "quorem == %((a,b), (q,r)). - a = b*q + r & - (if 0 int*int" +definition adjust :: "int \ int \ int \ int \ int" where --{*for the division algorithm*} - [code]: "adjust b == %(q,r). if 0 \ r-b then (2*q + 1, r-b) - else (2*q, r)" + [code]: "adjust b = (\(q, r). if 0 \ r - b then (2 * q + 1, r - b) + else (2 * q, r))" text{*algorithm for the case @{text "a\0, b>0"}*} -function - posDivAlg :: "int \ int \ int \ int" -where - "posDivAlg a b = - (if (a0) then (0,a) - else adjust b (posDivAlg a (2*b)))" +function posDivAlg :: "int \ int \ int \ int" where + "posDivAlg a b = (if a < b \ b \ 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 (\(a, b). nat (a - b + 1))") auto text{*algorithm for the case @{text "a<0, b>0"}*} -function - negDivAlg :: "int \ int \ int \ int" -where - "negDivAlg a b = - (if (0\a+b | b\0) then (-1,a+b) - else adjust b (negDivAlg a (2*b)))" +function negDivAlg :: "int \ int \ int \ int" where + "negDivAlg a b = (if 0 \a + b \ b \ 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 (\(a, b). nat (- a - b))") auto text{*algorithm for the general case @{term "b\0"}*} -constdefs - negateSnd :: "int*int => int*int" - [code]: "negateSnd == %(q,r). (q,-r)" +definition negateSnd :: "int \ int \ int \ int" where + [code inline]: "negateSnd = apsnd uminus" -definition - divAlg :: "int \ int \ int \ int" +definition divmod :: "int \ int \ int \ 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 = (\(a, b). (if 0\a then - if 0\b then posDivAlg a b - else if a=0 then (0, 0) + "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 0a then + fun divmod (a,b) = if 0\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 \ 0 |] + "[| divmod_rel a b (q, r); divmod_rel a b (q', r'); b \ 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 \ 0 |] + "[| divmod_rel a b (q, r); divmod_rel a b (q', r'); b \ 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 \ 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\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 \ 0 ==> quorem ((0,b), (0,0))" -by (auto simp add: quorem_def linorder_neq_iff) +lemma divmod_rel_0: "b \ 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 \ 0 ==> quorem ((a,b), divAlg (a, b))" -by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg +lemma divmod_correct: "b \ 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) 0 \ 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 \ 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 \ 0 ==> quorem ((a, b), (a div b, a mod b))" +lemma divmod_rel_div_mod: "b \ 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 \ 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 \ 0 |] ==> a div b = q" +by (simp add: divmod_rel_div_mod [THEN unique_quotient]) -lemma quorem_mod: "[| quorem((a,b),(q,r)); b \ 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 \ 0 |] ==> a mod b = r" +by (simp add: divmod_rel_div_mod [THEN unique_remainder]) lemma div_pos_pos_trivial: "[| (0::int) \ a; 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_neg_neg_trivial: "[| a \ (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 \ 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) \ a; 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_neg_neg_trivial: "[| a \ (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 \ 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 \ (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 \ (0::int) |] ==> q = 1" -apply (simp add: split_ifs quorem_def linorder_neq_iff) +lemma self_quotient: "[| divmod_rel a a (q, r); a \ (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 \ (0::int) |] ==> r = 0" +lemma self_remainder: "[| divmod_rel a a (q, r); a \ (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 \ 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) -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) -1 div b = -1" -by (simp add: div_def divAlg_def) +by (simp add: div_def divmod_def) lemma zmod_minus1: "(0::int) -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 \ 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 \ 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 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 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 \ 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 \ 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: "\a == b * q + r; if 0 < b then 0 \ r \ r < b else b < r \ r \ 0\ - \ quorem ((a, b), (q, r))" - unfolding quorem_def by simp + \ 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 \ 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 \ 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 \ 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 \ 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 \ 0" + and "l \ 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 \ 0`] divmod_rel_mod [OF this `l \ 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 \ 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 \ 0`] divmod_rel_mod [OF this `l \ 0`] + show ?thesis by simp +qed + lemma zdiv_zadd_self1: "a \ (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 \ 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 \ 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 diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/IsaMakefile Wed Jan 28 13:36:24 2009 +0100 @@ -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 \ diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Library/Efficient_Nat.thy Wed Jan 28 13:36:24 2009 +0100 @@ -56,10 +56,10 @@ and @{term "op mod \ nat \ nat \ nat"} operations. *} definition divmod_aux :: "nat \ nat \ nat \ 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]: diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Library/Library.thy Wed Jan 28 13:36:24 2009 +0100 @@ -35,6 +35,7 @@ Quicksort Quotient Ramsey + Reflection RBT State_Monad Univ_Poly diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Library/Nat_Infinity.thy --- a/src/HOL/Library/Nat_Infinity.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Library/Nat_Infinity.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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) diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Library/Reflection.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Reflection.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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: "(\x. f x = g x) \ 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 diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Library/reflection.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/reflection.ML Wed Jan 28 13:36:24 2009 +0100 @@ -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 diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Library/reify_data.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/reify_data.ML Wed Jan 28 13:36:24 2009 +0100 @@ -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; diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Lubs.thy --- a/src/HOL/Lubs.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Lubs.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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*} diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Nat.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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" diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Parity.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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 = diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Polynomial.thy --- a/src/HOL/Polynomial.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Polynomial.thy Wed Jan 28 13:36:24 2009 +0100 @@ -6,7 +6,7 @@ header {* Univariate Polynomials *} theory Polynomial -imports Plain SetInterval +imports Plain SetInterval Main begin subsection {* Definition of type @{text poly} *} diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Recdef.thy --- a/src/HOL/Recdef.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Recdef.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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") diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Relation_Power.thy --- a/src/HOL/Relation_Power.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Relation_Power.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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 diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Ring_and_Field.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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 diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/Tools/ComputeNumeral.thy --- a/src/HOL/Tools/ComputeNumeral.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/Tools/ComputeNumeral.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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\a then +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 0x. f x = g x) \ 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 diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/ex/ReflectionEx.thy --- a/src/HOL/ex/ReflectionEx.thy Wed Jan 28 11:36:45 2009 +0100 +++ b/src/HOL/ex/ReflectionEx.thy Wed Jan 28 13:36:24 2009 +0100 @@ -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 diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/ex/reflection.ML --- a/src/HOL/ex/reflection.ML Wed Jan 28 11:36:45 2009 +0100 +++ /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 diff -r 8b0c1397868e -r f2584b0c76b5 src/HOL/ex/reflection_data.ML --- a/src/HOL/ex/reflection_data.ML Wed Jan 28 11:36:45 2009 +0100 +++ /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;