--- a/src/HOL/Hoare/Hoare_Logic.thy Fri Feb 21 19:20:26 2014 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy Fri Feb 21 21:27:55 2014 +0100
@@ -96,12 +96,12 @@
ML_file "hoare_tac.ML"
method_setup vcg = {*
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac))) *}
"verification condition generator"
method_setup vcg_simp = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac ctxt))) *}
+ SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt))) *}
"verification condition generator plus simplification"
end
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Fri Feb 21 19:20:26 2014 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Fri Feb 21 21:27:55 2014 +0100
@@ -107,12 +107,12 @@
ML_file "hoare_tac.ML"
method_setup vcg = {*
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac))) *}
"verification condition generator"
method_setup vcg_simp = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac ctxt))) *}
+ SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt))) *}
"verification condition generator plus simplification"
(* Special syntax for guarded statements and guarded array updates: *)
--- a/src/HOL/Hoare/hoare_syntax.ML Fri Feb 21 19:20:26 2014 +0100
+++ b/src/HOL/Hoare/hoare_syntax.ML Fri Feb 21 21:27:55 2014 +0100
@@ -42,7 +42,7 @@
(*all meta-variables for bexp except for TRUE are translated as if they
were boolean expressions*)
-fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *)
+fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE" (* FIXME !? *)
| bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
@@ -52,7 +52,7 @@
fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
- | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
+ | com_tr (Const (@{const_syntax Basic},_) $ f) _ = Syntax.const @{const_syntax Basic} $ f
| com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
| com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
@@ -88,27 +88,27 @@
| dest_abstuple tm = tm;
fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
- | abs2list (Abs (x, T, t)) = [Free (x, T)]
+ | abs2list (Abs (x, T, _)) = [Free (x, T)]
| abs2list _ = [];
-fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = mk_ts t
- | mk_ts (Abs (x, _, t)) = mk_ts t
+fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (_, _, t)) = mk_ts t
+ | mk_ts (Abs (_, _, t)) = mk_ts t
| mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
| mk_ts t = [t];
fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) =
(Syntax.free x :: abs2list t, mk_ts t)
| mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
- | mk_vts t = raise Match;
+ | mk_vts _ = raise Match;
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) (* FIXME no_ch!? *)
+fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) (* FIXME no_ch!? *)
| find_ch ((v, t) :: vts) i xs =
if t = Bound i then find_ch vts (i - 1) xs
else (true, (v, subst_bounds (xs, t)));
-fun is_f (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = true
- | is_f (Abs (x, _, t)) = true
- | is_f t = false;
+fun is_f (Const (@{const_syntax case_prod}, _) $ Abs _) = true
+ | is_f (Abs _) = true
+ | is_f _ = false;
(* assn_tr' & bexp_tr'*)
@@ -148,7 +148,7 @@
in
-fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q
+fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q;
end;
--- a/src/HOL/Hoare/hoare_tac.ML Fri Feb 21 19:20:26 2014 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Fri Feb 21 21:27:55 2014 +0100
@@ -4,7 +4,15 @@
Derivation of the proof rules and, most importantly, the VCG tactic.
*)
-(* FIXME structure Hoare: HOARE *)
+signature HOARE =
+sig
+ val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool ->
+ int -> tactic
+ val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic
+end;
+
+structure Hoare: HOARE =
+struct
(*** The tactics ***)
@@ -19,7 +27,7 @@
(** maps (%x1 ... xn. t) to [x1,...,xn] **)
fun abs2list (Const (@{const_name case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
- | abs2list (Abs (x, T, t)) = [Free (x, T)]
+ | abs2list (Abs (x, T, _)) = [Free (x, T)]
| abs2list _ = [];
(** maps {(x1,...,xn). t} to [x1,...,xn] **)
@@ -45,26 +53,30 @@
end;
(** maps [x1,...,xn] to (x1,...,xn) and types**)
-fun mk_bodyC [] = HOLogic.unit
- | mk_bodyC (x::xs) = if xs=[] then x
- else let val (n, T) = dest_Free x ;
- val z = mk_bodyC xs;
- val T2 = case z of Free(_, T) => T
- | Const (@{const_name Pair}, Type ("fun", [_, Type
- ("fun", [_, T])])) $ _ $ _ => T;
- in Const (@{const_name Pair}, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end;
+fun mk_bodyC [] = HOLogic.unit
+ | mk_bodyC [x] = x
+ | mk_bodyC (x :: xs) =
+ let
+ val (_, T) = dest_Free x;
+ val z = mk_bodyC xs;
+ val T2 =
+ (case z of
+ Free (_, T) => T
+ | Const (@{const_name Pair}, Type ("fun", [_, Type ("fun", [_, T])])) $ _ $ _ => T);
+ in Const (@{const_name Pair}, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end;
(** maps a subgoal of the form:
- VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)
+ VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]
+**)
fun get_vars c =
let
val d = Logic.strip_assums_concl c;
val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d;
in mk_vars pre end;
-fun mk_CollectC trm =
- let val T as Type ("fun",[t,_]) = fastype_of trm
- in HOLogic.Collect_const t $ trm end;
+fun mk_CollectC tm =
+ let val T as Type ("fun",[t,_]) = fastype_of tm;
+ in HOLogic.Collect_const t $ tm end;
fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> HOLogic.boolT);
@@ -76,8 +88,10 @@
val vars = get_vars prop;
val varsT = fastype_of (mk_bodyC vars);
- val big_Collect = mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) $ mk_bodyC vars));
- val small_Collect = mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) $ Bound 0));
+ val big_Collect =
+ mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) $ mk_bodyC vars));
+ val small_Collect =
+ mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) $ Bound 0));
val MsetT = fastype_of big_Collect;
fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
@@ -104,7 +118,7 @@
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]);
(*****************************************************************************)
-(** set2pred_tac transforms sets inclusion into predicates implication, **)
+(** set_to_pred_tac transforms sets inclusion into predicates implication, **)
(** maintaining the original variable names. **)
(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1" **)
(** Subgoals containing intersections (A Int B) or complement sets (-A) **)
@@ -115,7 +129,7 @@
(** simplification done by (split_all_tac) **)
(*****************************************************************************)
-fun set2pred_tac ctxt var_names = SUBGOAL (fn (goal, i) =>
+fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
before_set2pred_simp_tac ctxt i THEN_MAYBE
EVERY [
rtac subsetI i,
@@ -125,22 +139,22 @@
(rename_tac var_names i THEN
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
-(*****************************************************************************)
-(** BasicSimpTac is called to simplify all verification conditions. It does **)
-(** a light simplification by applying "mem_Collect_eq", then it calls **)
-(** MaxSimpTac, which solves subgoals of the form "A <= A", **)
-(** and transforms any other into predicates, applying then **)
-(** the tactic chosen by the user, which may solve the subgoal completely. **)
-(*****************************************************************************)
+(*******************************************************************************)
+(** basic_simp_tac is called to simplify all verification conditions. It does **)
+(** a light simplification by applying "mem_Collect_eq", then it calls **)
+(** max_simp_tac, which solves subgoals of the form "A <= A", **)
+(** and transforms any other into predicates, applying then **)
+(** the tactic chosen by the user, which may solve the subgoal completely. **)
+(*******************************************************************************)
-fun MaxSimpTac ctxt var_names tac =
- FIRST'[rtac subset_refl, set2pred_tac ctxt var_names THEN_MAYBE' tac];
+fun max_simp_tac ctxt var_names tac =
+ FIRST' [rtac subset_refl, set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
-fun BasicSimpTac ctxt var_names tac =
+fun basic_simp_tac ctxt var_names tac =
simp_tac
(put_simpset HOL_basic_ss ctxt
addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])
- THEN_MAYBE' MaxSimpTac ctxt var_names tac;
+ THEN_MAYBE' max_simp_tac ctxt var_names tac;
(** hoare_rule_tac **)
@@ -166,15 +180,17 @@
rule_tac false (i + 1)],
EVERY [
rtac @{thm WhileRule} i,
- BasicSimpTac ctxt var_names tac (i + 2),
+ basic_simp_tac ctxt var_names tac (i + 2),
rule_tac true (i + 1)]]
- THEN (if pre_cond then BasicSimpTac ctxt var_names tac i else rtac subset_refl i)));
+ THEN (if pre_cond then basic_simp_tac ctxt var_names tac i else rtac subset_refl i)));
in rule_tac end;
(** tac is the tactic the user chooses to solve or simplify **)
(** the final verification conditions **)
-fun hoare_tac ctxt (tac: int -> tactic) = SUBGOAL (fn (goal, i) =>
+fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) =>
SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
+end;
+
--- a/src/HOL/Isar_Examples/Hoare.thy Fri Feb 21 19:20:26 2014 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Fri Feb 21 21:27:55 2014 +0100
@@ -189,26 +189,24 @@
@{ML Syntax_Trans.quote_tr'},). *}
syntax
- "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(.'(_').)" [0] 1000)
- "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000)
- "_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
- ("_[_'/\<acute>_]" [1000] 999)
- "_Assert" :: "'a \<Rightarrow> 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
- "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61)
- "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
- ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
- "_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
- ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61)
- "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"
- ("(0WHILE _ //DO _ /OD)" [0, 0] 61)
+ "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"
+ "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000)
+ "_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp" ("_[_'/\<acute>_]" [1000] 999)
+ "_Assert" :: "'a \<Rightarrow> 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
+ "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61)
+ "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
+ ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
+ "_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
+ ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61)
+ "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0WHILE _ //DO _ /OD)" [0, 0] 61)
translations
- "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect .(b)."
- "B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
- "\<acute>x := a" \<rightharpoonup> "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
+ "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect (_quote b)"
+ "B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
+ "\<acute>x := a" \<rightharpoonup> "CONST Basic (_quote (\<acute>(_update_name x (\<lambda>_. a))))"
"IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
- "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
- "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
+ "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
+ "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
parse_translation {*
let
@@ -328,12 +326,10 @@
text {* While statements --- with optional invariant. *}
-lemma [intro?]:
- "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
+lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
by (rule while)
-lemma [intro?]:
- "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
+lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
by (rule while)
@@ -400,7 +396,7 @@
method_setup hoare = {*
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD'
- (hoare_tac ctxt
+ (Hoare.hoare_tac ctxt
(simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] ))))) *}
"verification condition generator for Hoare logic"
--- a/src/HOL/ROOT Fri Feb 21 19:20:26 2014 +0100
+++ b/src/HOL/ROOT Fri Feb 21 21:27:55 2014 +0100
@@ -570,7 +570,7 @@
Simproc_Tests
Executable_Relation
FinFunPred
- Set_Comprehension_Pointfree_Tests
+ Set_Comprehension_Pointfree_Examples
Parallel_Example
IArray_Examples
SVC_Oracle
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy Fri Feb 21 21:27:55 2014 +0100
@@ -0,0 +1,140 @@
+(* Title: HOL/ex/Set_Comprehension_Pointfree_Examples.thy
+ Author: Lukas Bulwahn, Rafal Kolanski
+ Copyright 2012 TU Muenchen
+*)
+
+header {* Examples for the set comprehension to pointfree simproc *}
+
+theory Set_Comprehension_Pointfree_Examples
+imports Main
+begin
+
+declare [[simproc add: finite_Collect]]
+
+lemma
+ "finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}"
+ by simp
+
+lemma
+ "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B}"
+ by simp
+
+lemma
+ "finite B ==> finite A' ==> finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
+ by simp
+
+lemma
+ "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
+ by simp
+
+lemma
+ "finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
+ by simp
+
+lemma
+ "finite A ==> finite B ==> finite C ==> finite D ==>
+ finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
+ by simp
+
+lemma
+ "finite A ==> finite B ==> finite C ==> finite D ==> finite E ==>
+ finite {f a b c d e | a b c d e. a : A \<and> b : B \<and> c : C \<and> d : D \<and> e : E}"
+ by simp
+
+lemma
+ "finite A ==> finite B ==> finite C ==> finite D ==> finite E \<Longrightarrow>
+ finite {f a d c b e | e b c d a. b : B \<and> a : A \<and> e : E' \<and> c : C \<and> d : D \<and> e : E \<and> b : B'}"
+ by simp
+
+lemma
+ "\<lbrakk> finite A ; finite B ; finite C ; finite D \<rbrakk>
+ \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
+ by simp
+
+lemma
+ "finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D))
+ \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
+ by simp
+
+lemma
+ "finite S ==> finite {s'. EX s:S. s' = f a e s}"
+ by simp
+
+lemma
+ "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> a \<notin> Z}"
+ by simp
+
+lemma
+ "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> b : B \<and> (x,y) \<in> R}"
+by simp
+
+lemma
+ "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> (x,y) \<in> R \<and> b : B}"
+by simp
+
+lemma
+ "finite A ==> finite B ==> finite R ==> finite {f a (x, b) y| y b x a. a : A \<and> (x,y) \<in> R \<and> b : B}"
+by simp
+
+lemma
+ "finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \<or> a : AA) \<and> b : B \<and> a \<notin> Z}"
+by simp
+
+lemma
+ "finite A1 ==> finite A2 ==> finite A3 ==> finite A4 ==> finite A5 ==> finite B ==>
+ finite {f a b c | a b c. ((a : A1 \<and> a : A2) \<or> (a : A3 \<and> (a : A4 \<or> a : A5))) \<and> b : B \<and> a \<notin> Z}"
+apply simp
+oops
+
+lemma "finite B ==> finite {c. EX x. x : B & c = a * x}"
+by simp
+
+lemma
+ "finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}"
+by simp
+
+lemma
+ "finite S ==> inj (%(x, y). g x y) ==> finite {f x y| x y. g x y : S}"
+ by (auto intro: finite_vimageI)
+
+lemma
+ "finite A ==> finite S ==> inj (%(x, y). g x y) ==> finite {f x y z | x y z. g x y : S & z : A}"
+ by (auto intro: finite_vimageI)
+
+lemma
+ "finite S ==> finite A ==> inj (%(x, y). g x y) ==> inj (%(x, y). h x y)
+ ==> finite {f a b c d | a b c d. g a c : S & h b d : A}"
+ by (auto intro: finite_vimageI)
+
+lemma
+ assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"
+using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
+ (* injectivity to be automated with further rules and automation *)
+
+schematic_lemma (* check interaction with schematics *)
+ "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
+ = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
+ by simp
+
+declare [[simproc del: finite_Collect]]
+
+
+section {* Testing simproc in code generation *}
+
+definition union :: "nat set => nat set => nat set"
+where
+ "union A B = {x. x : A \<or> x : B}"
+
+definition common_subsets :: "nat set => nat set => nat set set"
+where
+ "common_subsets S1 S2 = {S. S \<subseteq> S1 \<and> S \<subseteq> S2}"
+
+definition products :: "nat set => nat set => nat set"
+where
+ "products A B = {c. EX a b. a : A & b : B & c = a * b}"
+
+export_code products in Haskell
+
+export_code union common_subsets products in Haskell
+
+end
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Fri Feb 21 19:20:26 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,140 +0,0 @@
-(* Title: HOL/ex/Set_Comprehension_Pointfree_Tests.thy
- Author: Lukas Bulwahn, Rafal Kolanski
- Copyright 2012 TU Muenchen
-*)
-
-header {* Tests for the set comprehension to pointfree simproc *}
-
-theory Set_Comprehension_Pointfree_Tests
-imports Main
-begin
-
-declare [[simproc add: finite_Collect]]
-
-lemma
- "finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}"
- by simp
-
-lemma
- "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B}"
- by simp
-
-lemma
- "finite B ==> finite A' ==> finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
- by simp
-
-lemma
- "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
- by simp
-
-lemma
- "finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
- by simp
-
-lemma
- "finite A ==> finite B ==> finite C ==> finite D ==>
- finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
- by simp
-
-lemma
- "finite A ==> finite B ==> finite C ==> finite D ==> finite E ==>
- finite {f a b c d e | a b c d e. a : A \<and> b : B \<and> c : C \<and> d : D \<and> e : E}"
- by simp
-
-lemma
- "finite A ==> finite B ==> finite C ==> finite D ==> finite E \<Longrightarrow>
- finite {f a d c b e | e b c d a. b : B \<and> a : A \<and> e : E' \<and> c : C \<and> d : D \<and> e : E \<and> b : B'}"
- by simp
-
-lemma
- "\<lbrakk> finite A ; finite B ; finite C ; finite D \<rbrakk>
- \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
- by simp
-
-lemma
- "finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D))
- \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
- by simp
-
-lemma
- "finite S ==> finite {s'. EX s:S. s' = f a e s}"
- by simp
-
-lemma
- "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> a \<notin> Z}"
- by simp
-
-lemma
- "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> b : B \<and> (x,y) \<in> R}"
-by simp
-
-lemma
- "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> (x,y) \<in> R \<and> b : B}"
-by simp
-
-lemma
- "finite A ==> finite B ==> finite R ==> finite {f a (x, b) y| y b x a. a : A \<and> (x,y) \<in> R \<and> b : B}"
-by simp
-
-lemma
- "finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \<or> a : AA) \<and> b : B \<and> a \<notin> Z}"
-by simp
-
-lemma
- "finite A1 ==> finite A2 ==> finite A3 ==> finite A4 ==> finite A5 ==> finite B ==>
- finite {f a b c | a b c. ((a : A1 \<and> a : A2) \<or> (a : A3 \<and> (a : A4 \<or> a : A5))) \<and> b : B \<and> a \<notin> Z}"
-apply simp
-oops
-
-lemma "finite B ==> finite {c. EX x. x : B & c = a * x}"
-by simp
-
-lemma
- "finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}"
-by simp
-
-lemma
- "finite S ==> inj (%(x, y). g x y) ==> finite {f x y| x y. g x y : S}"
- by (auto intro: finite_vimageI)
-
-lemma
- "finite A ==> finite S ==> inj (%(x, y). g x y) ==> finite {f x y z | x y z. g x y : S & z : A}"
- by (auto intro: finite_vimageI)
-
-lemma
- "finite S ==> finite A ==> inj (%(x, y). g x y) ==> inj (%(x, y). h x y)
- ==> finite {f a b c d | a b c d. g a c : S & h b d : A}"
- by (auto intro: finite_vimageI)
-
-lemma
- assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"
-using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
- (* injectivity to be automated with further rules and automation *)
-
-schematic_lemma (* check interaction with schematics *)
- "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
- = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
- by simp
-
-declare [[simproc del: finite_Collect]]
-
-
-section {* Testing simproc in code generation *}
-
-definition union :: "nat set => nat set => nat set"
-where
- "union A B = {x. x : A \<or> x : B}"
-
-definition common_subsets :: "nat set => nat set => nat set set"
-where
- "common_subsets S1 S2 = {S. S \<subseteq> S1 \<and> S \<subseteq> S2}"
-
-definition products :: "nat set => nat set => nat set"
-where
- "products A B = {c. EX a b. a : A & b : B & c = a * b}"
-
-export_code products in Haskell
-
-export_code union common_subsets products in Haskell
-
-end