--- a/Admin/PLATFORMS Fri Jan 07 23:30:29 2011 +0100
+++ b/Admin/PLATFORMS Fri Jan 07 23:46:06 2011 +0100
@@ -61,13 +61,13 @@
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
the platform, even on 64 bit hardware. Power-tools need to indicate
64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
-setting. The following bash expressions prefers the 64 bit platform,
+setting. The following bash expression prefers the 64 bit platform,
if that is available:
"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
Note that ML and JVM may have a different idea of the platform,
-depending the the respective binaries that are actually run.
+depending on the respective binaries that are actually run.
Dependable system tools
--- a/src/HOL/Decision_Procs/MIR.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Jan 07 23:46:06 2011 +0100
@@ -3585,9 +3585,9 @@
thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
by (auto simp add: split_def)
qed
- have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
- by (auto simp add: foldl_conv_concat)
- also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by auto
+ have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
+ by (auto simp add: foldl_conv_concat simp del: iupt.simps)
+ also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
@@ -3743,8 +3743,8 @@
by (auto simp add: split_def)
qed
- have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat)
- also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by auto
+ have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat simp del: iupt.simps)
+ also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
--- a/src/HOL/IsaMakefile Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/IsaMakefile Fri Jan 07 23:46:06 2011 +0100
@@ -300,6 +300,7 @@
Tools/int_arith.ML \
Tools/groebner.ML \
Tools/list_code.ML \
+ Tools/list_to_set_comprehension.ML \
Tools/nat_numeral_simprocs.ML \
Tools/Nitpick/kodkod.ML \
Tools/Nitpick/kodkod_sat.ML \
@@ -1040,7 +1041,8 @@
ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \
ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
- ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
+ ex/Intuitionistic.thy ex/Lagrange.thy \
+ ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy ex/MT.thy \
ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
--- a/src/HOL/List.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/List.thy Fri Jan 07 23:46:06 2011 +0100
@@ -6,7 +6,9 @@
theory List
imports Plain Presburger Recdef Code_Numeral Quotient ATP
-uses ("Tools/list_code.ML")
+uses
+ ("Tools/list_code.ML")
+ ("Tools/list_to_set_comprehension.ML")
begin
datatype 'a list =
@@ -339,13 +341,6 @@
mangled). In such cases it can be advisable to introduce separate
definitions for the list comprehensions in question. *}
-(*
-Proper theorem proving support would be nice. For example, if
-@{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
-produced something like
-@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
-*)
-
nonterminal lc_qual and lc_quals
syntax
@@ -450,6 +445,10 @@
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
*)
+use "Tools/list_to_set_comprehension.ML"
+
+simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
+
subsubsection {* @{const Nil} and @{const Cons} *}
@@ -965,7 +964,7 @@
by (induct xs) auto
lemma set_upt [simp]: "set[i..<j] = {i..<j}"
-by (induct j) (simp_all add: atLeastLessThanSuc)
+by (induct j) auto
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
@@ -1758,7 +1757,11 @@
lemma set_take_subset_set_take:
"m <= n \<Longrightarrow> set(take m xs) <= set(take n xs)"
-by(induct xs arbitrary: m n)(auto simp:take_Cons split:nat.split)
+apply (induct xs arbitrary: m n)
+apply simp
+apply (case_tac n)
+apply (auto simp: take_Cons)
+done
lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
@@ -2690,9 +2693,11 @@
by(simp add: upto.simps)
lemma set_upto[simp]: "set[i..j] = {i..j}"
-apply(induct i j rule:upto.induct)
-apply(simp add: upto.simps simp_from_to)
-done
+proof(induct i j rule:upto.induct)
+ case (1 i j)
+ from this show ?case
+ unfolding upto.simps[of i j] simp_from_to[of i j] by auto
+qed
subsubsection {* @{text "distinct"} and @{text remdups} *}
@@ -3366,7 +3371,7 @@
by(simp add:rotate_drop_take take_map drop_map)
lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
-by(simp add:rotate1_def split:list.split)
+by (cases xs) (auto simp add:rotate1_def)
lemma set_rotate[simp]: "set(rotate n xs) = set xs"
by (induct n) (simp_all add:rotate_def)
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Fri Jan 07 23:46:06 2011 +0100
@@ -89,14 +89,14 @@
apply clarsimp
apply (erule disjE)
apply (fastsimp dest: field_fields fields_is_type)
- apply (simp add: match_some_entry split: split_if_asm)
+ apply (simp add: match_some_entry image_iff)
apply (rule_tac x=1 in exI)
apply fastsimp
apply clarsimp
apply (erule disjE)
apply fastsimp
- apply (simp add: match_some_entry split: split_if_asm)
+ apply (simp add: match_some_entry image_iff)
apply (rule_tac x=1 in exI)
apply fastsimp
--- a/src/HOL/SMT.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/SMT.thy Fri Jan 07 23:46:06 2011 +0100
@@ -178,6 +178,11 @@
The option @{text smt_solver} can be used to change the target SMT
solver. The possible values can be obtained from the @{text smt_status}
command.
+
+Due to licensing restrictions, Yices and Z3 are not installed/enabled
+by default. Z3 is free for non-commercial applications and can be enabled
+by simply setting the environment variable @{text Z3_NON_COMMERCIAL} to
+@{text yes}.
*}
declare [[ smt_solver = cvc3 ]]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/list_to_set_comprehension.ML Fri Jan 07 23:46:06 2011 +0100
@@ -0,0 +1,206 @@
+(* Title: HOL/Tools/list_to_set_comprehension.ML
+ Author: Lukas Bulwahn, TU Muenchen
+
+ Simproc for rewriting list comprehensions applied to List.set to set comprehension
+*)
+
+signature LIST_TO_SET_COMPREHENSION =
+sig
+ val simproc : simpset -> cterm -> thm option
+end;
+
+structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
+struct
+
+fun CONVERSION' cv i st = Seq.single (Conv.gconv_rule cv i st)
+
+(* conversion *)
+
+fun trace_conv cv ct =
+ (tracing (Syntax.string_of_term_global @{theory} (Thm.term_of ct)); cv ct)
+
+fun all_exists_conv cv ctxt ct =
+ case Thm.term_of ct of
+ Const(@{const_name HOL.Ex}, _) $ Abs(_, _, _) =>
+ Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
+ | _ => cv ctxt ct
+
+fun all_but_last_exists_conv cv ctxt ct =
+ case Thm.term_of ct of
+ Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
+ Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
+ | _ => cv ctxt ct
+
+fun Collect_conv cv ctxt ct =
+ (case Thm.term_of ct of
+ Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
+ | _ => raise CTERM ("Collect_conv", [ct]));
+
+fun Trueprop_conv cv ct =
+ (case Thm.term_of ct of
+ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
+ | _ => raise CTERM ("Trueprop_conv", [ct]));
+
+fun eq_conv cv1 cv2 ct =
+ (case Thm.term_of ct of
+ Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
+ | _ => raise CTERM ("eq_conv", [ct]));
+
+fun conj_conv cv1 cv2 ct =
+ (case Thm.term_of ct of
+ Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
+ | _ => raise CTERM ("conj_conv", [ct]));
+
+fun right_hand_set_comprehension_conv conv ctxt = Trueprop_conv (eq_conv Conv.all_conv
+ (Collect_conv (all_exists_conv conv o #2) ctxt))
+
+(* term abstraction of list comprehension patterns *)
+
+datatype termlets = If | Case of (typ * int)
+
+val last = snd o split_last
+
+fun meta_eq th = th RS @{thm eq_reflection}
+
+fun rewr_conv' th = Conv.rewr_conv (meta_eq th)
+
+fun simproc ss redex =
+ let
+ val ctxt = Simplifier.the_context ss
+ val thy = ProofContext.theory_of ctxt
+ val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
+ val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
+ val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
+ val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
+ fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
+ fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
+ fun dest_singleton_list (Const (@{const_name List.Cons}, _)
+ $ t $ (Const (@{const_name List.Nil}, _))) = t
+ | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
+ (* We check that one case returns a singleton list and all other cases
+ return [], and return the index of the one singleton list case *)
+ fun possible_index_of_singleton_case cases =
+ let
+ fun check (i, case_t) s =
+ (case strip_abs_body case_t of
+ (Const (@{const_name List.Nil}, _)) => s
+ | t => (case s of NONE => SOME i | SOME s => NONE))
+ in
+ fold_index check cases NONE
+ end
+ (* returns (case_expr type index chosen_case) option *)
+ fun dest_case case_term =
+ let
+ val (case_const, args) = strip_comb case_term
+ in
+ case try dest_Const case_const of
+ SOME (c, T) => (case Datatype_Data.info_of_case thy c of
+ SOME _ => (case possible_index_of_singleton_case (fst (split_last args)) of
+ SOME i =>
+ let
+ val (Ts, _) = strip_type T
+ val T' = last Ts
+ in SOME (snd (split_last args), T', i, nth args i) end
+ | NONE => NONE)
+ | NONE => NONE)
+ | NONE => NONE
+ end
+ (* returns condition continuing term option *)
+ fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
+ SOME (cond, then_t)
+ | dest_if _ = NONE
+ fun tac _ [] =
+ rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
+ | tac ctxt (If :: cont) =
+ Splitter.split_tac [@{thm split_if}] 1
+ THEN rtac @{thm conjI} 1
+ THEN rtac @{thm impI} 1
+ THEN Subgoal.FOCUS (fn {prems, context, ...} =>
+ CONVERSION (right_hand_set_comprehension_conv (K
+ (conj_conv (Conv.rewr_conv (snd (split_last prems) RS @{thm Eq_TrueI})) Conv.all_conv
+ then_conv rewr_conv' @{thm simp_thms(22)})) context) 1) ctxt 1
+ THEN tac ctxt cont
+ THEN rtac @{thm impI} 1
+ THEN Subgoal.FOCUS (fn {prems, context, ...} =>
+ CONVERSION (right_hand_set_comprehension_conv (K
+ (conj_conv (Conv.rewr_conv (snd (split_last prems) RS @{thm Eq_FalseI})) Conv.all_conv
+ then_conv rewr_conv' @{thm simp_thms(24)})) context) 1) ctxt 1
+ THEN rtac set_Nil_I 1
+ | tac ctxt (Case (T, i) :: cont) =
+ let
+ val info = Datatype.the_info thy (fst (dest_Type T))
+ in
+ (* do case distinction *)
+ Splitter.split_tac [#split info] 1
+ THEN EVERY (map_index (fn (i', case_rewrite) =>
+ (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
+ THEN REPEAT_DETERM (rtac @{thm allI} 1)
+ THEN rtac @{thm impI} 1
+ THEN (if i' = i then
+ (* continue recursively *)
+ Subgoal.FOCUS (fn {prems, context, ...} =>
+ CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
+ ((conj_conv
+ (eq_conv Conv.all_conv (rewr_conv' (snd (split_last prems)))
+ then_conv (Conv.try_conv (Conv.rewrs_conv (map meta_eq (#inject info))))) Conv.all_conv)
+ then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
+ then_conv (Conv.try_conv (rewr_conv' @{thm conj_assoc})))) context
+ then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
+ Conv.repeat_conv (all_but_last_exists_conv (K (rewr_conv' @{thm simp_thms(39)})) ctxt)) context)))) 1) ctxt 1
+ THEN tac ctxt cont
+ else
+ Subgoal.FOCUS (fn {prems, context, ...} =>
+ CONVERSION ((right_hand_set_comprehension_conv (K
+ (conj_conv
+ ((eq_conv Conv.all_conv
+ (rewr_conv' (snd (split_last prems))))
+ then_conv (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info)))) Conv.all_conv
+ then_conv (rewr_conv' @{thm simp_thms(24)}))) context)
+ then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
+ Conv.repeat_conv (Conv.bottom_conv (K (rewr_conv' @{thm simp_thms(36)})) ctxt)) context)))) 1) ctxt 1
+ THEN rtac set_Nil_I 1)) (#case_rewrites info))
+ end
+ fun make_inner_eqs bound_vs Tis eqs t =
+ case dest_case t of
+ SOME (x, T, i, cont) =>
+ let
+ val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
+ val x' = incr_boundvars (length vs) x
+ val eqs' = map (incr_boundvars (length vs)) eqs
+ val (constr_name, _) = nth (the (Datatype_Data.get_constrs thy (fst (dest_Type T)))) i
+ val constr_t = list_comb (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
+ val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
+ in
+ make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
+ end
+ | NONE =>
+ case dest_if t of
+ SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
+ | NONE =>
+ if eqs = [] then NONE (* no rewriting, nothing to be done *)
+ else
+ let
+ val Type ("List.list", [rT]) = fastype_of t
+ val pat_eq =
+ case try dest_singleton_list t of
+ SOME t' => Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool})
+ $ Bound (length bound_vs) $ t'
+ | NONE => Const ("Set.member", rT --> HOLogic.mk_setT rT --> @{typ bool})
+ $ Bound (length bound_vs) $ (mk_set rT $ t)
+ val reverse_bounds = curry subst_bounds
+ ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
+ val eqs' = map reverse_bounds eqs
+ val pat_eq' = reverse_bounds pat_eq
+ val inner_t = fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy (T, t))
+ (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
+ val lhs = term_of redex
+ val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
+ val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ in
+ SOME ((Goal.prove ctxt [] [] rewrite_rule_t (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
+ end
+ in
+ make_inner_eqs [] [] [] (dest_set (term_of redex))
+ end
+
+end
--- a/src/HOL/ex/CTL.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/CTL.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/CTL.thy
- ID: $Id$
Author: Gertrud Bauer
*)
--- a/src/HOL/ex/Guess.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/Guess.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(*
- ID: $Id$
Author: Makarius
*)
--- a/src/HOL/ex/Hex_Bin_Examples.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/Hex_Bin_Examples.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Hex_Bin_Examples.thy
- ID: $Id$
Author: Gerwin Klein, NICTA
*)
--- a/src/HOL/ex/Higher_Order_Logic.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Higher_Order_Logic.thy
- ID: $Id$
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
*)
--- a/src/HOL/ex/Intuitionistic.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/Intuitionistic.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Intuitionistic.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/List_to_Set_Comprehension_Examples.thy Fri Jan 07 23:46:06 2011 +0100
@@ -0,0 +1,84 @@
+(* Title: HOL/ex/List_to_Set_Comprehension_Examples.thy
+ Author: Lukas Bulwahn
+ Copyright 2011 TU Muenchen
+*)
+
+header {* Examples for the list comprehension to set comprehension simproc *}
+
+theory List_to_Set_Comprehension_Examples
+imports Main
+begin
+
+text {*
+Examples that show and test the simproc that rewrites list comprehensions
+applied to List.set to set comprehensions.
+*}
+
+subsection {* Some own examples for set (case ..) simpproc *}
+
+lemma "set [(x, xs). x # xs <- as] = {(x, xs). x # xs \<in> set as}"
+by auto
+
+lemma "set [(x, y, ys). x # y # ys <- as] = {(x, y, ys). x # y # ys \<in> set as}"
+by auto
+
+lemma "set [(x, y, z, zs). x # y # z # zs <- as] = {(x, y, z, zs). x # y # z # zs \<in> set as}"
+by auto
+
+lemma "set [(zs, x, z, y). x # (y, z) # zs <- as] = {(zs, x, z, y). x # (y, z) # zs \<in> set as}"
+by auto
+
+lemma "set [(x, y). x # y <- zs, x = x'] = {(x, y). x # y \<in> set zs & x = x'}"
+by auto
+
+subsection {* Existing examples from the List theory *}
+
+lemma "set [(x,y,z). b] = {(x', y', z'). x = x' & y = y' & z = z' & b}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs] = {(x, y', z'). x \<in> set xs & y' = y & z = z'}"
+by auto
+
+lemma "set [e x y. x\<leftarrow>xs, y\<leftarrow>ys] = {z. \<exists> x y. z = e x y & x \<in> set xs & y \<in> set ys}"
+by auto
+
+lemma "set [(x,y,z). x<a, x>b] = {(x', y', z'). x' = x & y' = y & z = z' & x < a & x>b}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs, x>b] = {(x', y', z'). y = y' & z = z' & x' \<in> set xs & x' > b}"
+by auto
+
+lemma "set [(x,y,z). x<a, x\<leftarrow>xs] = {(x', y', z'). y = y' & z = z' & x' \<in> set xs & x < a}"
+by auto
+
+lemma "set [(x,y). Cons True x \<leftarrow> xs] = {(x, y'). y = y' & Cons True x \<in> set xs}"
+by auto
+
+lemma "set [(x,y,z). Cons x [] \<leftarrow> xs] = {(x, y', z'). y = y' & z = z' & Cons x [] \<in> set xs}"
+by auto
+
+lemma "set [(x,y,z). x<a, x>b, x=d] = {(x', y', z'). x = x' & y = y' & z = z' & x < a & x > b & x = d}"
+by auto
+
+lemma "set [(x,y,z). x<a, x>b, y\<leftarrow>ys] = {(x', y, z'). x = x' & y \<in> set ys & z = z' & x < a & x > b}"
+by auto
+
+lemma "set [(x,y,z). x<a, x\<leftarrow>xs,y>b] = {(x',y',z'). x' \<in> set xs & y = y' & z = z' & x < a & y > b}"
+by auto
+
+lemma "set [(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys] = {(x', y', z'). z = z' & x < a & x' \<in> set xs & y' \<in> set ys}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs, x>b, y<a] = {(x', y', z'). y = y' & z = z' & x' \<in> set xs & x' > b & y < a}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys] = {(x', y', z'). z = z' & x' \<in> set xs & x' > b & y' \<in> set ys}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x] = {(x', y', z'). z = z' & x' \<in> set xs & y' \<in> set ys & y' > x'}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs] = {(x', y', z'). x' \<in> set xs & y' \<in> set ys & z' \<in> set zs}"
+by auto
+
+end
--- a/src/HOL/ex/MT.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/MT.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/MT.thy
- ID: $Id$
Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
--- a/src/HOL/ex/MonoidGroup.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/MonoidGroup.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/MonoidGroup.thy
- ID: $Id$
Author: Markus Wenzel
*)
--- a/src/HOL/ex/Primrec.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/Primrec.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Primrec.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
--- a/src/HOL/ex/ROOT.ML Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/ROOT.ML Fri Jan 07 23:46:06 2011 +0100
@@ -71,7 +71,8 @@
"Gauge_Integration",
"Dedekind_Real",
"Quicksort",
- "Birthday_Paradoxon"
+ "Birthday_Paradoxon",
+ "List_to_Set_Comprehension_Examples"
];
use_thy "SVC_Oracle";
--- a/src/HOL/ex/SVC_Oracle.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/SVC_Oracle.thy
- ID: $Id$
Author: Lawrence C Paulson
Copyright 1999 University of Cambridge
--- a/src/HOL/ex/Sorting.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/Sorting.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/sorting.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 1994 TU Muenchen
*)
--- a/src/HOL/ex/Unification.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/Unification.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,4 +1,4 @@
-(* ID: $Id$
+(*
Author: Alexander Krauss, Technische Universitaet Muenchen
*)
--- a/src/HOL/ex/set.thy Fri Jan 07 23:30:29 2011 +0100
+++ b/src/HOL/ex/set.thy Fri Jan 07 23:46:06 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/set.thy
- ID: $Id$
Author: Tobias Nipkow and Lawrence C Paulson
Copyright 1991 University of Cambridge
*)