Branch merge with updates from mainline isabelle.
authorThomas Sewell <tsewell@nicta.com.au>
Thu Sep 17 14:17:37 2009 +1000 (2009-09-17)
changeset 32750c876bcb601fc
parent 32749 3282c12a856c
parent 32592 e29c0b7dcf66
child 32751 5b65449d7669
Branch merge with updates from mainline isabelle.
src/HOL/NatTransfer.thy
src/HOL/Tools/transfer_data.ML
     1.1 --- a/NEWS	Fri Sep 11 20:58:29 2009 +1000
     1.2 +++ b/NEWS	Thu Sep 17 14:17:37 2009 +1000
     1.3 @@ -41,14 +41,6 @@
     1.4  semidefinite programming solvers.  For more information and examples
     1.5  see src/HOL/Library/Sum_Of_Squares.
     1.6  
     1.7 -* Set.UNIV and Set.empty are mere abbreviations for top and bot.
     1.8 -INCOMPATIBILITY.
     1.9 -
    1.10 -* More convenient names for set intersection and union.
    1.11 -INCOMPATIBILITY:
    1.12 -    Set.Int ~>  Set.inter
    1.13 -    Set.Un ~>   Set.union
    1.14 -
    1.15  * Code generator attributes follow the usual underscore convention:
    1.16      code_unfold     replaces    code unfold
    1.17      code_post       replaces    code post
    1.18 @@ -57,16 +49,14 @@
    1.19  
    1.20  * New class "boolean_algebra".
    1.21  
    1.22 -* Refinements to lattices classes:
    1.23 -  - added boolean_algebra type class
    1.24 +* Refinements to lattice classes and sets:
    1.25    - less default intro/elim rules in locale variant, more default
    1.26      intro/elim rules in class variant: more uniformity
    1.27    - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
    1.28    - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
    1.29    - renamed ACI to inf_sup_aci
    1.30    - class "complete_lattice" moved to separate theory "complete_lattice";
    1.31 -    corresponding constants renamed:
    1.32 -    
    1.33 +    corresponding constants (and abbreviations) renamed:
    1.34      Set.Inf ~>      Complete_Lattice.Inf
    1.35      Set.Sup ~>      Complete_Lattice.Sup
    1.36      Set.INFI ~>     Complete_Lattice.INFI
    1.37 @@ -75,6 +65,14 @@
    1.38      Set.Union ~>    Complete_Lattice.Union
    1.39      Set.INTER ~>    Complete_Lattice.INTER
    1.40      Set.UNION ~>    Complete_Lattice.UNION
    1.41 +  - more convenient names for set intersection and union:
    1.42 +    Set.Int ~>  Set.inter
    1.43 +    Set.Un ~>   Set.union
    1.44 +  - mere abbreviations:
    1.45 +    Set.empty               (for bot)
    1.46 +    Set.UNIV                (for top)
    1.47 +    Complete_Lattice.Inter  (for Inf)
    1.48 +    Complete_Lattice.Union  (for Sup)
    1.49  
    1.50    INCOMPATIBILITY.
    1.51  
    1.52 @@ -87,7 +85,7 @@
    1.53  INCOMPATIBILITY.
    1.54  
    1.55  * Power operations on relations and functions are now one dedicate
    1.56 -constant compow with infix syntax "^^".  Power operations on
    1.57 +constant "compow" with infix syntax "^^".  Power operations on
    1.58  multiplicative monoids retains syntax "^" and is now defined generic
    1.59  in class power.  INCOMPATIBILITY.
    1.60  
     2.1 --- a/doc-src/manual.bib	Fri Sep 11 20:58:29 2009 +1000
     2.2 +++ b/doc-src/manual.bib	Thu Sep 17 14:17:37 2009 +1000
     2.3 @@ -484,7 +484,7 @@
     2.4    booktitle     = {Types for Proofs and Programs, TYPES 2008},
     2.5    publisher     = {Springer},
     2.6    series        = {LNCS},
     2.7 -  volume        = {????},
     2.8 +  volume        = {5497},
     2.9    year          = {2009}
    2.10  }
    2.11  
     3.1 --- a/src/HOL/Complete_Lattice.thy	Fri Sep 11 20:58:29 2009 +1000
     3.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Sep 17 14:17:37 2009 +1000
     3.3 @@ -203,8 +203,8 @@
     3.4  
     3.5  subsection {* Union *}
     3.6  
     3.7 -definition Union :: "'a set set \<Rightarrow> 'a set" where
     3.8 -  Sup_set_eq [symmetric]: "Union S = \<Squnion>S"
     3.9 +abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
    3.10 +  "Union S \<equiv> \<Squnion>S"
    3.11  
    3.12  notation (xsymbols)
    3.13    Union  ("\<Union>_" [90] 90)
    3.14 @@ -216,7 +216,7 @@
    3.15    have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
    3.16      by auto
    3.17    then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
    3.18 -    by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)
    3.19 +    by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
    3.20  qed
    3.21  
    3.22  lemma Union_iff [simp, noatp]:
    3.23 @@ -314,7 +314,7 @@
    3.24  
    3.25  lemma UNION_eq_Union_image:
    3.26    "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
    3.27 -  by (simp add: SUPR_def SUPR_set_eq [symmetric] Sup_set_eq)
    3.28 +  by (simp add: SUPR_def SUPR_set_eq [symmetric])
    3.29  
    3.30  lemma Union_def:
    3.31    "\<Union>S = (\<Union>x\<in>S. x)"
    3.32 @@ -439,8 +439,8 @@
    3.33  
    3.34  subsection {* Inter *}
    3.35  
    3.36 -definition Inter :: "'a set set \<Rightarrow> 'a set" where
    3.37 -  Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"
    3.38 +abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
    3.39 +  "Inter S \<equiv> \<Sqinter>S"
    3.40    
    3.41  notation (xsymbols)
    3.42    Inter  ("\<Inter>_" [90] 90)
    3.43 @@ -452,7 +452,7 @@
    3.44    have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
    3.45      by auto
    3.46    then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
    3.47 -    by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)
    3.48 +    by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
    3.49  qed
    3.50  
    3.51  lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
    3.52 @@ -541,7 +541,7 @@
    3.53  
    3.54  lemma INTER_eq_Inter_image:
    3.55    "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
    3.56 -  by (simp add: INFI_def INFI_set_eq [symmetric] Inf_set_eq)
    3.57 +  by (simp add: INFI_def INFI_set_eq [symmetric])
    3.58    
    3.59  lemma Inter_def:
    3.60    "\<Inter>S = (\<Inter>x\<in>S. x)"
     4.1 --- a/src/HOL/Fact.thy	Fri Sep 11 20:58:29 2009 +1000
     4.2 +++ b/src/HOL/Fact.thy	Thu Sep 17 14:17:37 2009 +1000
     4.3 @@ -8,7 +8,7 @@
     4.4  header{*Factorial Function*}
     4.5  
     4.6  theory Fact
     4.7 -imports NatTransfer
     4.8 +imports Nat_Transfer
     4.9  begin
    4.10  
    4.11  class fact =
     5.1 --- a/src/HOL/Fun.thy	Fri Sep 11 20:58:29 2009 +1000
     5.2 +++ b/src/HOL/Fun.thy	Thu Sep 17 14:17:37 2009 +1000
     5.3 @@ -7,6 +7,7 @@
     5.4  
     5.5  theory Fun
     5.6  imports Complete_Lattice
     5.7 +uses ("Tools/transfer.ML")
     5.8  begin
     5.9  
    5.10  text{*As a simplification rule, it replaces all function equalities by
    5.11 @@ -568,6 +569,16 @@
    5.12  *}
    5.13  
    5.14  
    5.15 +subsection {* Generic transfer procedure *}
    5.16 +
    5.17 +definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
    5.18 +  where "TransferMorphism a B \<longleftrightarrow> True"
    5.19 +
    5.20 +use "Tools/transfer.ML"
    5.21 +
    5.22 +setup Transfer.setup
    5.23 +
    5.24 +
    5.25  subsection {* Code generator setup *}
    5.26  
    5.27  types_code
     6.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Sep 11 20:58:29 2009 +1000
     6.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Thu Sep 17 14:17:37 2009 +1000
     6.3 @@ -176,12 +176,11 @@
     6.4  
     6.5  code_type array (OCaml "_/ array")
     6.6  code_const Array (OCaml "failwith/ \"bare Array\"")
     6.7 -code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
     6.8 +code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
     6.9  code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
    6.10 -code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)")
    6.11 -code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)")
    6.12 -code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)")
    6.13 -code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)")
    6.14 +code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
    6.15 +code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
    6.16 +code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
    6.17  
    6.18  code_reserved OCaml Array
    6.19  
     7.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Fri Sep 11 20:58:29 2009 +1000
     7.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Thu Sep 17 14:17:37 2009 +1000
     7.3 @@ -1,4 +1,3 @@
     7.4 -(* $Id$ *)
     7.5  
     7.6  header {* Slices of lists *}
     7.7  
     7.8 @@ -6,7 +5,6 @@
     7.9  imports Multiset
    7.10  begin
    7.11  
    7.12 -
    7.13  lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
    7.14  apply (induct xs arbitrary: i j k)
    7.15  apply simp
     8.1 --- a/src/HOL/Inductive.thy	Fri Sep 11 20:58:29 2009 +1000
     8.2 +++ b/src/HOL/Inductive.thy	Thu Sep 17 14:17:37 2009 +1000
     8.3 @@ -111,8 +111,7 @@
     8.4    and P_f: "!!S. P S ==> P(f S)"
     8.5    and P_Union: "!!M. !S:M. P S ==> P(Union M)"
     8.6    shows "P(lfp f)"
     8.7 -  using assms unfolding Sup_set_eq [symmetric]
     8.8 -  by (rule lfp_ordinal_induct [where P=P])
     8.9 +  using assms by (rule lfp_ordinal_induct [where P=P])
    8.10  
    8.11  
    8.12  text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
     9.1 --- a/src/HOL/IntDiv.thy	Fri Sep 11 20:58:29 2009 +1000
     9.2 +++ b/src/HOL/IntDiv.thy	Thu Sep 17 14:17:37 2009 +1000
     9.3 @@ -1102,20 +1102,6 @@
     9.4    thus ?thesis by simp
     9.5  qed
     9.6  
     9.7 -
     9.8 -theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
     9.9 -apply (simp split add: split_nat)
    9.10 -apply (rule iffI)
    9.11 -apply (erule exE)
    9.12 -apply (rule_tac x = "int x" in exI)
    9.13 -apply simp
    9.14 -apply (erule exE)
    9.15 -apply (rule_tac x = "nat x" in exI)
    9.16 -apply (erule conjE)
    9.17 -apply (erule_tac x = "nat x" in allE)
    9.18 -apply simp
    9.19 -done
    9.20 -
    9.21  theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
    9.22  proof -
    9.23    have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
    10.1 --- a/src/HOL/IsaMakefile	Fri Sep 11 20:58:29 2009 +1000
    10.2 +++ b/src/HOL/IsaMakefile	Thu Sep 17 14:17:37 2009 +1000
    10.3 @@ -291,7 +291,7 @@
    10.4    Log.thy \
    10.5    Lubs.thy \
    10.6    MacLaurin.thy \
    10.7 -  NatTransfer.thy \
    10.8 +  Nat_Transfer.thy \
    10.9    NthRoot.thy \
   10.10    SEQ.thy \
   10.11    Series.thy \
   10.12 @@ -306,7 +306,7 @@
   10.13    Real.thy \
   10.14    RealVector.thy \
   10.15    Tools/float_syntax.ML \
   10.16 -  Tools/transfer_data.ML \
   10.17 +  Tools/transfer.ML \
   10.18    Tools/Qelim/ferrante_rackoff_data.ML \
   10.19    Tools/Qelim/ferrante_rackoff.ML \
   10.20    Tools/Qelim/langford_data.ML \
   10.21 @@ -901,7 +901,7 @@
   10.22    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
   10.23    ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
   10.24    ex/Sudoku.thy ex/Tarski.thy \
   10.25 -  ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
   10.26 +  ex/Termination.thy ex/Transfer_Ex.thy ex/Unification.thy ex/document/root.bib		\
   10.27    ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
   10.28    ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
   10.29  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
    11.1 --- a/src/HOL/Lattices.thy	Fri Sep 11 20:58:29 2009 +1000
    11.2 +++ b/src/HOL/Lattices.thy	Thu Sep 17 14:17:37 2009 +1000
    11.3 @@ -12,7 +12,9 @@
    11.4  
    11.5  notation
    11.6    less_eq  (infix "\<sqsubseteq>" 50) and
    11.7 -  less  (infix "\<sqsubset>" 50)
    11.8 +  less  (infix "\<sqsubset>" 50) and
    11.9 +  top ("\<top>") and
   11.10 +  bot ("\<bottom>")
   11.11  
   11.12  class lower_semilattice = order +
   11.13    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
   11.14 @@ -220,6 +222,46 @@
   11.15  
   11.16  end
   11.17  
   11.18 +subsubsection {* Strict order *}
   11.19 +
   11.20 +context lower_semilattice
   11.21 +begin
   11.22 +
   11.23 +lemma less_infI1:
   11.24 +  "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   11.25 +  by (auto simp add: less_le intro: le_infI1)
   11.26 +
   11.27 +lemma less_infI2:
   11.28 +  "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   11.29 +  by (auto simp add: less_le intro: le_infI2)
   11.30 +
   11.31 +end
   11.32 +
   11.33 +context upper_semilattice
   11.34 +begin
   11.35 +
   11.36 +lemma less_supI1:
   11.37 +  "x < a \<Longrightarrow> x < a \<squnion> b"
   11.38 +proof -
   11.39 +  interpret dual: lower_semilattice "op \<ge>" "op >" sup
   11.40 +    by (fact dual_semilattice)
   11.41 +  assume "x < a"
   11.42 +  then show "x < a \<squnion> b"
   11.43 +    by (fact dual.less_infI1)
   11.44 +qed
   11.45 +
   11.46 +lemma less_supI2:
   11.47 +  "x < b \<Longrightarrow> x < a \<squnion> b"
   11.48 +proof -
   11.49 +  interpret dual: lower_semilattice "op \<ge>" "op >" sup
   11.50 +    by (fact dual_semilattice)
   11.51 +  assume "x < b"
   11.52 +  then show "x < a \<squnion> b"
   11.53 +    by (fact dual.less_infI2)
   11.54 +qed
   11.55 +
   11.56 +end
   11.57 +
   11.58  
   11.59  subsection {* Distributive lattices *}
   11.60  
   11.61 @@ -306,6 +348,40 @@
   11.62    "x \<squnion> bot = x"
   11.63    by (rule sup_absorb1) simp
   11.64  
   11.65 +lemma inf_eq_top_eq1:
   11.66 +  assumes "A \<sqinter> B = \<top>"
   11.67 +  shows "A = \<top>"
   11.68 +proof (cases "B = \<top>")
   11.69 +  case True with assms show ?thesis by simp
   11.70 +next
   11.71 +  case False with top_greatest have "B < \<top>" by (auto intro: neq_le_trans)
   11.72 +  then have "A \<sqinter> B < \<top>" by (rule less_infI2)
   11.73 +  with assms show ?thesis by simp
   11.74 +qed
   11.75 +
   11.76 +lemma inf_eq_top_eq2:
   11.77 +  assumes "A \<sqinter> B = \<top>"
   11.78 +  shows "B = \<top>"
   11.79 +  by (rule inf_eq_top_eq1, unfold inf_commute [of B]) (fact assms)
   11.80 +
   11.81 +lemma sup_eq_bot_eq1:
   11.82 +  assumes "A \<squnion> B = \<bottom>"
   11.83 +  shows "A = \<bottom>"
   11.84 +proof -
   11.85 +  interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
   11.86 +    by (rule dual_boolean_algebra)
   11.87 +  from dual.inf_eq_top_eq1 assms show ?thesis .
   11.88 +qed
   11.89 +
   11.90 +lemma sup_eq_bot_eq2:
   11.91 +  assumes "A \<squnion> B = \<bottom>"
   11.92 +  shows "B = \<bottom>"
   11.93 +proof -
   11.94 +  interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
   11.95 +    by (rule dual_boolean_algebra)
   11.96 +  from dual.inf_eq_top_eq2 assms show ?thesis .
   11.97 +qed
   11.98 +
   11.99  lemma compl_unique:
  11.100    assumes "x \<sqinter> y = bot"
  11.101      and "x \<squnion> y = top"
  11.102 @@ -517,6 +593,8 @@
  11.103    less_eq  (infix "\<sqsubseteq>" 50) and
  11.104    less (infix "\<sqsubset>" 50) and
  11.105    inf  (infixl "\<sqinter>" 70) and
  11.106 -  sup  (infixl "\<squnion>" 65)
  11.107 +  sup  (infixl "\<squnion>" 65) and
  11.108 +  top ("\<top>") and
  11.109 +  bot ("\<bottom>")
  11.110  
  11.111  end
    12.1 --- a/src/HOL/Library/Executable_Set.thy	Fri Sep 11 20:58:29 2009 +1000
    12.2 +++ b/src/HOL/Library/Executable_Set.thy	Thu Sep 17 14:17:37 2009 +1000
    12.3 @@ -8,7 +8,7 @@
    12.4  imports Main Fset
    12.5  begin
    12.6  
    12.7 -subsection {* Derived set operations *}
    12.8 +subsection {* Preprocessor setup *}
    12.9  
   12.10  declare member [code] 
   12.11  
   12.12 @@ -24,9 +24,7 @@
   12.13  definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   12.14    [code del]: "eq_set = op ="
   12.15  
   12.16 -(* FIXME allow for Stefan's code generator:
   12.17 -declare set_eq_subset[code_unfold]
   12.18 -*)
   12.19 +(*declare eq_set_def [symmetric, code_unfold]*)
   12.20  
   12.21  lemma [code]:
   12.22    "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   12.23 @@ -37,13 +35,20 @@
   12.24  declare Inter_image_eq [symmetric, code]
   12.25  declare Union_image_eq [symmetric, code]
   12.26  
   12.27 -
   12.28 -subsection {* Rewrites for primitive operations *}
   12.29 -
   12.30  declare List_Set.project_def [symmetric, code_unfold]
   12.31  
   12.32 +definition Inter :: "'a set set \<Rightarrow> 'a set" where
   12.33 +  "Inter = Complete_Lattice.Inter"
   12.34  
   12.35 -subsection {* code generator setup *}
   12.36 +declare Inter_def [symmetric, code_unfold]
   12.37 +
   12.38 +definition Union :: "'a set set \<Rightarrow> 'a set" where
   12.39 +  "Union = Complete_Lattice.Union"
   12.40 +
   12.41 +declare Union_def [symmetric, code_unfold]
   12.42 +
   12.43 +
   12.44 +subsection {* Code generator setup *}
   12.45  
   12.46  ML {*
   12.47  nonfix inter;
   12.48 @@ -75,8 +80,8 @@
   12.49    "op \<union>"              ("{*Fset.union*}")
   12.50    "op \<inter>"              ("{*Fset.inter*}")
   12.51    "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
   12.52 -  "Complete_Lattice.Union" ("{*Fset.Union*}")
   12.53 -  "Complete_Lattice.Inter" ("{*Fset.Inter*}")
   12.54 +  "Union"             ("{*Fset.Union*}")
   12.55 +  "Inter"             ("{*Fset.Inter*}")
   12.56    card                ("{*Fset.card*}")
   12.57    fold                ("{*foldl o flip*}")
   12.58  
    13.1 --- a/src/HOL/Mirabelle/Mirabelle.thy	Fri Sep 11 20:58:29 2009 +1000
    13.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Thu Sep 17 14:17:37 2009 +1000
    13.3 @@ -1,5 +1,5 @@
    13.4 -(* Title: Mirabelle.thy
    13.5 -   Author: Jasmin Blanchette and Sascha Boehme
    13.6 +(*  Title:      HOL/Mirabelle/Mirabelle.thy
    13.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
    13.8  *)
    13.9  
   13.10  theory Mirabelle
    14.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Fri Sep 11 20:58:29 2009 +1000
    14.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Thu Sep 17 14:17:37 2009 +1000
    14.3 @@ -1,5 +1,5 @@
    14.4 -(* Title: Mirabelle_Test.thy
    14.5 -   Author: Sascha Boehme
    14.6 +(*  Title:      HOL/Mirabelle/Mirabelle_Test.thy
    14.7 +    Author:     Sascha Boehme, TU Munich
    14.8  *)
    14.9  
   14.10  header {* Simple test theory for Mirabelle actions *}
   14.11 @@ -14,9 +14,9 @@
   14.12    "Tools/mirabelle_sledgehammer.ML"
   14.13  begin
   14.14  
   14.15 -(*
   14.16 -  only perform type-checking of the actions,
   14.17 -  any reasonable test would be too complicated
   14.18 -*)
   14.19 +text {*
   14.20 +  Only perform type-checking of the actions,
   14.21 +  any reasonable test would be too complicated.
   14.22 +*}
   14.23  
   14.24  end
    15.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Sep 11 20:58:29 2009 +1000
    15.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 17 14:17:37 2009 +1000
    15.3 @@ -1,27 +1,30 @@
    15.4 -(* Title:  mirabelle.ML
    15.5 -   Author: Jasmin Blanchette and Sascha Boehme
    15.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle.ML
    15.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
    15.8  *)
    15.9  
   15.10  signature MIRABELLE =
   15.11  sig
   15.12 -  (* configuration *)
   15.13 +  (*configuration*)
   15.14    val logfile : string Config.T
   15.15    val timeout : int Config.T
   15.16    val start_line : int Config.T
   15.17    val end_line : int Config.T
   15.18    val setup : theory -> theory
   15.19  
   15.20 -  (* core *)
   15.21 -  type init_action
   15.22 -  type done_action
   15.23 -  type run_action
   15.24 -  type action
   15.25 +  (*core*)
   15.26 +  type init_action = int -> theory -> theory
   15.27 +  type done_args = {last: Toplevel.state, log: string -> unit}
   15.28 +  type done_action = int -> done_args -> unit
   15.29 +  type run_args = {pre: Proof.state, post: Toplevel.state option,
   15.30 +    timeout: Time.time, log: string -> unit, pos: Position.T}
   15.31 +  type run_action = int -> run_args -> unit
   15.32 +  type action = init_action * run_action * done_action
   15.33    val catch : (int -> string) -> run_action -> run_action
   15.34    val register : action -> theory -> theory
   15.35    val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
   15.36      unit
   15.37  
   15.38 -  (* utility functions *)
   15.39 +  (*utility functions*)
   15.40    val goal_thm_of : Proof.state -> thm
   15.41    val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
   15.42      Proof.state -> bool
   15.43 @@ -47,14 +50,14 @@
   15.44  val setup = setup1 #> setup2 #> setup3 #> setup4
   15.45  
   15.46  
   15.47 -
   15.48  (* Mirabelle core *)
   15.49  
   15.50 -
   15.51  type init_action = int -> theory -> theory
   15.52 -type done_action = int -> {last: Toplevel.state, log: string -> unit} -> unit
   15.53 -type run_action = int -> {pre: Proof.state, post: Toplevel.state option,
   15.54 -  timeout: Time.time, log: string -> unit, pos: Position.T} -> unit
   15.55 +type done_args = {last: Toplevel.state, log: string -> unit}
   15.56 +type done_action = int -> done_args -> unit
   15.57 +type run_args = {pre: Proof.state, post: Toplevel.state option,
   15.58 +  timeout: Time.time, log: string -> unit, pos: Position.T}
   15.59 +type run_action = int -> run_args -> unit
   15.60  type action = init_action * run_action * done_action
   15.61  
   15.62  structure Actions = TheoryDataFun
   15.63 @@ -70,7 +73,7 @@
   15.64  fun app_with f g x = (g x; ())
   15.65    handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ())
   15.66  
   15.67 -fun catch tag f id (st as {log, ...}) =
   15.68 +fun catch tag f id (st as {log, ...}: run_args) =
   15.69    let fun log_exn e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
   15.70    in app_with log_exn (f id) st end
   15.71  
    16.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Fri Sep 11 20:58:29 2009 +1000
    16.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Thu Sep 17 14:17:37 2009 +1000
    16.3 @@ -1,5 +1,5 @@
    16.4 -(* Title:  mirabelle_arith.ML
    16.5 -   Author: Jasmin Blanchette and Sascha Boehme
    16.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_arith.ML
    16.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
    16.8  *)
    16.9  
   16.10  structure Mirabelle_Arith : MIRABELLE_ACTION =
   16.11 @@ -10,7 +10,7 @@
   16.12  fun init _ = I
   16.13  fun done _ _ = ()
   16.14  
   16.15 -fun run id {pre, timeout, log, ...} =
   16.16 +fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
   16.17    if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
   16.18    then log (arith_tag id ^ "succeeded")
   16.19    else ()
    17.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Fri Sep 11 20:58:29 2009 +1000
    17.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Thu Sep 17 14:17:37 2009 +1000
    17.3 @@ -1,5 +1,5 @@
    17.4 -(* Title:  mirabelle_metis.ML
    17.5 -   Author: Jasmin Blanchette and Sascha Boehme
    17.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_metis.ML
    17.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
    17.8  *)
    17.9  
   17.10  structure Mirabelle_Metis : MIRABELLE_ACTION =
   17.11 @@ -10,7 +10,7 @@
   17.12  fun init _ = I
   17.13  fun done _ _ = ()
   17.14  
   17.15 -fun run id {pre, post, timeout, log} =
   17.16 +fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) =
   17.17    let
   17.18      val thms = Mirabelle.theorems_of_sucessful_proof post
   17.19      val names = map Thm.get_name thms
    18.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Sep 11 20:58:29 2009 +1000
    18.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Thu Sep 17 14:17:37 2009 +1000
    18.3 @@ -1,5 +1,5 @@
    18.4 -(* Title:  mirabelle_quickcheck.ML
    18.5 -   Author: Jasmin Blanchette and Sascha Boehme
    18.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
    18.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
    18.8  *)
    18.9  
   18.10  structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
   18.11 @@ -10,7 +10,7 @@
   18.12  fun init _ = I
   18.13  fun done _ _ = ()
   18.14  
   18.15 -fun run args id {pre, timeout, log, ...} =
   18.16 +fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) =
   18.17    let
   18.18      val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
   18.19      val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
    19.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Fri Sep 11 20:58:29 2009 +1000
    19.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Thu Sep 17 14:17:37 2009 +1000
    19.3 @@ -1,5 +1,5 @@
    19.4 -(* Title:  mirabelle_refute.ML
    19.5 -   Author: Jasmin Blanchette and Sascha Boehme
    19.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_refute.ML
    19.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
    19.8  *)
    19.9  
   19.10  structure Mirabelle_Refute : MIRABELLE_ACTION =
    20.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 11 20:58:29 2009 +1000
    20.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 17 14:17:37 2009 +1000
    20.3 @@ -1,5 +1,5 @@
    20.4 -(* Title:  mirabelle_sledgehammer.ML
    20.5 -   Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow
    20.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
    20.7 +    Author:     Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich
    20.8  *)
    20.9  
   20.10  structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
   20.11 @@ -7,6 +7,7 @@
   20.12  
   20.13  val proverK = "prover"
   20.14  val prover_timeoutK = "prover_timeout"
   20.15 +val prover_hard_timeoutK = "prover_hard_timeout"
   20.16  val keepK = "keep"
   20.17  val full_typesK = "full_types"
   20.18  val minimizeK = "minimize"
   20.19 @@ -22,6 +23,7 @@
   20.20  datatype sh_data = ShData of {
   20.21    calls: int,
   20.22    success: int,
   20.23 +  lemmas: int,
   20.24    time_isa: int,
   20.25    time_atp: int,
   20.26    time_atp_fail: int}
   20.27 @@ -35,46 +37,77 @@
   20.28    posns: Position.T list
   20.29    }
   20.30  
   20.31 +datatype min_data = MinData of {
   20.32 +  calls: int,
   20.33 +  ratios: int,
   20.34 +  lemmas: int
   20.35 +  }
   20.36  
   20.37  (* The first me_data component is only used if "minimize" is on.
   20.38     Then it records how metis behaves with un-minimized lemmas.
   20.39  *)
   20.40 -datatype data = Data of sh_data * me_data * me_data
   20.41 +datatype data = Data of sh_data * me_data * min_data * me_data
   20.42  
   20.43 -fun make_sh_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) =
   20.44 -  ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa,
   20.45 -    time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}
   20.46 +fun make_sh_data (calls,success,lemmas,time_isa,time_atp,time_atp_fail) =
   20.47 +  ShData{calls=calls, success=success, lemmas=lemmas, time_isa=time_isa,
   20.48 +    time_atp=time_atp, time_atp_fail=time_atp_fail}
   20.49 +
   20.50 +fun make_min_data (calls, ratios, lemmas) =
   20.51 +  MinData{calls=calls, ratios=ratios, lemmas=lemmas}
   20.52  
   20.53  fun make_me_data (calls, success, time, timeout, lemmas, posns) =
   20.54    MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
   20.55  
   20.56 -val empty_data = Data(make_sh_data (0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0, 0, []), make_me_data(0, 0, 0, 0, 0, []))
   20.57 +val empty_data =
   20.58 +  Data(make_sh_data (0, 0, 0, 0, 0, 0),
   20.59 +       make_me_data(0, 0, 0, 0, 0, []),
   20.60 +       MinData{calls=0, ratios=0, lemmas=0},
   20.61 +       make_me_data(0, 0, 0, 0, 0, []))
   20.62  
   20.63  fun map_sh_data f
   20.64 -  (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, meda)) =
   20.65 -  Data (make_sh_data (f (calls, success, time_isa, time_atp, time_atp_fail)),
   20.66 -        meda0, meda)
   20.67 +  (Data (ShData{calls, success, lemmas, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) =
   20.68 +  Data (make_sh_data (f (calls, success, lemmas, time_isa, time_atp, time_atp_fail)),
   20.69 +        meda0, minda, meda)
   20.70 +
   20.71 +fun map_min_data f
   20.72 +  (Data(shda, meda0, MinData{calls,ratios,lemmas}, meda)) =
   20.73 +  Data(shda, meda0, make_min_data(f(calls,ratios,lemmas)), meda)
   20.74 +
   20.75 +fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) =
   20.76 +  Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda)
   20.77  
   20.78 -fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, meda)) =
   20.79 -  Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), meda)
   20.80 +fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,time,timeout,lemmas,posns})) =
   20.81 +  Data(shda, meda0, minda, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
   20.82  
   20.83 -fun map_me_data f (Data (shda, meda0, MeData{calls,success,time,timeout,lemmas,posns})) =
   20.84 -  Data(shda, meda0, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
   20.85 +val inc_sh_calls =
   20.86 +  map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
   20.87 +    => (calls + 1, success, lemmas, time_isa, time_atp, time_atp_fail))
   20.88 +
   20.89 +val inc_sh_success =
   20.90 +  map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
   20.91 +    => (calls, success + 1, lemmas, time_isa, time_atp, time_atp_fail))
   20.92  
   20.93 -val inc_sh_calls = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
   20.94 -  => (sh_calls + 1, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail))
   20.95 +fun inc_sh_lemmas n =
   20.96 +  map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
   20.97 +    => (calls, success, lemmas + n, time_isa, time_atp, time_atp_fail))
   20.98  
   20.99 -val inc_sh_success = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
  20.100 -  => (sh_calls, sh_success + 1, sh_time_isa, sh_time_atp, sh_time_atp_fail))
  20.101 +fun inc_sh_time_isa t =
  20.102 +  map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
  20.103 +    => (calls, success, lemmas, time_isa + t, time_atp, time_atp_fail))
  20.104  
  20.105 -fun inc_sh_time_isa t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
  20.106 -  => (sh_calls, sh_success, sh_time_isa + t, sh_time_atp, sh_time_atp_fail))
  20.107 +fun inc_sh_time_atp t =
  20.108 +  map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
  20.109 +    => (calls, success, lemmas, time_isa, time_atp + t, time_atp_fail))
  20.110  
  20.111 -fun inc_sh_time_atp t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
  20.112 -  => (sh_calls, sh_success, sh_time_isa, sh_time_atp + t, sh_time_atp_fail))
  20.113 +fun inc_sh_time_atp_fail t =
  20.114 +  map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
  20.115 +    => (calls, success, lemmas, time_isa, time_atp, time_atp_fail + t))
  20.116  
  20.117 -fun inc_sh_time_atp_fail t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
  20.118 -  => (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail + t))
  20.119 +val inc_min_calls =
  20.120 +  map_min_data (fn (calls, ratios, lemmas) => (calls + 1, ratios, lemmas))
  20.121 +
  20.122 +fun inc_min_ratios n =
  20.123 +  map_min_data (fn (calls, ratios, lemmas) => (calls, ratios + n, lemmas))
  20.124  
  20.125  val inc_metis_calls = map_me_data
  20.126   (fn (calls, success, time, timeout, lemmas,posns)
  20.127 @@ -133,9 +166,10 @@
  20.128  fun avg_time t n =
  20.129    if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
  20.130  
  20.131 -fun log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail =
  20.132 +fun log_sh_data log sh_calls sh_success sh_lemmas sh_time_isa sh_time_atp sh_time_atp_fail =
  20.133   (log ("Total number of sledgehammer calls: " ^ str sh_calls);
  20.134    log ("Number of successful sledgehammer calls: " ^ str sh_success);
  20.135 +  log ("Number of sledgehammer lemmas: " ^ str sh_lemmas);
  20.136    log ("Success rate: " ^ percentage sh_success sh_calls ^ "%");
  20.137    log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time sh_time_isa));
  20.138    log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time sh_time_atp));
  20.139 @@ -161,7 +195,7 @@
  20.140    log ("Number of " ^ tag ^ "metis exceptions: " ^
  20.141      str (sh_success - metis_success - metis_timeout));
  20.142    log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
  20.143 -  log ("Number of " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
  20.144 +  log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
  20.145    log ("Total time for successful metis calls: " ^ str3 (time metis_time));
  20.146    log ("Average time for successful metis calls: " ^
  20.147      str3 (avg_time metis_time metis_success));
  20.148 @@ -169,22 +203,36 @@
  20.149    then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns))
  20.150    else ()
  20.151   )
  20.152 +
  20.153 +fun log_min_data log calls ratios =
  20.154 +  (log ("Number of minimizations: " ^ string_of_int calls);
  20.155 +   log ("Minimization ratios: " ^ string_of_int ratios)
  20.156 +  )
  20.157 +
  20.158  in
  20.159  
  20.160 -fun log_data id log (Data (ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa, time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}, MeData{calls=metis_calls0,
  20.161 -    success=metis_success0, time=metis_time0, timeout=metis_timeout0, lemmas=metis_lemmas0,posns=metis_posns0}, MeData{calls=metis_calls,
  20.162 -    success=metis_success, time=metis_time, timeout=metis_timeout, lemmas=metis_lemmas,posns=metis_posns})) =
  20.163 +fun log_data id log (Data
  20.164 +   (ShData{calls=sh_calls, lemmas=sh_lemmas, success=sh_success,
  20.165 +      time_isa=sh_time_isa,time_atp=sh_time_atp,time_atp_fail=sh_time_atp_fail},
  20.166 +    MeData{calls=metis_calls0,
  20.167 +      success=metis_success0, time=metis_time0, timeout=metis_timeout0,
  20.168 +      lemmas=metis_lemmas0,posns=metis_posns0},
  20.169 +    MinData{calls=min_calls, ratios=min_ratios, lemmas=min_lemmas},
  20.170 +    MeData{calls=metis_calls,
  20.171 +      success=metis_success, time=metis_time, timeout=metis_timeout,
  20.172 +      lemmas=metis_lemmas,posns=metis_posns})) =
  20.173    if sh_calls > 0
  20.174    then
  20.175     (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
  20.176 -    log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail;
  20.177 +    log_sh_data log sh_calls sh_success sh_lemmas sh_time_isa sh_time_atp sh_time_atp_fail;
  20.178      log "";
  20.179      if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls
  20.180        metis_success metis_time metis_timeout metis_lemmas  metis_posns else ();
  20.181      log "";
  20.182      if metis_calls0 > 0
  20.183 -      then log_metis_data log "unminimized " sh_calls sh_success metis_calls0
  20.184 -              metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0
  20.185 +      then (log_min_data log min_calls min_ratios; log "";
  20.186 +            log_metis_data log "unminimized " sh_calls sh_success metis_calls0
  20.187 +              metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
  20.188        else ()
  20.189     )
  20.190    else ()
  20.191 @@ -196,7 +244,7 @@
  20.192  val data = ref ([] : (int * data) list)
  20.193  
  20.194  fun init id thy = (change data (cons (id, empty_data)); thy)
  20.195 -fun done id {log, ...} =
  20.196 +fun done id ({log, ...}: Mirabelle.done_args) =
  20.197    AList.lookup (op =) (!data) id
  20.198    |> Option.map (log_data id log)
  20.199    |> K ()
  20.200 @@ -233,17 +281,22 @@
  20.201    SH_FAIL of int * int |
  20.202    SH_ERROR
  20.203  
  20.204 -fun run_sh (prover_name, prover) timeout st _ =
  20.205 +fun run_sh (prover_name, prover) hard_timeout timeout st _ =
  20.206    let
  20.207      val atp = prover timeout NONE NONE prover_name 1
  20.208 +    val time_limit =
  20.209 +      (case hard_timeout of
  20.210 +        NONE => I
  20.211 +      | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
  20.212      val ((success, (message, thm_names), time_atp, _, _, _), time_isa) =
  20.213 -      Mirabelle.cpu_time atp (Proof.get_goal st)
  20.214 +      time_limit (Mirabelle.cpu_time atp) (Proof.get_goal st)
  20.215    in
  20.216      if success then (message, SH_OK (time_isa, time_atp, thm_names))
  20.217      else (message, SH_FAIL(time_isa, time_atp))
  20.218    end
  20.219    handle ResHolClause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
  20.220         | ERROR msg => ("error: " ^ msg, SH_ERROR)
  20.221 +       | TimeLimit.TimeOut => ("timeout", SH_ERROR)
  20.222  
  20.223  fun thms_of_name ctxt name =
  20.224    let
  20.225 @@ -260,18 +313,22 @@
  20.226  
  20.227  in
  20.228  
  20.229 -fun run_sledgehammer args named_thms id {pre=st, log, ...} =
  20.230 +fun run_sledgehammer args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
  20.231    let
  20.232      val _ = change_data id inc_sh_calls
  20.233      val atp as (prover_name, _) = get_atp (Proof.theory_of st) args
  20.234      val dir = AList.lookup (op =) args keepK
  20.235      val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
  20.236 -    val (msg, result) = safe init_sh done_sh (run_sh atp timeout st) dir
  20.237 +    val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
  20.238 +      |> Option.map (fst o read_int o explode)
  20.239 +    val (msg, result) = safe init_sh done_sh
  20.240 +      (run_sh atp hard_timeout timeout st) dir
  20.241    in
  20.242      case result of
  20.243        SH_OK (time_isa, time_atp, names) =>
  20.244          let
  20.245            val _ = change_data id inc_sh_success
  20.246 +          val _ = change_data id (inc_sh_lemmas (length names))
  20.247            val _ = change_data id (inc_sh_time_isa time_isa)
  20.248            val _ = change_data id (inc_sh_time_atp time_atp)
  20.249  
  20.250 @@ -292,8 +349,9 @@
  20.251  end
  20.252  
  20.253  
  20.254 -fun run_minimize args named_thms id {pre=st, log, ...} =
  20.255 +fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
  20.256    let
  20.257 +    val n0 = length (these (!named_thms))
  20.258      val (prover_name, prover) = get_atp (Proof.theory_of st) args
  20.259      val minimize = AtpMinimal.minimalize prover prover_name
  20.260      val timeout =
  20.261 @@ -302,24 +360,29 @@
  20.262        |> the_default 5
  20.263      val _ = log separator
  20.264    in
  20.265 -    (case minimize timeout st (these (!named_thms)) of
  20.266 -      (SOME named_thms', msg) =>
  20.267 -        if length named_thms' = length (these (!named_thms))
  20.268 -        then log (minimize_tag id ^ "already minimal")
  20.269 -        else
  20.270 -         (named_thms := SOME named_thms';
  20.271 -          log (minimize_tag id ^ "succeeded:\n" ^ msg))
  20.272 -    | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg))
  20.273 +    case minimize timeout st (these (!named_thms)) of
  20.274 +      (SOME (named_thms',its), msg) =>
  20.275 +        (change_data id inc_min_calls;
  20.276 +         change_data id (inc_min_ratios ((100*its) div n0));
  20.277 +         if length named_thms' = n0
  20.278 +         then log (minimize_tag id ^ "already minimal")
  20.279 +         else (named_thms := SOME named_thms';
  20.280 +               log (minimize_tag id ^ "succeeded:\n" ^ msg))
  20.281 +        )
  20.282 +    | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
  20.283    end
  20.284  
  20.285  
  20.286 -fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout, inc_metis_lemmas, inc_metis_posns) args named_thms id {pre=st, timeout, log, pos, ...} =
  20.287 +fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout,
  20.288 +    inc_metis_lemmas, inc_metis_posns) args named_thms id
  20.289 +    ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
  20.290    let
  20.291      fun metis thms ctxt = MetisTools.metis_tac ctxt thms
  20.292      fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
  20.293  
  20.294      fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
  20.295        | with_time (true, t) = (change_data id inc_metis_success;
  20.296 +          change_data id (inc_metis_lemmas (length named_thms));
  20.297            change_data id (inc_metis_time t);
  20.298            change_data id (inc_metis_posns pos);
  20.299            "succeeded (" ^ string_of_int t ^ ")")
  20.300 @@ -329,17 +392,18 @@
  20.301  
  20.302      val _ = log separator
  20.303      val _ = change_data id inc_metis_calls
  20.304 -    val _ = change_data id (inc_metis_lemmas (length named_thms))
  20.305    in
  20.306      maps snd named_thms
  20.307      |> timed_metis
  20.308      |> log o prefix (metis_tag id) 
  20.309    end
  20.310  
  20.311 -fun sledgehammer_action args id (st as {log, ...}) =
  20.312 +fun sledgehammer_action args id (st as {log, ...}: Mirabelle.run_args) =
  20.313    let
  20.314 -    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
  20.315 -    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0, inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
  20.316 +    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time,
  20.317 +        inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
  20.318 +    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0,
  20.319 +        inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
  20.320      val named_thms = ref (NONE : (string * thm list) list option)
  20.321  
  20.322      fun if_enabled k f =
  20.323 @@ -349,9 +413,8 @@
  20.324      val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st
  20.325      val _ = if_enabled minimizeK
  20.326        (Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))))
  20.327 -    val _ = if is_some (!named_thms)
  20.328 -      then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st
  20.329 -      else ()
  20.330 +    val _ = if_enabled minimizeK
  20.331 +      (Mirabelle.catch minimize_tag (run_minimize args named_thms))
  20.332      val _ = if is_some (!named_thms)
  20.333        then Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st
  20.334        else ()
    21.1 --- a/src/HOL/Mirabelle/doc/options.txt	Fri Sep 11 20:58:29 2009 +1000
    21.2 +++ b/src/HOL/Mirabelle/doc/options.txt	Thu Sep 17 14:17:37 2009 +1000
    21.3 @@ -1,9 +1,11 @@
    21.4  Options for sledgehammer:
    21.5  
    21.6    * prover=NAME: name of the external prover to call
    21.7 -  * prover_timeout=TIME: timeout for invoked ATP
    21.8 +  * prover_timeout=TIME: timeout for invoked ATP (seconds of process time)
    21.9 +  * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed time)
   21.10    * keep=PATH: path where to keep temporary files created by sledgehammer 
   21.11    * full_types: enable full-typed encoding
   21.12    * minimize: enable minimization of theorem set found by sledgehammer
   21.13 -  * minimize_timeout=TIME: timeout for each minimization step
   21.14 +  * minimize_timeout=TIME: timeout for each minimization step (seconds of
   21.15 +    process time)
   21.16    * metis: apply metis with the theorems found by sledgehammer
    22.1 --- a/src/HOL/NatTransfer.thy	Fri Sep 11 20:58:29 2009 +1000
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,537 +0,0 @@
    22.4 -(*  Title:      HOL/Library/NatTransfer.thy
    22.5 -    Authors:    Jeremy Avigad and Amine Chaieb
    22.6 -
    22.7 -    Sets up transfer from nats to ints and
    22.8 -    back.
    22.9 -*)
   22.10 -
   22.11 -
   22.12 -header {* NatTransfer *}
   22.13 -
   22.14 -theory NatTransfer
   22.15 -imports Main Parity
   22.16 -uses ("Tools/transfer_data.ML")
   22.17 -begin
   22.18 -
   22.19 -subsection {* A transfer Method between isomorphic domains*}
   22.20 -
   22.21 -definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
   22.22 -  where "TransferMorphism a B = True"
   22.23 -
   22.24 -use "Tools/transfer_data.ML"
   22.25 -
   22.26 -setup TransferData.setup
   22.27 -
   22.28 -
   22.29 -subsection {* Set up transfer from nat to int *}
   22.30 -
   22.31 -(* set up transfer direction *)
   22.32 -
   22.33 -lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
   22.34 -  by (simp add: TransferMorphism_def)
   22.35 -
   22.36 -declare TransferMorphism_nat_int[transfer
   22.37 -  add mode: manual
   22.38 -  return: nat_0_le
   22.39 -  labels: natint
   22.40 -]
   22.41 -
   22.42 -(* basic functions and relations *)
   22.43 -
   22.44 -lemma transfer_nat_int_numerals:
   22.45 -    "(0::nat) = nat 0"
   22.46 -    "(1::nat) = nat 1"
   22.47 -    "(2::nat) = nat 2"
   22.48 -    "(3::nat) = nat 3"
   22.49 -  by auto
   22.50 -
   22.51 -definition
   22.52 -  tsub :: "int \<Rightarrow> int \<Rightarrow> int"
   22.53 -where
   22.54 -  "tsub x y = (if x >= y then x - y else 0)"
   22.55 -
   22.56 -lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
   22.57 -  by (simp add: tsub_def)
   22.58 -
   22.59 -
   22.60 -lemma transfer_nat_int_functions:
   22.61 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
   22.62 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
   22.63 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
   22.64 -    "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
   22.65 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
   22.66 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
   22.67 -  by (auto simp add: eq_nat_nat_iff nat_mult_distrib
   22.68 -      nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
   22.69 -
   22.70 -lemma transfer_nat_int_function_closures:
   22.71 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
   22.72 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
   22.73 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
   22.74 -    "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
   22.75 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
   22.76 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
   22.77 -    "(0::int) >= 0"
   22.78 -    "(1::int) >= 0"
   22.79 -    "(2::int) >= 0"
   22.80 -    "(3::int) >= 0"
   22.81 -    "int z >= 0"
   22.82 -  apply (auto simp add: zero_le_mult_iff tsub_def)
   22.83 -  apply (case_tac "y = 0")
   22.84 -  apply auto
   22.85 -  apply (subst pos_imp_zdiv_nonneg_iff, auto)
   22.86 -  apply (case_tac "y = 0")
   22.87 -  apply force
   22.88 -  apply (rule pos_mod_sign)
   22.89 -  apply arith
   22.90 -done
   22.91 -
   22.92 -lemma transfer_nat_int_relations:
   22.93 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
   22.94 -      (nat (x::int) = nat y) = (x = y)"
   22.95 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
   22.96 -      (nat (x::int) < nat y) = (x < y)"
   22.97 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
   22.98 -      (nat (x::int) <= nat y) = (x <= y)"
   22.99 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
  22.100 -      (nat (x::int) dvd nat y) = (x dvd y)"
  22.101 -  by (auto simp add: zdvd_int even_nat_def)
  22.102 -
  22.103 -declare TransferMorphism_nat_int[transfer add return:
  22.104 -  transfer_nat_int_numerals
  22.105 -  transfer_nat_int_functions
  22.106 -  transfer_nat_int_function_closures
  22.107 -  transfer_nat_int_relations
  22.108 -]
  22.109 -
  22.110 -
  22.111 -(* first-order quantifiers *)
  22.112 -
  22.113 -lemma transfer_nat_int_quantifiers:
  22.114 -    "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
  22.115 -    "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
  22.116 -  by (rule all_nat, rule ex_nat)
  22.117 -
  22.118 -(* should we restrict these? *)
  22.119 -lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
  22.120 -    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
  22.121 -  by auto
  22.122 -
  22.123 -lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
  22.124 -    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
  22.125 -  by auto
  22.126 -
  22.127 -declare TransferMorphism_nat_int[transfer add
  22.128 -  return: transfer_nat_int_quantifiers
  22.129 -  cong: all_cong ex_cong]
  22.130 -
  22.131 -
  22.132 -(* if *)
  22.133 -
  22.134 -lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
  22.135 -    nat (if P then x else y)"
  22.136 -  by auto
  22.137 -
  22.138 -declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
  22.139 -
  22.140 -
  22.141 -(* operations with sets *)
  22.142 -
  22.143 -definition
  22.144 -  nat_set :: "int set \<Rightarrow> bool"
  22.145 -where
  22.146 -  "nat_set S = (ALL x:S. x >= 0)"
  22.147 -
  22.148 -lemma transfer_nat_int_set_functions:
  22.149 -    "card A = card (int ` A)"
  22.150 -    "{} = nat ` ({}::int set)"
  22.151 -    "A Un B = nat ` (int ` A Un int ` B)"
  22.152 -    "A Int B = nat ` (int ` A Int int ` B)"
  22.153 -    "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
  22.154 -    "{..n} = nat ` {0..int n}"
  22.155 -    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
  22.156 -  apply (rule card_image [symmetric])
  22.157 -  apply (auto simp add: inj_on_def image_def)
  22.158 -  apply (rule_tac x = "int x" in bexI)
  22.159 -  apply auto
  22.160 -  apply (rule_tac x = "int x" in bexI)
  22.161 -  apply auto
  22.162 -  apply (rule_tac x = "int x" in bexI)
  22.163 -  apply auto
  22.164 -  apply (rule_tac x = "int x" in exI)
  22.165 -  apply auto
  22.166 -  apply (rule_tac x = "int x" in bexI)
  22.167 -  apply auto
  22.168 -  apply (rule_tac x = "int x" in bexI)
  22.169 -  apply auto
  22.170 -done
  22.171 -
  22.172 -lemma transfer_nat_int_set_function_closures:
  22.173 -    "nat_set {}"
  22.174 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
  22.175 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
  22.176 -    "x >= 0 \<Longrightarrow> nat_set {x..y}"
  22.177 -    "nat_set {x. x >= 0 & P x}"
  22.178 -    "nat_set (int ` C)"
  22.179 -    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
  22.180 -  unfolding nat_set_def apply auto
  22.181 -done
  22.182 -
  22.183 -lemma transfer_nat_int_set_relations:
  22.184 -    "(finite A) = (finite (int ` A))"
  22.185 -    "(x : A) = (int x : int ` A)"
  22.186 -    "(A = B) = (int ` A = int ` B)"
  22.187 -    "(A < B) = (int ` A < int ` B)"
  22.188 -    "(A <= B) = (int ` A <= int ` B)"
  22.189 -
  22.190 -  apply (rule iffI)
  22.191 -  apply (erule finite_imageI)
  22.192 -  apply (erule finite_imageD)
  22.193 -  apply (auto simp add: image_def expand_set_eq inj_on_def)
  22.194 -  apply (drule_tac x = "int x" in spec, auto)
  22.195 -  apply (drule_tac x = "int x" in spec, auto)
  22.196 -  apply (drule_tac x = "int x" in spec, auto)
  22.197 -done
  22.198 -
  22.199 -lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
  22.200 -    (int ` nat ` A = A)"
  22.201 -  by (auto simp add: nat_set_def image_def)
  22.202 -
  22.203 -lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
  22.204 -    {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
  22.205 -  by auto
  22.206 -
  22.207 -declare TransferMorphism_nat_int[transfer add
  22.208 -  return: transfer_nat_int_set_functions
  22.209 -    transfer_nat_int_set_function_closures
  22.210 -    transfer_nat_int_set_relations
  22.211 -    transfer_nat_int_set_return_embed
  22.212 -  cong: transfer_nat_int_set_cong
  22.213 -]
  22.214 -
  22.215 -
  22.216 -(* setsum and setprod *)
  22.217 -
  22.218 -(* this handles the case where the *domain* of f is nat *)
  22.219 -lemma transfer_nat_int_sum_prod:
  22.220 -    "setsum f A = setsum (%x. f (nat x)) (int ` A)"
  22.221 -    "setprod f A = setprod (%x. f (nat x)) (int ` A)"
  22.222 -  apply (subst setsum_reindex)
  22.223 -  apply (unfold inj_on_def, auto)
  22.224 -  apply (subst setprod_reindex)
  22.225 -  apply (unfold inj_on_def o_def, auto)
  22.226 -done
  22.227 -
  22.228 -(* this handles the case where the *range* of f is nat *)
  22.229 -lemma transfer_nat_int_sum_prod2:
  22.230 -    "setsum f A = nat(setsum (%x. int (f x)) A)"
  22.231 -    "setprod f A = nat(setprod (%x. int (f x)) A)"
  22.232 -  apply (subst int_setsum [symmetric])
  22.233 -  apply auto
  22.234 -  apply (subst int_setprod [symmetric])
  22.235 -  apply auto
  22.236 -done
  22.237 -
  22.238 -lemma transfer_nat_int_sum_prod_closure:
  22.239 -    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
  22.240 -    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
  22.241 -  unfolding nat_set_def
  22.242 -  apply (rule setsum_nonneg)
  22.243 -  apply auto
  22.244 -  apply (rule setprod_nonneg)
  22.245 -  apply auto
  22.246 -done
  22.247 -
  22.248 -(* this version doesn't work, even with nat_set A \<Longrightarrow>
  22.249 -      x : A \<Longrightarrow> x >= 0 turned on. Why not?
  22.250 -
  22.251 -  also: what does =simp=> do?
  22.252 -
  22.253 -lemma transfer_nat_int_sum_prod_closure:
  22.254 -    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
  22.255 -    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
  22.256 -  unfolding nat_set_def simp_implies_def
  22.257 -  apply (rule setsum_nonneg)
  22.258 -  apply auto
  22.259 -  apply (rule setprod_nonneg)
  22.260 -  apply auto
  22.261 -done
  22.262 -*)
  22.263 -
  22.264 -(* Making A = B in this lemma doesn't work. Why not?
  22.265 -   Also, why aren't setsum_cong and setprod_cong enough,
  22.266 -   with the previously mentioned rule turned on? *)
  22.267 -
  22.268 -lemma transfer_nat_int_sum_prod_cong:
  22.269 -    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
  22.270 -      setsum f A = setsum g B"
  22.271 -    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
  22.272 -      setprod f A = setprod g B"
  22.273 -  unfolding nat_set_def
  22.274 -  apply (subst setsum_cong, assumption)
  22.275 -  apply auto [2]
  22.276 -  apply (subst setprod_cong, assumption, auto)
  22.277 -done
  22.278 -
  22.279 -declare TransferMorphism_nat_int[transfer add
  22.280 -  return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
  22.281 -    transfer_nat_int_sum_prod_closure
  22.282 -  cong: transfer_nat_int_sum_prod_cong]
  22.283 -
  22.284 -(* lists *)
  22.285 -
  22.286 -definition
  22.287 -  embed_list :: "nat list \<Rightarrow> int list"
  22.288 -where
  22.289 -  "embed_list l = map int l";
  22.290 -
  22.291 -definition
  22.292 -  nat_list :: "int list \<Rightarrow> bool"
  22.293 -where
  22.294 -  "nat_list l = nat_set (set l)";
  22.295 -
  22.296 -definition
  22.297 -  return_list :: "int list \<Rightarrow> nat list"
  22.298 -where
  22.299 -  "return_list l = map nat l";
  22.300 -
  22.301 -thm nat_0_le;
  22.302 -
  22.303 -lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
  22.304 -    embed_list (return_list l) = l";
  22.305 -  unfolding embed_list_def return_list_def nat_list_def nat_set_def
  22.306 -  apply (induct l);
  22.307 -  apply auto;
  22.308 -done;
  22.309 -
  22.310 -lemma transfer_nat_int_list_functions:
  22.311 -  "l @ m = return_list (embed_list l @ embed_list m)"
  22.312 -  "[] = return_list []";
  22.313 -  unfolding return_list_def embed_list_def;
  22.314 -  apply auto;
  22.315 -  apply (induct l, auto);
  22.316 -  apply (induct m, auto);
  22.317 -done;
  22.318 -
  22.319 -(*
  22.320 -lemma transfer_nat_int_fold1: "fold f l x =
  22.321 -    fold (%x. f (nat x)) (embed_list l) x";
  22.322 -*)
  22.323 -
  22.324 -
  22.325 -
  22.326 -
  22.327 -subsection {* Set up transfer from int to nat *}
  22.328 -
  22.329 -(* set up transfer direction *)
  22.330 -
  22.331 -lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
  22.332 -  by (simp add: TransferMorphism_def)
  22.333 -
  22.334 -declare TransferMorphism_int_nat[transfer add
  22.335 -  mode: manual
  22.336 -(*  labels: int-nat *)
  22.337 -  return: nat_int
  22.338 -]
  22.339 -
  22.340 -
  22.341 -(* basic functions and relations *)
  22.342 -
  22.343 -definition
  22.344 -  is_nat :: "int \<Rightarrow> bool"
  22.345 -where
  22.346 -  "is_nat x = (x >= 0)"
  22.347 -
  22.348 -lemma transfer_int_nat_numerals:
  22.349 -    "0 = int 0"
  22.350 -    "1 = int 1"
  22.351 -    "2 = int 2"
  22.352 -    "3 = int 3"
  22.353 -  by auto
  22.354 -
  22.355 -lemma transfer_int_nat_functions:
  22.356 -    "(int x) + (int y) = int (x + y)"
  22.357 -    "(int x) * (int y) = int (x * y)"
  22.358 -    "tsub (int x) (int y) = int (x - y)"
  22.359 -    "(int x)^n = int (x^n)"
  22.360 -    "(int x) div (int y) = int (x div y)"
  22.361 -    "(int x) mod (int y) = int (x mod y)"
  22.362 -  by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
  22.363 -
  22.364 -lemma transfer_int_nat_function_closures:
  22.365 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
  22.366 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
  22.367 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
  22.368 -    "is_nat x \<Longrightarrow> is_nat (x^n)"
  22.369 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
  22.370 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
  22.371 -    "is_nat 0"
  22.372 -    "is_nat 1"
  22.373 -    "is_nat 2"
  22.374 -    "is_nat 3"
  22.375 -    "is_nat (int z)"
  22.376 -  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
  22.377 -
  22.378 -lemma transfer_int_nat_relations:
  22.379 -    "(int x = int y) = (x = y)"
  22.380 -    "(int x < int y) = (x < y)"
  22.381 -    "(int x <= int y) = (x <= y)"
  22.382 -    "(int x dvd int y) = (x dvd y)"
  22.383 -    "(even (int x)) = (even x)"
  22.384 -  by (auto simp add: zdvd_int even_nat_def)
  22.385 -
  22.386 -lemma UNIV_apply:
  22.387 -  "UNIV x = True"
  22.388 -  by (simp add: top_fun_eq top_bool_eq)
  22.389 -
  22.390 -declare TransferMorphism_int_nat[transfer add return:
  22.391 -  transfer_int_nat_numerals
  22.392 -  transfer_int_nat_functions
  22.393 -  transfer_int_nat_function_closures
  22.394 -  transfer_int_nat_relations
  22.395 -  UNIV_apply
  22.396 -]
  22.397 -
  22.398 -
  22.399 -(* first-order quantifiers *)
  22.400 -
  22.401 -lemma transfer_int_nat_quantifiers:
  22.402 -    "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
  22.403 -    "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
  22.404 -  apply (subst all_nat)
  22.405 -  apply auto [1]
  22.406 -  apply (subst ex_nat)
  22.407 -  apply auto
  22.408 -done
  22.409 -
  22.410 -declare TransferMorphism_int_nat[transfer add
  22.411 -  return: transfer_int_nat_quantifiers]
  22.412 -
  22.413 -
  22.414 -(* if *)
  22.415 -
  22.416 -lemma int_if_cong: "(if P then (int x) else (int y)) =
  22.417 -    int (if P then x else y)"
  22.418 -  by auto
  22.419 -
  22.420 -declare TransferMorphism_int_nat [transfer add return: int_if_cong]
  22.421 -
  22.422 -
  22.423 -
  22.424 -(* operations with sets *)
  22.425 -
  22.426 -lemma transfer_int_nat_set_functions:
  22.427 -    "nat_set A \<Longrightarrow> card A = card (nat ` A)"
  22.428 -    "{} = int ` ({}::nat set)"
  22.429 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
  22.430 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
  22.431 -    "{x. x >= 0 & P x} = int ` {x. P(int x)}"
  22.432 -    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
  22.433 -       (* need all variants of these! *)
  22.434 -  by (simp_all only: is_nat_def transfer_nat_int_set_functions
  22.435 -          transfer_nat_int_set_function_closures
  22.436 -          transfer_nat_int_set_return_embed nat_0_le
  22.437 -          cong: transfer_nat_int_set_cong)
  22.438 -
  22.439 -lemma transfer_int_nat_set_function_closures:
  22.440 -    "nat_set {}"
  22.441 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
  22.442 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
  22.443 -    "is_nat x \<Longrightarrow> nat_set {x..y}"
  22.444 -    "nat_set {x. x >= 0 & P x}"
  22.445 -    "nat_set (int ` C)"
  22.446 -    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
  22.447 -  by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
  22.448 -
  22.449 -lemma transfer_int_nat_set_relations:
  22.450 -    "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
  22.451 -    "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
  22.452 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
  22.453 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
  22.454 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
  22.455 -  by (simp_all only: is_nat_def transfer_nat_int_set_relations
  22.456 -    transfer_nat_int_set_return_embed nat_0_le)
  22.457 -
  22.458 -lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
  22.459 -  by (simp only: transfer_nat_int_set_relations
  22.460 -    transfer_nat_int_set_function_closures
  22.461 -    transfer_nat_int_set_return_embed nat_0_le)
  22.462 -
  22.463 -lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
  22.464 -    {(x::nat). P x} = {x. P' x}"
  22.465 -  by auto
  22.466 -
  22.467 -declare TransferMorphism_int_nat[transfer add
  22.468 -  return: transfer_int_nat_set_functions
  22.469 -    transfer_int_nat_set_function_closures
  22.470 -    transfer_int_nat_set_relations
  22.471 -    transfer_int_nat_set_return_embed
  22.472 -  cong: transfer_int_nat_set_cong
  22.473 -]
  22.474 -
  22.475 -
  22.476 -(* setsum and setprod *)
  22.477 -
  22.478 -(* this handles the case where the *domain* of f is int *)
  22.479 -lemma transfer_int_nat_sum_prod:
  22.480 -    "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
  22.481 -    "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
  22.482 -  apply (subst setsum_reindex)
  22.483 -  apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
  22.484 -  apply (subst setprod_reindex)
  22.485 -  apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
  22.486 -            cong: setprod_cong)
  22.487 -done
  22.488 -
  22.489 -(* this handles the case where the *range* of f is int *)
  22.490 -lemma transfer_int_nat_sum_prod2:
  22.491 -    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
  22.492 -    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
  22.493 -      setprod f A = int(setprod (%x. nat (f x)) A)"
  22.494 -  unfolding is_nat_def
  22.495 -  apply (subst int_setsum, auto)
  22.496 -  apply (subst int_setprod, auto simp add: cong: setprod_cong)
  22.497 -done
  22.498 -
  22.499 -declare TransferMorphism_int_nat[transfer add
  22.500 -  return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
  22.501 -  cong: setsum_cong setprod_cong]
  22.502 -
  22.503 -
  22.504 -subsection {* Test it out *}
  22.505 -
  22.506 -(* nat to int *)
  22.507 -
  22.508 -lemma ex1: "(x::nat) + y = y + x"
  22.509 -  by auto
  22.510 -
  22.511 -thm ex1 [transferred]
  22.512 -
  22.513 -lemma ex2: "(a::nat) div b * b + a mod b = a"
  22.514 -  by (rule mod_div_equality)
  22.515 -
  22.516 -thm ex2 [transferred]
  22.517 -
  22.518 -lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
  22.519 -  by auto
  22.520 -
  22.521 -thm ex3 [transferred natint]
  22.522 -
  22.523 -lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
  22.524 -  by auto
  22.525 -
  22.526 -thm ex4 [transferred]
  22.527 -
  22.528 -lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
  22.529 -  by (induct n rule: nat_induct, auto)
  22.530 -
  22.531 -thm ex5 [transferred]
  22.532 -
  22.533 -theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
  22.534 -  by (rule ex5 [transferred])
  22.535 -
  22.536 -thm ex6 [transferred]
  22.537 -
  22.538 -thm ex5 [transferred, transferred]
  22.539 -
  22.540 -end
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/HOL/Nat_Transfer.thy	Thu Sep 17 14:17:37 2009 +1000
    23.3 @@ -0,0 +1,484 @@
    23.4 +
    23.5 +(* Authors: Jeremy Avigad and Amine Chaieb *)
    23.6 +
    23.7 +header {* Sets up transfer from nats to ints and back. *}
    23.8 +
    23.9 +theory Nat_Transfer
   23.10 +imports Main Parity
   23.11 +begin
   23.12 +
   23.13 +subsection {* Set up transfer from nat to int *}
   23.14 +
   23.15 +(* set up transfer direction *)
   23.16 +
   23.17 +lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
   23.18 +  by (simp add: TransferMorphism_def)
   23.19 +
   23.20 +declare TransferMorphism_nat_int[transfer
   23.21 +  add mode: manual
   23.22 +  return: nat_0_le
   23.23 +  labels: natint
   23.24 +]
   23.25 +
   23.26 +(* basic functions and relations *)
   23.27 +
   23.28 +lemma transfer_nat_int_numerals:
   23.29 +    "(0::nat) = nat 0"
   23.30 +    "(1::nat) = nat 1"
   23.31 +    "(2::nat) = nat 2"
   23.32 +    "(3::nat) = nat 3"
   23.33 +  by auto
   23.34 +
   23.35 +definition
   23.36 +  tsub :: "int \<Rightarrow> int \<Rightarrow> int"
   23.37 +where
   23.38 +  "tsub x y = (if x >= y then x - y else 0)"
   23.39 +
   23.40 +lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
   23.41 +  by (simp add: tsub_def)
   23.42 +
   23.43 +
   23.44 +lemma transfer_nat_int_functions:
   23.45 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
   23.46 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
   23.47 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
   23.48 +    "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
   23.49 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
   23.50 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
   23.51 +  by (auto simp add: eq_nat_nat_iff nat_mult_distrib
   23.52 +      nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
   23.53 +
   23.54 +lemma transfer_nat_int_function_closures:
   23.55 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
   23.56 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
   23.57 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
   23.58 +    "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
   23.59 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
   23.60 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
   23.61 +    "(0::int) >= 0"
   23.62 +    "(1::int) >= 0"
   23.63 +    "(2::int) >= 0"
   23.64 +    "(3::int) >= 0"
   23.65 +    "int z >= 0"
   23.66 +  apply (auto simp add: zero_le_mult_iff tsub_def)
   23.67 +  apply (case_tac "y = 0")
   23.68 +  apply auto
   23.69 +  apply (subst pos_imp_zdiv_nonneg_iff, auto)
   23.70 +  apply (case_tac "y = 0")
   23.71 +  apply force
   23.72 +  apply (rule pos_mod_sign)
   23.73 +  apply arith
   23.74 +done
   23.75 +
   23.76 +lemma transfer_nat_int_relations:
   23.77 +    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
   23.78 +      (nat (x::int) = nat y) = (x = y)"
   23.79 +    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
   23.80 +      (nat (x::int) < nat y) = (x < y)"
   23.81 +    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
   23.82 +      (nat (x::int) <= nat y) = (x <= y)"
   23.83 +    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
   23.84 +      (nat (x::int) dvd nat y) = (x dvd y)"
   23.85 +  by (auto simp add: zdvd_int)
   23.86 +
   23.87 +declare TransferMorphism_nat_int[transfer add return:
   23.88 +  transfer_nat_int_numerals
   23.89 +  transfer_nat_int_functions
   23.90 +  transfer_nat_int_function_closures
   23.91 +  transfer_nat_int_relations
   23.92 +]
   23.93 +
   23.94 +
   23.95 +(* first-order quantifiers *)
   23.96 +
   23.97 +lemma transfer_nat_int_quantifiers:
   23.98 +    "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
   23.99 +    "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
  23.100 +  by (rule all_nat, rule ex_nat)
  23.101 +
  23.102 +(* should we restrict these? *)
  23.103 +lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
  23.104 +    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
  23.105 +  by auto
  23.106 +
  23.107 +lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
  23.108 +    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
  23.109 +  by auto
  23.110 +
  23.111 +declare TransferMorphism_nat_int[transfer add
  23.112 +  return: transfer_nat_int_quantifiers
  23.113 +  cong: all_cong ex_cong]
  23.114 +
  23.115 +
  23.116 +(* if *)
  23.117 +
  23.118 +lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
  23.119 +    nat (if P then x else y)"
  23.120 +  by auto
  23.121 +
  23.122 +declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
  23.123 +
  23.124 +
  23.125 +(* operations with sets *)
  23.126 +
  23.127 +definition
  23.128 +  nat_set :: "int set \<Rightarrow> bool"
  23.129 +where
  23.130 +  "nat_set S = (ALL x:S. x >= 0)"
  23.131 +
  23.132 +lemma transfer_nat_int_set_functions:
  23.133 +    "card A = card (int ` A)"
  23.134 +    "{} = nat ` ({}::int set)"
  23.135 +    "A Un B = nat ` (int ` A Un int ` B)"
  23.136 +    "A Int B = nat ` (int ` A Int int ` B)"
  23.137 +    "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
  23.138 +    "{..n} = nat ` {0..int n}"
  23.139 +    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
  23.140 +  apply (rule card_image [symmetric])
  23.141 +  apply (auto simp add: inj_on_def image_def)
  23.142 +  apply (rule_tac x = "int x" in bexI)
  23.143 +  apply auto
  23.144 +  apply (rule_tac x = "int x" in bexI)
  23.145 +  apply auto
  23.146 +  apply (rule_tac x = "int x" in bexI)
  23.147 +  apply auto
  23.148 +  apply (rule_tac x = "int x" in exI)
  23.149 +  apply auto
  23.150 +  apply (rule_tac x = "int x" in bexI)
  23.151 +  apply auto
  23.152 +  apply (rule_tac x = "int x" in bexI)
  23.153 +  apply auto
  23.154 +done
  23.155 +
  23.156 +lemma transfer_nat_int_set_function_closures:
  23.157 +    "nat_set {}"
  23.158 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
  23.159 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
  23.160 +    "x >= 0 \<Longrightarrow> nat_set {x..y}"
  23.161 +    "nat_set {x. x >= 0 & P x}"
  23.162 +    "nat_set (int ` C)"
  23.163 +    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
  23.164 +  unfolding nat_set_def apply auto
  23.165 +done
  23.166 +
  23.167 +lemma transfer_nat_int_set_relations:
  23.168 +    "(finite A) = (finite (int ` A))"
  23.169 +    "(x : A) = (int x : int ` A)"
  23.170 +    "(A = B) = (int ` A = int ` B)"
  23.171 +    "(A < B) = (int ` A < int ` B)"
  23.172 +    "(A <= B) = (int ` A <= int ` B)"
  23.173 +
  23.174 +  apply (rule iffI)
  23.175 +  apply (erule finite_imageI)
  23.176 +  apply (erule finite_imageD)
  23.177 +  apply (auto simp add: image_def expand_set_eq inj_on_def)
  23.178 +  apply (drule_tac x = "int x" in spec, auto)
  23.179 +  apply (drule_tac x = "int x" in spec, auto)
  23.180 +  apply (drule_tac x = "int x" in spec, auto)
  23.181 +done
  23.182 +
  23.183 +lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
  23.184 +    (int ` nat ` A = A)"
  23.185 +  by (auto simp add: nat_set_def image_def)
  23.186 +
  23.187 +lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
  23.188 +    {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
  23.189 +  by auto
  23.190 +
  23.191 +declare TransferMorphism_nat_int[transfer add
  23.192 +  return: transfer_nat_int_set_functions
  23.193 +    transfer_nat_int_set_function_closures
  23.194 +    transfer_nat_int_set_relations
  23.195 +    transfer_nat_int_set_return_embed
  23.196 +  cong: transfer_nat_int_set_cong
  23.197 +]
  23.198 +
  23.199 +
  23.200 +(* setsum and setprod *)
  23.201 +
  23.202 +(* this handles the case where the *domain* of f is nat *)
  23.203 +lemma transfer_nat_int_sum_prod:
  23.204 +    "setsum f A = setsum (%x. f (nat x)) (int ` A)"
  23.205 +    "setprod f A = setprod (%x. f (nat x)) (int ` A)"
  23.206 +  apply (subst setsum_reindex)
  23.207 +  apply (unfold inj_on_def, auto)
  23.208 +  apply (subst setprod_reindex)
  23.209 +  apply (unfold inj_on_def o_def, auto)
  23.210 +done
  23.211 +
  23.212 +(* this handles the case where the *range* of f is nat *)
  23.213 +lemma transfer_nat_int_sum_prod2:
  23.214 +    "setsum f A = nat(setsum (%x. int (f x)) A)"
  23.215 +    "setprod f A = nat(setprod (%x. int (f x)) A)"
  23.216 +  apply (subst int_setsum [symmetric])
  23.217 +  apply auto
  23.218 +  apply (subst int_setprod [symmetric])
  23.219 +  apply auto
  23.220 +done
  23.221 +
  23.222 +lemma transfer_nat_int_sum_prod_closure:
  23.223 +    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
  23.224 +    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
  23.225 +  unfolding nat_set_def
  23.226 +  apply (rule setsum_nonneg)
  23.227 +  apply auto
  23.228 +  apply (rule setprod_nonneg)
  23.229 +  apply auto
  23.230 +done
  23.231 +
  23.232 +(* this version doesn't work, even with nat_set A \<Longrightarrow>
  23.233 +      x : A \<Longrightarrow> x >= 0 turned on. Why not?
  23.234 +
  23.235 +  also: what does =simp=> do?
  23.236 +
  23.237 +lemma transfer_nat_int_sum_prod_closure:
  23.238 +    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
  23.239 +    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
  23.240 +  unfolding nat_set_def simp_implies_def
  23.241 +  apply (rule setsum_nonneg)
  23.242 +  apply auto
  23.243 +  apply (rule setprod_nonneg)
  23.244 +  apply auto
  23.245 +done
  23.246 +*)
  23.247 +
  23.248 +(* Making A = B in this lemma doesn't work. Why not?
  23.249 +   Also, why aren't setsum_cong and setprod_cong enough,
  23.250 +   with the previously mentioned rule turned on? *)
  23.251 +
  23.252 +lemma transfer_nat_int_sum_prod_cong:
  23.253 +    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
  23.254 +      setsum f A = setsum g B"
  23.255 +    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
  23.256 +      setprod f A = setprod g B"
  23.257 +  unfolding nat_set_def
  23.258 +  apply (subst setsum_cong, assumption)
  23.259 +  apply auto [2]
  23.260 +  apply (subst setprod_cong, assumption, auto)
  23.261 +done
  23.262 +
  23.263 +declare TransferMorphism_nat_int[transfer add
  23.264 +  return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
  23.265 +    transfer_nat_int_sum_prod_closure
  23.266 +  cong: transfer_nat_int_sum_prod_cong]
  23.267 +
  23.268 +(* lists *)
  23.269 +
  23.270 +definition
  23.271 +  embed_list :: "nat list \<Rightarrow> int list"
  23.272 +where
  23.273 +  "embed_list l = map int l";
  23.274 +
  23.275 +definition
  23.276 +  nat_list :: "int list \<Rightarrow> bool"
  23.277 +where
  23.278 +  "nat_list l = nat_set (set l)";
  23.279 +
  23.280 +definition
  23.281 +  return_list :: "int list \<Rightarrow> nat list"
  23.282 +where
  23.283 +  "return_list l = map nat l";
  23.284 +
  23.285 +thm nat_0_le;
  23.286 +
  23.287 +lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
  23.288 +    embed_list (return_list l) = l";
  23.289 +  unfolding embed_list_def return_list_def nat_list_def nat_set_def
  23.290 +  apply (induct l);
  23.291 +  apply auto;
  23.292 +done;
  23.293 +
  23.294 +lemma transfer_nat_int_list_functions:
  23.295 +  "l @ m = return_list (embed_list l @ embed_list m)"
  23.296 +  "[] = return_list []";
  23.297 +  unfolding return_list_def embed_list_def;
  23.298 +  apply auto;
  23.299 +  apply (induct l, auto);
  23.300 +  apply (induct m, auto);
  23.301 +done;
  23.302 +
  23.303 +(*
  23.304 +lemma transfer_nat_int_fold1: "fold f l x =
  23.305 +    fold (%x. f (nat x)) (embed_list l) x";
  23.306 +*)
  23.307 +
  23.308 +
  23.309 +
  23.310 +
  23.311 +subsection {* Set up transfer from int to nat *}
  23.312 +
  23.313 +(* set up transfer direction *)
  23.314 +
  23.315 +lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
  23.316 +  by (simp add: TransferMorphism_def)
  23.317 +
  23.318 +declare TransferMorphism_int_nat[transfer add
  23.319 +  mode: manual
  23.320 +(*  labels: int-nat *)
  23.321 +  return: nat_int
  23.322 +]
  23.323 +
  23.324 +
  23.325 +(* basic functions and relations *)
  23.326 +
  23.327 +definition
  23.328 +  is_nat :: "int \<Rightarrow> bool"
  23.329 +where
  23.330 +  "is_nat x = (x >= 0)"
  23.331 +
  23.332 +lemma transfer_int_nat_numerals:
  23.333 +    "0 = int 0"
  23.334 +    "1 = int 1"
  23.335 +    "2 = int 2"
  23.336 +    "3 = int 3"
  23.337 +  by auto
  23.338 +
  23.339 +lemma transfer_int_nat_functions:
  23.340 +    "(int x) + (int y) = int (x + y)"
  23.341 +    "(int x) * (int y) = int (x * y)"
  23.342 +    "tsub (int x) (int y) = int (x - y)"
  23.343 +    "(int x)^n = int (x^n)"
  23.344 +    "(int x) div (int y) = int (x div y)"
  23.345 +    "(int x) mod (int y) = int (x mod y)"
  23.346 +  by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
  23.347 +
  23.348 +lemma transfer_int_nat_function_closures:
  23.349 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
  23.350 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
  23.351 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
  23.352 +    "is_nat x \<Longrightarrow> is_nat (x^n)"
  23.353 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
  23.354 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
  23.355 +    "is_nat 0"
  23.356 +    "is_nat 1"
  23.357 +    "is_nat 2"
  23.358 +    "is_nat 3"
  23.359 +    "is_nat (int z)"
  23.360 +  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
  23.361 +
  23.362 +lemma transfer_int_nat_relations:
  23.363 +    "(int x = int y) = (x = y)"
  23.364 +    "(int x < int y) = (x < y)"
  23.365 +    "(int x <= int y) = (x <= y)"
  23.366 +    "(int x dvd int y) = (x dvd y)"
  23.367 +    "(even (int x)) = (even x)"
  23.368 +  by (auto simp add: zdvd_int even_nat_def)
  23.369 +
  23.370 +lemma UNIV_apply:
  23.371 +  "UNIV x = True"
  23.372 +  by (simp add: top_fun_eq top_bool_eq)
  23.373 +
  23.374 +declare TransferMorphism_int_nat[transfer add return:
  23.375 +  transfer_int_nat_numerals
  23.376 +  transfer_int_nat_functions
  23.377 +  transfer_int_nat_function_closures
  23.378 +  transfer_int_nat_relations
  23.379 +  UNIV_apply
  23.380 +]
  23.381 +
  23.382 +
  23.383 +(* first-order quantifiers *)
  23.384 +
  23.385 +lemma transfer_int_nat_quantifiers:
  23.386 +    "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
  23.387 +    "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
  23.388 +  apply (subst all_nat)
  23.389 +  apply auto [1]
  23.390 +  apply (subst ex_nat)
  23.391 +  apply auto
  23.392 +done
  23.393 +
  23.394 +declare TransferMorphism_int_nat[transfer add
  23.395 +  return: transfer_int_nat_quantifiers]
  23.396 +
  23.397 +
  23.398 +(* if *)
  23.399 +
  23.400 +lemma int_if_cong: "(if P then (int x) else (int y)) =
  23.401 +    int (if P then x else y)"
  23.402 +  by auto
  23.403 +
  23.404 +declare TransferMorphism_int_nat [transfer add return: int_if_cong]
  23.405 +
  23.406 +
  23.407 +
  23.408 +(* operations with sets *)
  23.409 +
  23.410 +lemma transfer_int_nat_set_functions:
  23.411 +    "nat_set A \<Longrightarrow> card A = card (nat ` A)"
  23.412 +    "{} = int ` ({}::nat set)"
  23.413 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
  23.414 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
  23.415 +    "{x. x >= 0 & P x} = int ` {x. P(int x)}"
  23.416 +    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
  23.417 +       (* need all variants of these! *)
  23.418 +  by (simp_all only: is_nat_def transfer_nat_int_set_functions
  23.419 +          transfer_nat_int_set_function_closures
  23.420 +          transfer_nat_int_set_return_embed nat_0_le
  23.421 +          cong: transfer_nat_int_set_cong)
  23.422 +
  23.423 +lemma transfer_int_nat_set_function_closures:
  23.424 +    "nat_set {}"
  23.425 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
  23.426 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
  23.427 +    "is_nat x \<Longrightarrow> nat_set {x..y}"
  23.428 +    "nat_set {x. x >= 0 & P x}"
  23.429 +    "nat_set (int ` C)"
  23.430 +    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
  23.431 +  by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
  23.432 +
  23.433 +lemma transfer_int_nat_set_relations:
  23.434 +    "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
  23.435 +    "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
  23.436 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
  23.437 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
  23.438 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
  23.439 +  by (simp_all only: is_nat_def transfer_nat_int_set_relations
  23.440 +    transfer_nat_int_set_return_embed nat_0_le)
  23.441 +
  23.442 +lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
  23.443 +  by (simp only: transfer_nat_int_set_relations
  23.444 +    transfer_nat_int_set_function_closures
  23.445 +    transfer_nat_int_set_return_embed nat_0_le)
  23.446 +
  23.447 +lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
  23.448 +    {(x::nat). P x} = {x. P' x}"
  23.449 +  by auto
  23.450 +
  23.451 +declare TransferMorphism_int_nat[transfer add
  23.452 +  return: transfer_int_nat_set_functions
  23.453 +    transfer_int_nat_set_function_closures
  23.454 +    transfer_int_nat_set_relations
  23.455 +    transfer_int_nat_set_return_embed
  23.456 +  cong: transfer_int_nat_set_cong
  23.457 +]
  23.458 +
  23.459 +
  23.460 +(* setsum and setprod *)
  23.461 +
  23.462 +(* this handles the case where the *domain* of f is int *)
  23.463 +lemma transfer_int_nat_sum_prod:
  23.464 +    "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
  23.465 +    "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
  23.466 +  apply (subst setsum_reindex)
  23.467 +  apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
  23.468 +  apply (subst setprod_reindex)
  23.469 +  apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
  23.470 +            cong: setprod_cong)
  23.471 +done
  23.472 +
  23.473 +(* this handles the case where the *range* of f is int *)
  23.474 +lemma transfer_int_nat_sum_prod2:
  23.475 +    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
  23.476 +    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
  23.477 +      setprod f A = int(setprod (%x. nat (f x)) A)"
  23.478 +  unfolding is_nat_def
  23.479 +  apply (subst int_setsum, auto)
  23.480 +  apply (subst int_setprod, auto simp add: cong: setprod_cong)
  23.481 +done
  23.482 +
  23.483 +declare TransferMorphism_int_nat[transfer add
  23.484 +  return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
  23.485 +  cong: setsum_cong setprod_cong]
  23.486 +
  23.487 +end
    24.1 --- a/src/HOL/Nominal/Examples/Class.thy	Fri Sep 11 20:58:29 2009 +1000
    24.2 +++ b/src/HOL/Nominal/Examples/Class.thy	Thu Sep 17 14:17:37 2009 +1000
    24.3 @@ -11134,7 +11134,6 @@
    24.4    shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
    24.5    and   "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
    24.6  apply(simp add: lfp_def)
    24.7 -apply(simp add: Inf_set_eq)
    24.8  apply(simp add: big_inter_eqvt)
    24.9  apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
   24.10  apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
   24.11 @@ -11146,7 +11145,6 @@
   24.12  apply(drule subseteq_eqvt(1)[THEN iffD2])
   24.13  apply(simp add: perm_bool)
   24.14  apply(simp add: lfp_def)
   24.15 -apply(simp add: Inf_set_eq)
   24.16  apply(simp add: big_inter_eqvt)
   24.17  apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
   24.18  apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
    25.1 --- a/src/HOL/Predicate.thy	Fri Sep 11 20:58:29 2009 +1000
    25.2 +++ b/src/HOL/Predicate.thy	Thu Sep 17 14:17:37 2009 +1000
    25.3 @@ -366,7 +366,7 @@
    25.4  definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
    25.5    "P \<guillemotright>= f = Pred (\<lambda>x. (\<exists>y. eval P y \<and> eval (f y) x))"
    25.6  
    25.7 -instantiation pred :: (type) complete_lattice
    25.8 +instantiation pred :: (type) "{complete_lattice, boolean_algebra}"
    25.9  begin
   25.10  
   25.11  definition
   25.12 @@ -393,10 +393,16 @@
   25.13  definition
   25.14    [code del]: "\<Squnion>A = Pred (SUPR A eval)"
   25.15  
   25.16 -instance by default
   25.17 -  (auto simp add: less_eq_pred_def less_pred_def
   25.18 +definition
   25.19 +  "- P = Pred (- eval P)"
   25.20 +
   25.21 +definition
   25.22 +  "P - Q = Pred (eval P - eval Q)"
   25.23 +
   25.24 +instance proof
   25.25 +qed (auto simp add: less_eq_pred_def less_pred_def
   25.26      inf_pred_def sup_pred_def bot_pred_def top_pred_def
   25.27 -    Inf_pred_def Sup_pred_def,
   25.28 +    Inf_pred_def Sup_pred_def uminus_pred_def minus_pred_def fun_Compl_def bool_Compl_def,
   25.29      auto simp add: le_fun_def less_fun_def le_bool_def less_bool_def
   25.30      eval_inject mem_def)
   25.31  
   25.32 @@ -464,6 +470,127 @@
   25.33  lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
   25.34    unfolding sup_pred_def by auto
   25.35  
   25.36 +lemma single_not_bot [simp]:
   25.37 +  "single x \<noteq> \<bottom>"
   25.38 +  by (auto simp add: single_def bot_pred_def expand_fun_eq)
   25.39 +
   25.40 +lemma not_bot:
   25.41 +  assumes "A \<noteq> \<bottom>"
   25.42 +  obtains x where "eval A x"
   25.43 +using assms by (cases A)
   25.44 +  (auto simp add: bot_pred_def, auto simp add: mem_def)
   25.45 +  
   25.46 +
   25.47 +subsubsection {* Emptiness check and definite choice *}
   25.48 +
   25.49 +definition is_empty :: "'a pred \<Rightarrow> bool" where
   25.50 +  "is_empty A \<longleftrightarrow> A = \<bottom>"
   25.51 +
   25.52 +lemma is_empty_bot:
   25.53 +  "is_empty \<bottom>"
   25.54 +  by (simp add: is_empty_def)
   25.55 +
   25.56 +lemma not_is_empty_single:
   25.57 +  "\<not> is_empty (single x)"
   25.58 +  by (auto simp add: is_empty_def single_def bot_pred_def expand_fun_eq)
   25.59 +
   25.60 +lemma is_empty_sup:
   25.61 +  "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
   25.62 +  by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2)
   25.63 +
   25.64 +definition singleton :: "'a pred \<Rightarrow> 'a" where
   25.65 +  "singleton A = (if \<exists>!x. eval A x then THE x. eval A x else undefined)"
   25.66 +
   25.67 +lemma singleton_eqI:
   25.68 +  "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton A = x"
   25.69 +  by (auto simp add: singleton_def)
   25.70 +
   25.71 +lemma eval_singletonI:
   25.72 +  "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton A)"
   25.73 +proof -
   25.74 +  assume assm: "\<exists>!x. eval A x"
   25.75 +  then obtain x where "eval A x" ..
   25.76 +  moreover with assm have "singleton A = x" by (rule singleton_eqI)
   25.77 +  ultimately show ?thesis by simp 
   25.78 +qed
   25.79 +
   25.80 +lemma single_singleton:
   25.81 +  "\<exists>!x. eval A x \<Longrightarrow> single (singleton A) = A"
   25.82 +proof -
   25.83 +  assume assm: "\<exists>!x. eval A x"
   25.84 +  then have "eval A (singleton A)"
   25.85 +    by (rule eval_singletonI)
   25.86 +  moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton A = x"
   25.87 +    by (rule singleton_eqI)
   25.88 +  ultimately have "eval (single (singleton A)) = eval A"
   25.89 +    by (simp (no_asm_use) add: single_def expand_fun_eq) blast
   25.90 +  then show ?thesis by (simp add: eval_inject)
   25.91 +qed
   25.92 +
   25.93 +lemma singleton_undefinedI:
   25.94 +  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton A = undefined"
   25.95 +  by (simp add: singleton_def)
   25.96 +
   25.97 +lemma singleton_bot:
   25.98 +  "singleton \<bottom> = undefined"
   25.99 +  by (auto simp add: bot_pred_def intro: singleton_undefinedI)
  25.100 +
  25.101 +lemma singleton_single:
  25.102 +  "singleton (single x) = x"
  25.103 +  by (auto simp add: intro: singleton_eqI singleI elim: singleE)
  25.104 +
  25.105 +lemma singleton_sup_single_single:
  25.106 +  "singleton (single x \<squnion> single y) = (if x = y then x else undefined)"
  25.107 +proof (cases "x = y")
  25.108 +  case True then show ?thesis by (simp add: singleton_single)
  25.109 +next
  25.110 +  case False
  25.111 +  have "eval (single x \<squnion> single y) x"
  25.112 +    and "eval (single x \<squnion> single y) y"
  25.113 +  by (auto intro: supI1 supI2 singleI)
  25.114 +  with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)"
  25.115 +    by blast
  25.116 +  then have "singleton (single x \<squnion> single y) = undefined"
  25.117 +    by (rule singleton_undefinedI)
  25.118 +  with False show ?thesis by simp
  25.119 +qed
  25.120 +
  25.121 +lemma singleton_sup_aux:
  25.122 +  "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
  25.123 +    else if B = \<bottom> then singleton A
  25.124 +    else singleton
  25.125 +      (single (singleton A) \<squnion> single (singleton B)))"
  25.126 +proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
  25.127 +  case True then show ?thesis by (simp add: single_singleton)
  25.128 +next
  25.129 +  case False
  25.130 +  from False have A_or_B:
  25.131 +    "singleton A = undefined \<or> singleton B = undefined"
  25.132 +    by (auto intro!: singleton_undefinedI)
  25.133 +  then have rhs: "singleton
  25.134 +    (single (singleton A) \<squnion> single (singleton B)) = undefined"
  25.135 +    by (auto simp add: singleton_sup_single_single singleton_single)
  25.136 +  from False have not_unique:
  25.137 +    "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp
  25.138 +  show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>")
  25.139 +    case True
  25.140 +    then obtain a b where a: "eval A a" and b: "eval B b"
  25.141 +      by (blast elim: not_bot)
  25.142 +    with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)"
  25.143 +      by (auto simp add: sup_pred_def bot_pred_def)
  25.144 +    then have "singleton (A \<squnion> B) = undefined" by (rule singleton_undefinedI)
  25.145 +    with True rhs show ?thesis by simp
  25.146 +  next
  25.147 +    case False then show ?thesis by auto
  25.148 +  qed
  25.149 +qed
  25.150 +
  25.151 +lemma singleton_sup:
  25.152 +  "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
  25.153 +    else if B = \<bottom> then singleton A
  25.154 +    else if singleton A = singleton B then singleton A else undefined)"
  25.155 +using singleton_sup_aux [of A B] by (simp only: singleton_sup_single_single)
  25.156 +
  25.157  
  25.158  subsubsection {* Derived operations *}
  25.159  
  25.160 @@ -630,6 +757,46 @@
  25.161  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
  25.162    "map f P = P \<guillemotright>= (single o f)"
  25.163  
  25.164 +primrec null :: "'a seq \<Rightarrow> bool" where
  25.165 +    "null Empty \<longleftrightarrow> True"
  25.166 +  | "null (Insert x P) \<longleftrightarrow> False"
  25.167 +  | "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
  25.168 +
  25.169 +lemma null_is_empty:
  25.170 +  "null xq \<longleftrightarrow> is_empty (pred_of_seq xq)"
  25.171 +  by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup)
  25.172 +
  25.173 +lemma is_empty_code [code]:
  25.174 +  "is_empty (Seq f) \<longleftrightarrow> null (f ())"
  25.175 +  by (simp add: null_is_empty Seq_def)
  25.176 +
  25.177 +primrec the_only :: "'a seq \<Rightarrow> 'a" where
  25.178 +  [code del]: "the_only Empty = undefined"
  25.179 +  | "the_only (Insert x P) = (if is_empty P then x else let y = singleton P in if x = y then x else undefined)"
  25.180 +  | "the_only (Join P xq) = (if is_empty P then the_only xq else if null xq then singleton P
  25.181 +       else let x = singleton P; y = the_only xq in
  25.182 +       if x = y then x else undefined)"
  25.183 +
  25.184 +lemma the_only_singleton:
  25.185 +  "the_only xq = singleton (pred_of_seq xq)"
  25.186 +  by (induct xq)
  25.187 +    (auto simp add: singleton_bot singleton_single is_empty_def
  25.188 +    null_is_empty Let_def singleton_sup)
  25.189 +
  25.190 +lemma singleton_code [code]:
  25.191 +  "singleton (Seq f) = (case f ()
  25.192 +   of Empty \<Rightarrow> undefined
  25.193 +    | Insert x P \<Rightarrow> if is_empty P then x
  25.194 +        else let y = singleton P in
  25.195 +          if x = y then x else undefined
  25.196 +    | Join P xq \<Rightarrow> if is_empty P then the_only xq
  25.197 +        else if null xq then singleton P
  25.198 +        else let x = singleton P; y = the_only xq in
  25.199 +          if x = y then x else undefined)"
  25.200 +  by (cases "f ()")
  25.201 +   (auto simp add: Seq_def the_only_singleton is_empty_def
  25.202 +      null_is_empty singleton_bot singleton_single singleton_sup Let_def)
  25.203 +
  25.204  ML {*
  25.205  signature PREDICATE =
  25.206  sig
  25.207 @@ -707,7 +874,7 @@
  25.208    bind (infixl "\<guillemotright>=" 70)
  25.209  
  25.210  hide (open) type pred seq
  25.211 -hide (open) const Pred eval single bind if_pred not_pred
  25.212 -  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map
  25.213 +hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
  25.214 +  Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map
  25.215  
  25.216  end
    26.1 --- a/src/HOL/Presburger.thy	Fri Sep 11 20:58:29 2009 +1000
    26.2 +++ b/src/HOL/Presburger.thy	Thu Sep 17 14:17:37 2009 +1000
    26.3 @@ -382,15 +382,22 @@
    26.4  
    26.5  lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
    26.6    by simp_all
    26.7 +
    26.8  text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
    26.9 -lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   26.10 +
   26.11 +lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
   26.12    by (simp split add: split_nat)
   26.13  
   26.14 -lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
   26.15 -  apply (auto split add: split_nat)
   26.16 -  apply (rule_tac x="int x" in exI, simp)
   26.17 -  apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
   26.18 -  done
   26.19 +lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
   26.20 +proof
   26.21 +  assume "\<exists>x. P x"
   26.22 +  then obtain x where "P x" ..
   26.23 +  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
   26.24 +  then show "\<exists>x\<ge>0. P (nat x)" ..
   26.25 +next
   26.26 +  assume "\<exists>x\<ge>0. P (nat x)"
   26.27 +  then show "\<exists>x. P x" by auto
   26.28 +qed
   26.29  
   26.30  lemma zdiff_int_split: "P (int (x - y)) =
   26.31    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
    27.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Fri Sep 11 20:58:29 2009 +1000
    27.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Sep 17 14:17:37 2009 +1000
    27.3 @@ -7,7 +7,7 @@
    27.4  signature ATP_MINIMAL =
    27.5  sig
    27.6    val minimalize: AtpManager.prover -> string -> int -> Proof.state ->
    27.7 -    (string * thm list) list -> (string * thm list) list option * string
    27.8 +    (string * thm list) list -> ((string * thm list) list * int) option * string
    27.9  end
   27.10  
   27.11  structure AtpMinimal: ATP_MINIMAL =
   27.12 @@ -69,9 +69,14 @@
   27.13           forall e in v. ~p(v \ e)
   27.14     *)
   27.15    fun minimal p s =
   27.16 -    case min p [] s of
   27.17 -      [x] => if p [] then [] else [x]
   27.18 -    | m => m
   27.19 +    let val c = ref 0
   27.20 +        fun pc xs = (c := !c + 1; p xs)
   27.21 +    in
   27.22 +    (case min pc [] s of
   27.23 +       [x] => if pc [] then [] else [x]
   27.24 +     | m => m,
   27.25 +     !c)
   27.26 +    end
   27.27  end
   27.28  
   27.29  
   27.30 @@ -150,13 +155,14 @@
   27.31                filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
   27.32              else
   27.33                name_thms_pairs
   27.34 -          val min_thms = if null to_use then []
   27.35 +          val (min_thms, n) = if null to_use then ([], 0)
   27.36              else minimal (test_thms (SOME filtered)) to_use
   27.37            val min_names = order_unique (map fst min_thms)
   27.38 +          val _ = println ("Interations: " ^ string_of_int n)
   27.39            val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
   27.40            val _ = debug_fn (fn () => print_names min_thms)
   27.41          in
   27.42 -          answer' (SOME min_thms) ("Try this command: " ^
   27.43 +          answer' (SOME(min_thms,n)) ("Try this command: " ^
   27.44              Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
   27.45          end
   27.46      | (Timeout, _) =>
   27.47 @@ -167,7 +173,7 @@
   27.48      | (Failure, _) =>
   27.49          answer'' "Failure: No proof with the theorems supplied")
   27.50      handle ResHolClause.TOO_TRIVIAL =>
   27.51 -        answer' (SOME []) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
   27.52 +        answer' (SOME ([],0)) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
   27.53      | ERROR msg =>
   27.54          answer'' ("Error: " ^ msg)
   27.55    end
    28.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Sep 11 20:58:29 2009 +1000
    28.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Sep 17 14:17:37 2009 +1000
    28.3 @@ -79,14 +79,14 @@
    28.4        preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
    28.5  
    28.6      (* write out problem file and call prover *)
    28.7 -    fun cmd_line probfile = "TIMEFORMAT='%3U'; ((time " ^ space_implode " "
    28.8 -      [File.shell_path cmd, args, File.platform_path probfile] ^ ") 2>&1)"
    28.9 +    val perl_script = "perl -w $ISABELLE_ATP_MANAGER/lib/scripts/local_atp.pl"
   28.10 +    fun cmd_line probfile = perl_script ^ " '" ^ space_implode " "
   28.11 +      [File.shell_path cmd, args, File.platform_path probfile] ^ "'"
   28.12      fun split_time s =
   28.13        let
   28.14          val split = String.tokens (fn c => str c = "\n")
   28.15          val (proof, t) = s |> split |> split_last |> apfst cat_lines
   28.16 -        val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
   28.17 -        val time = num --| Scan.$$ "." -- num >> (fn (a, b) => a * 1000 + b)
   28.18 +        val time = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
   28.19          val as_time = the_default 0 o Scan.read Symbol.stopper time o explode
   28.20        in (proof, as_time t) end
   28.21      fun run_on probfile =
    29.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.2 +++ b/src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl	Thu Sep 17 14:17:37 2009 +1000
    29.3 @@ -0,0 +1,15 @@
    29.4 +use POSIX qw(setsid);
    29.5 +
    29.6 +$SIG{'INT'} = "DEFAULT";
    29.7 +
    29.8 +defined (my $pid = fork) or die "$!";
    29.9 +if (not $pid) {
   29.10 +  POSIX::setsid or die $!;
   29.11 +  exec @ARGV;
   29.12 +}
   29.13 +else {
   29.14 +  wait;
   29.15 +  my ($user, $system, $cuser, $csystem) = times;
   29.16 +  my $time = ($user + $cuser) * 1000;
   29.17 +  print "$time\n";
   29.18 +}
    30.1 --- a/src/HOL/Tools/Function/fundef_core.ML	Fri Sep 11 20:58:29 2009 +1000
    30.2 +++ b/src/HOL/Tools/Function/fundef_core.ML	Thu Sep 17 14:17:37 2009 +1000
    30.3 @@ -478,7 +478,7 @@
    30.4  fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
    30.5      let
    30.6        val f_def =
    30.7 -          Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
    30.8 +          Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
    30.9                                  Abs ("y", ranT, G $ Bound 1 $ Bound 0))
   30.10                |> Syntax.check_term lthy
   30.11  
   30.12 @@ -767,7 +767,7 @@
   30.13        val R' = Free ("R", fastype_of R)
   30.14  
   30.15        val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
   30.16 -      val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
   30.17 +      val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
   30.18  
   30.19        val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   30.20  
    31.1 --- a/src/HOL/Tools/res_reconstruct.ML	Fri Sep 11 20:58:29 2009 +1000
    31.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Thu Sep 17 14:17:37 2009 +1000
    31.3 @@ -523,7 +523,7 @@
    31.4        let
    31.5        val last_axiom = Vector.length thm_names
    31.6        fun is_axiom n = n <= last_axiom
    31.7 -      fun is_conj n = n >= #1 conj_count andalso n < #1 conj_count + #2 conj_count
    31.8 +      fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
    31.9        fun getname i = Vector.sub(thm_names, i-1)
   31.10        in
   31.11          (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
    32.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.2 +++ b/src/HOL/Tools/transfer.ML	Thu Sep 17 14:17:37 2009 +1000
    32.3 @@ -0,0 +1,241 @@
    32.4 +(*  Author:     Amine Chaieb, University of Cambridge, 2009
    32.5 +                Jeremy Avigad, Carnegie Mellon University
    32.6 +*)
    32.7 +
    32.8 +signature TRANSFER =
    32.9 +sig
   32.10 +  type data
   32.11 +  type entry
   32.12 +  val get: Proof.context -> data
   32.13 +  val del: attribute
   32.14 +  val setup: theory -> theory
   32.15 +end;
   32.16 +
   32.17 +structure Transfer : TRANSFER =
   32.18 +struct
   32.19 +
   32.20 +val eq_thm = Thm.eq_thm;
   32.21 +
   32.22 +type entry = {inj : thm list, emb : thm list, ret : thm list, cong : thm list,
   32.23 +  guess : bool, hints : string list}; 
   32.24 +type data = simpset * (thm * entry) list;
   32.25 +
   32.26 +structure Data = GenericDataFun
   32.27 +(
   32.28 +  type T = data;
   32.29 +  val empty = (HOL_ss, []);
   32.30 +  val extend  = I;
   32.31 +  fun merge _ ((ss1, e1), (ss2, e2)) =
   32.32 +    (merge_ss (ss1, ss2), AList.merge eq_thm (K true) (e1, e2));
   32.33 +);
   32.34 +
   32.35 +val get = Data.get o Context.Proof;
   32.36 +
   32.37 +fun del_data key = apsnd (remove (eq_fst eq_thm) (key, []));
   32.38 +
   32.39 +val del = Thm.declaration_attribute (Data.map o del_data);
   32.40 +val add_ss = Thm.declaration_attribute 
   32.41 +   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
   32.42 +
   32.43 +val del_ss = Thm.declaration_attribute 
   32.44 +   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
   32.45 +
   32.46 +val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
   32.47 +
   32.48 +fun merge_update eq m (k,v) [] = [(k,v)]
   32.49 +  | merge_update eq m (k,v) ((k',v')::al) = 
   32.50 +           if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
   32.51 +
   32.52 +fun C f x y = f y x
   32.53 +
   32.54 +fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} = 
   32.55 + HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
   32.56 +
   32.57 +fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th = 
   32.58 + let 
   32.59 +  val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
   32.60 +  val (aT,bT) = 
   32.61 +     let val T = typ_of (ctyp_of_term a) 
   32.62 +     in (Term.range_type T, Term.domain_type T)
   32.63 +     end
   32.64 +  val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
   32.65 +  val ns = filter (fn i => Type.could_unify (snd i, aT) andalso not (fst (fst i) mem_string leave)) (Term.add_vars (prop_of th) [])
   32.66 +  val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt'
   32.67 +  val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns
   32.68 +  val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
   32.69 +  val cis = map (Thm.capply a) cfis
   32.70 +  val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
   32.71 +  val th1 = Drule.cterm_instantiate (cns~~ cis) th
   32.72 +  val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
   32.73 +  val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e)) 
   32.74 +                                         (fold_rev implies_intr (map cprop_of hs) th2)
   32.75 +in hd (Variable.export ctxt''' ctxt0 [th3]) end;
   32.76 +
   32.77 +local
   32.78 +fun transfer_ruleh a D leave ctxt th = 
   32.79 + let val (ss,al) = get ctxt
   32.80 +     val a0 = cterm_of (ProofContext.theory_of ctxt) a
   32.81 +     val D0 = cterm_of (ProofContext.theory_of ctxt) D
   32.82 +     fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th' 
   32.83 +                 in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
   32.84 +                 end
   32.85 + in case get_first h al of
   32.86 +      SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
   32.87 +    | NONE => error "Transfer: corresponding instance not found in context-data"
   32.88 + end
   32.89 +in fun transfer_rule (a,D) leave (gctxt,th) = 
   32.90 +   (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
   32.91 +end;
   32.92 +
   32.93 +fun  splits P [] = []
   32.94 +   | splits P (xxs as (x::xs)) = 
   32.95 +    let val pss = filter (P x) xxs
   32.96 +        val qss = filter_out (P x) xxs
   32.97 +    in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
   32.98 +    end
   32.99 +
  32.100 +fun all_transfers leave (gctxt,th) = 
  32.101 + let 
  32.102 +  val ctxt = Context.proof_of gctxt
  32.103 +  val tys = map snd (Term.add_vars (prop_of th) [])
  32.104 +  val _ = if null tys then error "transfer: Unable to guess instance" else ()
  32.105 +  val tyss = splits (curry Type.could_unify) tys 
  32.106 +  val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
  32.107 +  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
  32.108 +  val insts = 
  32.109 +    map_filter (fn tys => 
  32.110 +          get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k)) 
  32.111 +                                  then SOME (get_aD k, ss) 
  32.112 +                                  else NONE) (snd (get ctxt))) tyss
  32.113 +  val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
  32.114 +  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
  32.115 +  val cth = Conjunction.intr_balanced ths
  32.116 + in (gctxt, cth)
  32.117 + end;
  32.118 +
  32.119 +fun transfer_rule_by_hint ls leave (gctxt,th) = 
  32.120 + let 
  32.121 +  val ctxt = Context.proof_of gctxt
  32.122 +  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
  32.123 +  val insts = 
  32.124 +    map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls 
  32.125 +          then SOME (get_aD k, e) else NONE)
  32.126 +        (snd (get ctxt))
  32.127 +  val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
  32.128 +  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
  32.129 +  val cth = Conjunction.intr_balanced ths
  32.130 + in (gctxt, cth)
  32.131 + end;
  32.132 +
  32.133 +
  32.134 +fun transferred_attribute ls NONE leave = 
  32.135 +         if null ls then all_transfers leave else transfer_rule_by_hint ls leave
  32.136 +  | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
  32.137 +
  32.138 +                                                    (* Add data to the context *)
  32.139 +fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
  32.140 +                      ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
  32.141 +                       {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
  32.142 + = 
  32.143 + let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
  32.144 + {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2, 
  32.145 +  ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
  32.146 +  hints = subtract (op = : string*string -> bool) hints0 
  32.147 +            (hints1 union_string hints2)}
  32.148 + end;
  32.149 +
  32.150 +local
  32.151 + val h = curry (merge Thm.eq_thm)
  32.152 +in
  32.153 +fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
  32.154 +                   {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) = 
  32.155 +    {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
  32.156 +end; 
  32.157 +
  32.158 +fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
  32.159 +  Thm.declaration_attribute (fn key => fn context => context |> Data.map
  32.160 +   (fn (ss, al) => 
  32.161 +     let
  32.162 +      val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key) 
  32.163 +                in 0 end) 
  32.164 +                handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
  32.165 +      val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
  32.166 +      val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
  32.167 +      val entry = 
  32.168 +        if g then 
  32.169 +         let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
  32.170 +             val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
  32.171 +             val inj' = if null inja then #inj (case AList.lookup eq_thm al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual") 
  32.172 +                        else inja
  32.173 +             val ret' = merge Thm.eq_thm (reta,  map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
  32.174 +         in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end 
  32.175 +        else e0
  32.176 +    in (ss, merge_update eq_thm (gen_merge_entries ed) (key, entry) al)
  32.177 +    end));
  32.178 +
  32.179 +
  32.180 +
  32.181 +(* concrete syntax *)
  32.182 +
  32.183 +local
  32.184 +
  32.185 +fun keyword k = Scan.lift (Args.$$$ k) >> K ()
  32.186 +fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
  32.187 +
  32.188 +val congN = "cong"
  32.189 +val injN = "inj"
  32.190 +val embedN = "embed"
  32.191 +val returnN = "return"
  32.192 +val addN = "add"
  32.193 +val delN = "del"
  32.194 +val modeN = "mode"
  32.195 +val automaticN = "automatic"
  32.196 +val manualN = "manual"
  32.197 +val directionN = "direction"
  32.198 +val labelsN = "labels"
  32.199 +val leavingN = "leaving"
  32.200 +
  32.201 +val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
  32.202 +
  32.203 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
  32.204 +val terms = thms >> map Drule.dest_term
  32.205 +val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd) 
  32.206 +val name = Scan.lift Args.name
  32.207 +val names = Scan.repeat (Scan.unless any_keyword name)
  32.208 +fun optional scan = Scan.optional scan []
  32.209 +fun optional2 scan = Scan.optional scan ([],[])
  32.210 +
  32.211 +val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
  32.212 +val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
  32.213 +val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
  32.214 +val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
  32.215 +val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
  32.216 +val addscan = Scan.unless any_keyword (keyword addN)
  32.217 +val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
  32.218 +val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
  32.219 +
  32.220 +val transf_add = addscan |-- entry
  32.221 +in
  32.222 +
  32.223 +val install_att_syntax =
  32.224 +  (Scan.lift (Args.$$$ delN >> K del) ||
  32.225 +    transf_add
  32.226 +    >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
  32.227 +
  32.228 +val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
  32.229 +  -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
  32.230 +
  32.231 +end;
  32.232 +
  32.233 +
  32.234 +(* theory setup *)
  32.235 +
  32.236 +val setup =
  32.237 +  Attrib.setup @{binding transfer} install_att_syntax
  32.238 +    "Installs transfer data" #>
  32.239 +  Attrib.setup @{binding transfer_simps} (Attrib.add_del add_ss del_ss)
  32.240 +    "simp rules for transfer" #>
  32.241 +  Attrib.setup @{binding transferred} transferred_att_syntax
  32.242 +    "Transfers theorems";
  32.243 +
  32.244 +end;
    33.1 --- a/src/HOL/Tools/transfer_data.ML	Fri Sep 11 20:58:29 2009 +1000
    33.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.3 @@ -1,243 +0,0 @@
    33.4 -(*  Title:      Tools/transfer.ML
    33.5 -    Author:     Amine Chaieb, University of Cambridge, 2009
    33.6 -                Jeremy Avigad, Carnegie Mellon University
    33.7 -*)
    33.8 -
    33.9 -signature TRANSFER_DATA =
   33.10 -sig
   33.11 -  type data
   33.12 -  type entry
   33.13 -  val get: Proof.context -> data
   33.14 -  val del: attribute
   33.15 -  val add: attribute 
   33.16 -  val setup: theory -> theory
   33.17 -end;
   33.18 -
   33.19 -structure TransferData (* : TRANSFER_DATA*) =
   33.20 -struct
   33.21 -type entry = {inj : thm list , emb : thm list , ret : thm list , cong : thm list, guess : bool, hints : string list}; 
   33.22 -type data = simpset * (thm * entry) list;
   33.23 -
   33.24 -val eq_key = Thm.eq_thm;
   33.25 -fun eq_data arg = eq_fst eq_key arg;
   33.26 -
   33.27 -structure Data = GenericDataFun
   33.28 -(
   33.29 -  type T = data;
   33.30 -  val empty = (HOL_ss, []);
   33.31 -  val extend  = I;
   33.32 -  fun merge _ ((ss, e), (ss', e')) =
   33.33 -    (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
   33.34 -);
   33.35 -
   33.36 -val get = Data.get o Context.Proof;
   33.37 -
   33.38 -fun del_data key = apsnd (remove eq_data (key, []));
   33.39 -
   33.40 -val del = Thm.declaration_attribute (Data.map o del_data);
   33.41 -val add_ss = Thm.declaration_attribute 
   33.42 -   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
   33.43 -
   33.44 -val del_ss = Thm.declaration_attribute 
   33.45 -   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
   33.46 -
   33.47 -val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
   33.48 -
   33.49 -fun merge_update eq m (k,v) [] = [(k,v)]
   33.50 -  | merge_update eq m (k,v) ((k',v')::al) = 
   33.51 -           if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
   33.52 -
   33.53 -fun C f x y = f y x
   33.54 -
   33.55 -fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} = 
   33.56 - HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
   33.57 -
   33.58 -fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th = 
   33.59 - let 
   33.60 -  val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
   33.61 -  val (aT,bT) = 
   33.62 -     let val T = typ_of (ctyp_of_term a) 
   33.63 -     in (Term.range_type T, Term.domain_type T)
   33.64 -     end
   33.65 -  val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
   33.66 -  val ns = filter (fn i => Type.could_unify (snd i, aT) andalso not (fst (fst i) mem_string leave)) (Term.add_vars (prop_of th) [])
   33.67 -  val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt'
   33.68 -  val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns
   33.69 -  val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
   33.70 -  val cis = map (Thm.capply a) cfis
   33.71 -  val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
   33.72 -  val th1 = Drule.cterm_instantiate (cns~~ cis) th
   33.73 -  val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
   33.74 -  val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e)) 
   33.75 -                                         (fold_rev implies_intr (map cprop_of hs) th2)
   33.76 -in hd (Variable.export ctxt''' ctxt0 [th3]) end;
   33.77 -
   33.78 -local
   33.79 -fun transfer_ruleh a D leave ctxt th = 
   33.80 - let val (ss,al) = get ctxt
   33.81 -     val a0 = cterm_of (ProofContext.theory_of ctxt) a
   33.82 -     val D0 = cterm_of (ProofContext.theory_of ctxt) D
   33.83 -     fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th' 
   33.84 -                 in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
   33.85 -                 end
   33.86 - in case get_first h al of
   33.87 -      SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
   33.88 -    | NONE => error "Transfer: corresponding instance not found in context-data"
   33.89 - end
   33.90 -in fun transfer_rule (a,D) leave (gctxt,th) = 
   33.91 -   (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
   33.92 -end;
   33.93 -
   33.94 -fun  splits P [] = []
   33.95 -   | splits P (xxs as (x::xs)) = 
   33.96 -    let val pss = filter (P x) xxs
   33.97 -        val qss = filter_out (P x) xxs
   33.98 -    in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
   33.99 -    end
  33.100 -
  33.101 -fun all_transfers leave (gctxt,th) = 
  33.102 - let 
  33.103 -  val ctxt = Context.proof_of gctxt
  33.104 -  val tys = map snd (Term.add_vars (prop_of th) [])
  33.105 -  val _ = if null tys then error "transfer: Unable to guess instance" else ()
  33.106 -  val tyss = splits (curry Type.could_unify) tys 
  33.107 -  val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
  33.108 -  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
  33.109 -  val insts = 
  33.110 -    map_filter (fn tys => 
  33.111 -          get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k)) 
  33.112 -                                  then SOME (get_aD k, ss) 
  33.113 -                                  else NONE) (snd (get ctxt))) tyss
  33.114 -  val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
  33.115 -  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
  33.116 -  val cth = Conjunction.intr_balanced ths
  33.117 - in (gctxt, cth)
  33.118 - end;
  33.119 -
  33.120 -fun transfer_rule_by_hint ls leave (gctxt,th) = 
  33.121 - let 
  33.122 -  val ctxt = Context.proof_of gctxt
  33.123 -  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
  33.124 -  val insts = 
  33.125 -    map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls 
  33.126 -			    then SOME (get_aD k, e) else NONE)
  33.127 -        (snd (get ctxt))
  33.128 -  val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
  33.129 -  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
  33.130 -  val cth = Conjunction.intr_balanced ths
  33.131 - in (gctxt, cth)
  33.132 - end;
  33.133 -
  33.134 -
  33.135 -fun transferred_attribute ls NONE leave = 
  33.136 -         if null ls then all_transfers leave else transfer_rule_by_hint ls leave
  33.137 -  | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
  33.138 -
  33.139 -                                                    (* Add data to the context *)
  33.140 -fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
  33.141 -                      ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
  33.142 -                       {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
  33.143 - = 
  33.144 - let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
  33.145 - {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2, 
  33.146 -  ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
  33.147 -  hints = subtract (op = : string*string -> bool) hints0 
  33.148 -            (hints1 union_string hints2)}
  33.149 - end;
  33.150 -
  33.151 -local
  33.152 - val h = curry (merge Thm.eq_thm)
  33.153 -in
  33.154 -fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
  33.155 -                   {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) = 
  33.156 -    {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
  33.157 -end; 
  33.158 -
  33.159 -fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
  33.160 -  Thm.declaration_attribute (fn key => fn context => context |> Data.map
  33.161 -   (fn (ss, al) => 
  33.162 -     let
  33.163 -      val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key) 
  33.164 -                in 0 end) 
  33.165 -                handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
  33.166 -      val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
  33.167 -      val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
  33.168 -      val entry = 
  33.169 -        if g then 
  33.170 -         let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
  33.171 -             val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
  33.172 -             val inj' = if null inja then #inj (case AList.lookup eq_key al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual") 
  33.173 -                        else inja
  33.174 -             val ret' = merge Thm.eq_thm (reta,  map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
  33.175 -         in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end 
  33.176 -        else e0
  33.177 -    in (ss, merge_update eq_key (gen_merge_entries ed) (key, entry) al)
  33.178 -    end));
  33.179 -
  33.180 -
  33.181 -
  33.182 -(* concrete syntax *)
  33.183 -
  33.184 -local
  33.185 -
  33.186 -fun keyword k = Scan.lift (Args.$$$ k) >> K ()
  33.187 -fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
  33.188 -
  33.189 -val congN = "cong"
  33.190 -val injN = "inj"
  33.191 -val embedN = "embed"
  33.192 -val returnN = "return"
  33.193 -val addN = "add"
  33.194 -val delN = "del"
  33.195 -val modeN = "mode"
  33.196 -val automaticN = "automatic"
  33.197 -val manualN = "manual"
  33.198 -val directionN = "direction"
  33.199 -val labelsN = "labels"
  33.200 -val leavingN = "leaving"
  33.201 -
  33.202 -val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
  33.203 -
  33.204 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
  33.205 -val terms = thms >> map Drule.dest_term
  33.206 -val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd) 
  33.207 -val name = Scan.lift Args.name
  33.208 -val names = Scan.repeat (Scan.unless any_keyword name)
  33.209 -fun optional scan = Scan.optional scan []
  33.210 -fun optional2 scan = Scan.optional scan ([],[])
  33.211 -
  33.212 -val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
  33.213 -val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
  33.214 -val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
  33.215 -val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
  33.216 -val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
  33.217 -val addscan = Scan.unless any_keyword (keyword addN)
  33.218 -val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
  33.219 -val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
  33.220 -
  33.221 -val transf_add = addscan |-- entry
  33.222 -in
  33.223 -
  33.224 -val install_att_syntax =
  33.225 -  (Scan.lift (Args.$$$ delN >> K del) ||
  33.226 -    transf_add
  33.227 -    >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
  33.228 -
  33.229 -val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
  33.230 -  -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
  33.231 -
  33.232 -end;
  33.233 -
  33.234 -
  33.235 -(* theory setup *)
  33.236 -
  33.237 -
  33.238 -val setup =
  33.239 -  Attrib.setup @{binding transfer} install_att_syntax
  33.240 -    "Installs transfer data" #>
  33.241 -  Attrib.setup @{binding transfer_simps} (Attrib.add_del add_ss del_ss)
  33.242 -    "simp rules for transfer" #>
  33.243 -  Attrib.setup @{binding transferred} transferred_att_syntax
  33.244 -    "Transfers theorems";
  33.245 -
  33.246 -end;
    34.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Sep 11 20:58:29 2009 +1000
    34.2 +++ b/src/HOL/UNITY/Transformers.thy	Thu Sep 17 14:17:37 2009 +1000
    34.3 @@ -88,7 +88,7 @@
    34.4  done
    34.5  
    34.6  lemma wens_Id [simp]: "wens F Id B = B"
    34.7 -by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
    34.8 +by (simp add: wens_def gfp_def wp_def awp_def, blast)
    34.9  
   34.10  text{*These two theorems justify the claim that @{term wens} returns the
   34.11  weakest assertion satisfying the ensures property*}
   34.12 @@ -101,7 +101,7 @@
   34.13  
   34.14  lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
   34.15  by (simp add: wens_def gfp_def constrains_def awp_def wp_def
   34.16 -              ensures_def transient_def Sup_set_eq, blast)
   34.17 +              ensures_def transient_def, blast)
   34.18  
   34.19  text{*These two results constitute assertion (4.13) of the thesis*}
   34.20  lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
   34.21 @@ -110,7 +110,7 @@
   34.22  done
   34.23  
   34.24  lemma wens_weakening: "B \<subseteq> wens F act B"
   34.25 -by (simp add: wens_def gfp_def Sup_set_eq, blast)
   34.26 +by (simp add: wens_def gfp_def, blast)
   34.27  
   34.28  text{*Assertion (6), or 4.16 in the thesis*}
   34.29  lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
   34.30 @@ -120,7 +120,7 @@
   34.31  
   34.32  text{*Assertion 4.17 in the thesis*}
   34.33  lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
   34.34 -by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
   34.35 +by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
   34.36    --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
   34.37        is declared as an iff-rule, then it's almost impossible to prove. 
   34.38        One proof is via @{text meson} after expanding all definitions, but it's
   34.39 @@ -331,7 +331,7 @@
   34.40  
   34.41  lemma wens_single_eq:
   34.42       "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
   34.43 -by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
   34.44 +by (simp add: wens_def gfp_def wp_def, blast)
   34.45  
   34.46  
   34.47  text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
    35.1 --- a/src/HOL/ex/CTL.thy	Fri Sep 11 20:58:29 2009 +1000
    35.2 +++ b/src/HOL/ex/CTL.thy	Thu Sep 17 14:17:37 2009 +1000
    35.3 @@ -95,7 +95,7 @@
    35.4      proof
    35.5        assume "x \<in> gfp (\<lambda>s. - f (- s))"
    35.6        then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
    35.7 -	by (auto simp add: gfp_def Sup_set_eq)
    35.8 +        by (auto simp add: gfp_def)
    35.9        then have "f (- u) \<subseteq> - u" by auto
   35.10        then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
   35.11        from l and this have "x \<notin> u" by auto
    36.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Fri Sep 11 20:58:29 2009 +1000
    36.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Sep 17 14:17:37 2009 +1000
    36.3 @@ -157,4 +157,13 @@
    36.4  values 3 "{(a,q). step (par nil nil) a q}"
    36.5  *)
    36.6  
    36.7 +
    36.8 +inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
    36.9 +    "k < l \<Longrightarrow> divmod_rel k l 0 k"
   36.10 +  | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
   36.11 +
   36.12 +code_pred divmod_rel ..
   36.13 +
   36.14 +value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)"
   36.15 +
   36.16  end
   36.17 \ No newline at end of file
    37.1 --- a/src/HOL/ex/ROOT.ML	Fri Sep 11 20:58:29 2009 +1000
    37.2 +++ b/src/HOL/ex/ROOT.ML	Thu Sep 17 14:17:37 2009 +1000
    37.3 @@ -60,6 +60,7 @@
    37.4    "BinEx",
    37.5    "Sqrt",
    37.6    "Sqrt_Script",
    37.7 +  "Transfer_Ex",
    37.8    "Arithmetic_Series_Complex",
    37.9    "HarmonicSeries",
   37.10    "Refute_Examples",
    38.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    38.2 +++ b/src/HOL/ex/Transfer_Ex.thy	Thu Sep 17 14:17:37 2009 +1000
    38.3 @@ -0,0 +1,42 @@
    38.4 +
    38.5 +header {* Various examples for transfer procedure *}
    38.6 +
    38.7 +theory Transfer_Ex
    38.8 +imports Complex_Main
    38.9 +begin
   38.10 +
   38.11 +(* nat to int *)
   38.12 +
   38.13 +lemma ex1: "(x::nat) + y = y + x"
   38.14 +  by auto
   38.15 +
   38.16 +thm ex1 [transferred]
   38.17 +
   38.18 +lemma ex2: "(a::nat) div b * b + a mod b = a"
   38.19 +  by (rule mod_div_equality)
   38.20 +
   38.21 +thm ex2 [transferred]
   38.22 +
   38.23 +lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
   38.24 +  by auto
   38.25 +
   38.26 +thm ex3 [transferred natint]
   38.27 +
   38.28 +lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
   38.29 +  by auto
   38.30 +
   38.31 +thm ex4 [transferred]
   38.32 +
   38.33 +lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
   38.34 +  by (induct n rule: nat_induct, auto)
   38.35 +
   38.36 +thm ex5 [transferred]
   38.37 +
   38.38 +theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
   38.39 +  by (rule ex5 [transferred])
   38.40 +
   38.41 +thm ex6 [transferred]
   38.42 +
   38.43 +thm ex5 [transferred, transferred]
   38.44 +
   38.45 +end
   38.46 \ No newline at end of file
    39.1 --- a/src/Pure/Concurrent/future.ML	Fri Sep 11 20:58:29 2009 +1000
    39.2 +++ b/src/Pure/Concurrent/future.ML	Thu Sep 17 14:17:37 2009 +1000
    39.3 @@ -84,7 +84,7 @@
    39.4  fun group_of (Future {group, ...}) = group;
    39.5  fun result_of (Future {result, ...}) = result;
    39.6  
    39.7 -fun peek x = Synchronized.peek (result_of x);
    39.8 +fun peek x = Synchronized.value (result_of x);
    39.9  fun is_finished x = is_some (peek x);
   39.10  
   39.11  fun value x = Future
    40.1 --- a/src/Pure/Concurrent/synchronized.ML	Fri Sep 11 20:58:29 2009 +1000
    40.2 +++ b/src/Pure/Concurrent/synchronized.ML	Thu Sep 17 14:17:37 2009 +1000
    40.3 @@ -8,7 +8,6 @@
    40.4  sig
    40.5    type 'a var
    40.6    val var: string -> 'a -> 'a var
    40.7 -  val peek: 'a var -> 'a
    40.8    val value: 'a var -> 'a
    40.9    val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
   40.10    val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
   40.11 @@ -33,9 +32,7 @@
   40.12    cond = ConditionVar.conditionVar (),
   40.13    var = ref x};
   40.14  
   40.15 -fun peek (Var {var, ...}) = ! var;  (*unsynchronized!*)
   40.16 -
   40.17 -fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);
   40.18 +fun value (Var {var, ...}) = ! var;
   40.19  
   40.20  
   40.21  (* synchronized access *)
    41.1 --- a/src/Pure/General/binding.ML	Fri Sep 11 20:58:29 2009 +1000
    41.2 +++ b/src/Pure/General/binding.ML	Thu Sep 17 14:17:37 2009 +1000
    41.3 @@ -30,18 +30,19 @@
    41.4    val str_of: binding -> string
    41.5  end;
    41.6  
    41.7 -structure Binding:> BINDING =
    41.8 +structure Binding: BINDING =
    41.9  struct
   41.10  
   41.11  (** representation **)
   41.12  
   41.13  (* datatype *)
   41.14  
   41.15 -datatype binding = Binding of
   41.16 +abstype binding = Binding of
   41.17   {prefix: (string * bool) list,     (*system prefix*)
   41.18    qualifier: (string * bool) list,  (*user qualifier*)
   41.19    name: bstring,                    (*base name*)
   41.20 -  pos: Position.T};                 (*source position*)
   41.21 +  pos: Position.T}                  (*source position*)
   41.22 +with
   41.23  
   41.24  fun make_binding (prefix, qualifier, name, pos) =
   41.25    Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
   41.26 @@ -109,6 +110,7 @@
   41.27    in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
   41.28  
   41.29  end;
   41.30 +end;
   41.31  
   41.32  type binding = Binding.binding;
   41.33  
    42.1 --- a/src/Pure/General/linear_set.scala	Fri Sep 11 20:58:29 2009 +1000
    42.2 +++ b/src/Pure/General/linear_set.scala	Thu Sep 17 14:17:37 2009 +1000
    42.3 @@ -1,22 +1,22 @@
    42.4  /*  Title:      Pure/General/linear_set.scala
    42.5      Author:     Makarius
    42.6 -    Author:     Fabian Immler TU Munich
    42.7 +    Author:     Fabian Immler, TU Munich
    42.8  
    42.9  Sets with canonical linear order, or immutable linked-lists.
   42.10  */
   42.11 +
   42.12  package isabelle
   42.13  
   42.14  
   42.15  object Linear_Set
   42.16  {
   42.17    private case class Rep[A](
   42.18 -    val first_elem: Option[A], val last_elem: Option[A], val body: Map[A, A])
   42.19 -
   42.20 -  private def empty_rep[A] = Rep[A](None, None, Map())
   42.21 +    val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
   42.22  
   42.23 -  private def make[A](first_elem: Option[A], last_elem: Option[A], body: Map[A, A]): Linear_Set[A] =
   42.24 -    new Linear_Set[A] { override val rep = Rep(first_elem, last_elem, body) }
   42.25 +  private def empty_rep[A] = Rep[A](None, None, Map(), Map())
   42.26  
   42.27 +  private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A])
   42.28 +    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) }
   42.29  
   42.30    def empty[A]: Linear_Set[A] = new Linear_Set
   42.31    def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
   42.32 @@ -35,48 +35,74 @@
   42.33  
   42.34    /* auxiliary operations */
   42.35  
   42.36 -  def next(elem: A) = rep.body.get(elem)
   42.37 -  def prev(elem: A) = rep.body.find(_._2 == elem).map(_._1)   // slow
   42.38 +  def next(elem: A): Option[A] = rep.nexts.get(elem)
   42.39 +  def prev(elem: A): Option[A] = rep.prevs.get(elem)
   42.40  
   42.41 -  private def _insert_after(hook: Option[A], elem: A): Linear_Set[A] =
   42.42 +  def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
   42.43      if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
   42.44 -    else hook match {
   42.45 -      case Some(hook) =>
   42.46 -        if (!contains(hook)) throw new Linear_Set.Undefined(hook.toString)
   42.47 -        else if (rep.body.isDefinedAt(hook))
   42.48 -          Linear_Set.make(rep.first_elem, rep.last_elem,
   42.49 -            rep.body - hook + (hook -> elem) + (elem -> rep.body(hook)))
   42.50 -        else Linear_Set.make(rep.first_elem, Some(elem), rep.body + (hook -> elem))
   42.51 +    else
   42.52 +      hook match {
   42.53 +        case None =>
   42.54 +          rep.first match {
   42.55 +            case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
   42.56 +            case Some(elem1) =>
   42.57 +              Linear_Set.make(Some(elem), rep.last,
   42.58 +                rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
   42.59 +          }
   42.60 +        case Some(elem1) =>
   42.61 +          if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
   42.62 +          else
   42.63 +            rep.nexts.get(elem1) match {
   42.64 +              case None =>
   42.65 +                Linear_Set.make(rep.first, Some(elem),
   42.66 +                  rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
   42.67 +              case Some(elem2) =>
   42.68 +                Linear_Set.make(rep.first, rep.last,
   42.69 +                  rep.nexts + (elem1 -> elem) + (elem -> elem2),
   42.70 +                  rep.prevs + (elem2 -> elem) + (elem -> elem1))
   42.71 +            }
   42.72 +      }
   42.73 +
   42.74 +  def delete_after(hook: Option[A]): Linear_Set[A] =
   42.75 +    hook match {
   42.76        case None =>
   42.77 -        if (isEmpty) Linear_Set.make(Some(elem), Some(elem), Map())
   42.78 -        else Linear_Set.make(Some(elem), rep.last_elem, rep.body + (elem -> rep.first_elem.get))
   42.79 +        rep.first match {
   42.80 +          case None => throw new Linear_Set.Undefined("")
   42.81 +          case Some(elem1) =>
   42.82 +            rep.nexts.get(elem1) match {
   42.83 +              case None => empty
   42.84 +              case Some(elem2) =>
   42.85 +                Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2)
   42.86 +            }
   42.87 +        }
   42.88 +      case Some(elem1) =>
   42.89 +        if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
   42.90 +        else
   42.91 +          rep.nexts.get(elem1) match {
   42.92 +            case None => throw new Linear_Set.Undefined("")
   42.93 +            case Some(elem2) =>
   42.94 +              rep.nexts.get(elem2) match {
   42.95 +                case None =>
   42.96 +                  Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
   42.97 +                case Some(elem3) =>
   42.98 +                  Linear_Set.make(rep.first, rep.last,
   42.99 +                    rep.nexts - elem2 + (elem1 -> elem3),
  42.100 +                    rep.prevs - elem2 + (elem3 -> elem1))
  42.101 +              }
  42.102 +          }
  42.103      }
  42.104  
  42.105 -  def insert_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
  42.106 -    elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
  42.107 +  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
  42.108 +    (elems :\ this)((elem, set) => set.insert_after(hook, elem))
  42.109  
  42.110 -  def delete_after(elem: Option[A]): Linear_Set[A] =
  42.111 -    elem match {
  42.112 -      case Some(elem) =>
  42.113 -        if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
  42.114 -        else if (!rep.body.isDefinedAt(elem)) throw new Linear_Set.Undefined(null)
  42.115 -        else if (rep.body(elem) == rep.last_elem.get)
  42.116 -          Linear_Set.make(rep.first_elem, Some(elem), rep.body - elem)
  42.117 -        else Linear_Set.make(rep.first_elem, rep.last_elem,
  42.118 -          rep.body - elem - rep.body(elem) + (elem -> rep.body(rep.body(elem))))
  42.119 -      case None =>
  42.120 -        if (isEmpty) throw new Linear_Set.Undefined(null)
  42.121 -        else if (size == 1) empty
  42.122 -        else Linear_Set.make(Some(rep.body(rep.first_elem.get)), rep.last_elem, rep.body - rep.first_elem.get)
  42.123 -    }
  42.124 -
  42.125 -  def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] = {
  42.126 -    if(!rep.first_elem.isDefined) this
  42.127 +  def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
  42.128 +  {
  42.129 +    if (isEmpty) this
  42.130      else {
  42.131        val next =
  42.132 -        if (from == rep.last_elem) None
  42.133 -        else if (from == None) rep.first_elem
  42.134 -        else from.map(rep.body(_))
  42.135 +        if (from == rep.last) None
  42.136 +        else if (from == None) rep.first
  42.137 +        else from.map(rep.nexts(_))
  42.138        if (next == to) this
  42.139        else delete_after(from).delete_between(from, to)
  42.140      }
  42.141 @@ -89,23 +115,23 @@
  42.142  
  42.143    def empty[B]: Linear_Set[B] = Linear_Set.empty
  42.144  
  42.145 -  override def isEmpty: Boolean = !rep.last_elem.isDefined
  42.146 -  def size: Int = if (isEmpty) 0 else rep.body.size + 1
  42.147 +  override def isEmpty: Boolean = !rep.first.isDefined
  42.148 +  def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
  42.149  
  42.150    def elements = new Iterator[A] {
  42.151 -    private var next_elem = rep.first_elem
  42.152 +    private var next_elem = rep.first
  42.153      def hasNext = next_elem.isDefined
  42.154      def next = {
  42.155        val elem = next_elem.get
  42.156 -      next_elem = if (rep.body.isDefinedAt(elem)) Some(rep.body(elem)) else None
  42.157 +      next_elem = rep.nexts.get(elem)
  42.158        elem
  42.159      }
  42.160    }
  42.161  
  42.162    def contains(elem: A): Boolean =
  42.163 -    !isEmpty && (rep.last_elem.get == elem || rep.body.isDefinedAt(elem))
  42.164 +    !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
  42.165  
  42.166 -  def + (elem: A): Linear_Set[A] = _insert_after(rep.last_elem, elem)
  42.167 +  def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
  42.168  
  42.169    override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
  42.170      this + elem1 + elem2 ++ elems
    43.1 --- a/src/Pure/General/position.ML	Fri Sep 11 20:58:29 2009 +1000
    43.2 +++ b/src/Pure/General/position.ML	Thu Sep 17 14:17:37 2009 +1000
    43.3 @@ -21,6 +21,7 @@
    43.4    val line: int -> T
    43.5    val line_file: int -> string -> T
    43.6    val id: string -> T
    43.7 +  val id_only: string -> T
    43.8    val get_id: T -> string option
    43.9    val put_id: string -> T -> T
   43.10    val of_properties: Properties.T -> T
   43.11 @@ -97,8 +98,8 @@
   43.12  fun line_file i name = Pos ((i, 0, 0), file_name name);
   43.13  fun line i = line_file i "";
   43.14  
   43.15 -
   43.16  fun id id = Pos ((0, 0, 1), [(Markup.idN, id)]);
   43.17 +fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
   43.18  
   43.19  fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
   43.20  fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
    44.1 --- a/src/Pure/Isar/isar_document.ML	Fri Sep 11 20:58:29 2009 +1000
    44.2 +++ b/src/Pure/Isar/isar_document.ML	Thu Sep 17 14:17:37 2009 +1000
    44.3 @@ -278,6 +278,7 @@
    44.4  val _ =
    44.5    OuterSyntax.internal_command "Isar.define_command"
    44.6      (P.string -- P.string >> (fn (id, text) =>
    44.7 +      Toplevel.position (Position.id_only id) o
    44.8        Toplevel.imperative (fn () =>
    44.9          define_command id (OuterSyntax.prepare_command (Position.id id) text))));
   44.10  
    45.1 --- a/src/Pure/ML-Systems/proper_int.ML	Fri Sep 11 20:58:29 2009 +1000
    45.2 +++ b/src/Pure/ML-Systems/proper_int.ML	Thu Sep 17 14:17:37 2009 +1000
    45.3 @@ -136,6 +136,24 @@
    45.4  end;
    45.5  
    45.6  
    45.7 +(* StringCvt *)
    45.8 +
    45.9 +structure StringCvt =
   45.10 +struct
   45.11 +  open StringCvt;
   45.12 +  datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option
   45.13 +  fun realfmt fmt = Real.fmt
   45.14 +    (case fmt of
   45.15 +      EXACT => StringCvt.EXACT
   45.16 +    | FIX NONE => StringCvt.FIX NONE
   45.17 +    | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
   45.18 +    | GEN NONE => StringCvt.GEN NONE
   45.19 +    | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
   45.20 +    | SCI NONE => StringCvt.SCI NONE
   45.21 +    | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
   45.22 +end;
   45.23 +
   45.24 +
   45.25  (* Word *)
   45.26  
   45.27  structure Word =
   45.28 @@ -165,6 +183,7 @@
   45.29    val trunc = mk_int o Real.trunc;
   45.30    fun toInt a b = mk_int (Real.toInt a b);
   45.31    fun fromInt a = Real.fromInt (dest_int a);
   45.32 +  val fmt = StringCvt.realfmt;
   45.33  end;
   45.34  
   45.35  val ceil = Real.ceil;
    46.1 --- a/src/Pure/thm.ML	Fri Sep 11 20:58:29 2009 +1000
    46.2 +++ b/src/Pure/thm.ML	Thu Sep 17 14:17:37 2009 +1000
    46.3 @@ -153,7 +153,7 @@
    46.4    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
    46.5  end;
    46.6  
    46.7 -structure Thm:> THM =
    46.8 +structure Thm: THM =
    46.9  struct
   46.10  
   46.11  structure Pt = Proofterm;
   46.12 @@ -163,11 +163,12 @@
   46.13  
   46.14  (** certified types **)
   46.15  
   46.16 -datatype ctyp = Ctyp of
   46.17 +abstype ctyp = Ctyp of
   46.18   {thy_ref: theory_ref,
   46.19    T: typ,
   46.20    maxidx: int,
   46.21 -  sorts: sort OrdList.T};
   46.22 +  sorts: sort OrdList.T}
   46.23 +with
   46.24  
   46.25  fun rep_ctyp (Ctyp args) = args;
   46.26  fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
   46.27 @@ -189,12 +190,13 @@
   46.28  (** certified terms **)
   46.29  
   46.30  (*certified terms with checked typ, maxidx, and sorts*)
   46.31 -datatype cterm = Cterm of
   46.32 +abstype cterm = Cterm of
   46.33   {thy_ref: theory_ref,
   46.34    t: term,
   46.35    T: typ,
   46.36    maxidx: int,
   46.37 -  sorts: sort OrdList.T};
   46.38 +  sorts: sort OrdList.T}
   46.39 +with
   46.40  
   46.41  exception CTERM of string * cterm list;
   46.42  
   46.43 @@ -337,7 +339,7 @@
   46.44  
   46.45  (*** Derivations and Theorems ***)
   46.46  
   46.47 -datatype thm = Thm of
   46.48 +abstype thm = Thm of
   46.49   deriv *                                        (*derivation*)
   46.50   {thy_ref: theory_ref,                          (*dynamic reference to theory*)
   46.51    tags: Properties.T,                           (*additional annotations/comments*)
   46.52 @@ -348,7 +350,8 @@
   46.53    prop: term}                                   (*conclusion*)
   46.54  and deriv = Deriv of
   46.55   {promises: (serial * thm future) OrdList.T,
   46.56 -  body: Pt.proof_body};
   46.57 +  body: Pt.proof_body}
   46.58 +with
   46.59  
   46.60  type conv = cterm -> thm;
   46.61  
   46.62 @@ -1718,6 +1721,10 @@
   46.63        end
   46.64    end;
   46.65  
   46.66 +end;
   46.67 +end;
   46.68 +end;
   46.69 +
   46.70  
   46.71  (* authentic derivation names *)
   46.72