# HG changeset patch # User wenzelm # Date 1393014475 -3600 # Node ID bab10fb557c2b9bd40454a73468c12cdcf44a785 # Parent d696adf157e6c5b54c688f85b079f086b416b124# Parent 12448c1798517b0924465988c5f3b6b6baf83d20 merged diff -r d696adf157e6 -r bab10fb557c2 src/HOL/Hoare/Hoare_Logic.thy --- 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 diff -r d696adf157e6 -r bab10fb557c2 src/HOL/Hoare/Hoare_Logic_Abort.thy --- 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: *) diff -r d696adf157e6 -r bab10fb557c2 src/HOL/Hoare/hoare_syntax.ML --- 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; diff -r d696adf157e6 -r bab10fb557c2 src/HOL/Hoare/hoare_tac.ML --- 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; + diff -r d696adf157e6 -r bab10fb557c2 src/HOL/Isar_Examples/Hoare.thy --- 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 \ ('a \ 'b)" ("(.'(_').)" [0] 1000) - "_antiquote" :: "('a \ 'b) \ 'b" ("\_" [1000] 1000) - "_Subst" :: "'a bexp \ 'b \ idt \ 'a bexp" - ("_[_'/\_]" [1000] 999) - "_Assert" :: "'a \ 'a set" ("(\_\)" [0] 1000) - "_Assign" :: "idt \ 'b \ 'a com" ("(\_ :=/ _)" [70, 65] 61) - "_Cond" :: "'a bexp \ 'a com \ 'a com \ 'a com" - ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) - "_While_inv" :: "'a bexp \ 'a assn \ 'a com \ 'a com" - ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) - "_While" :: "'a bexp \ 'a com \ 'a com" - ("(0WHILE _ //DO _ /OD)" [0, 0] 61) + "_quote" :: "'b \ ('a \ 'b)" + "_antiquote" :: "('a \ 'b) \ 'b" ("\_" [1000] 1000) + "_Subst" :: "'a bexp \ 'b \ idt \ 'a bexp" ("_[_'/\_]" [1000] 999) + "_Assert" :: "'a \ 'a set" ("(\_\)" [0] 1000) + "_Assign" :: "idt \ 'b \ 'a com" ("(\_ :=/ _)" [70, 65] 61) + "_Cond" :: "'a bexp \ 'a com \ 'a com \ 'a com" + ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) + "_While_inv" :: "'a bexp \ 'a assn \ 'a com \ 'a com" + ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) + "_While" :: "'a bexp \ 'a com \ 'a com" ("(0WHILE _ //DO _ /OD)" [0, 0] 61) translations - "\b\" \ "CONST Collect .(b)." - "B [a/\x]" \ "\\(_update_name x (\_. a)) \ B\" - "\x := a" \ "CONST Basic .(\(_update_name x (\_. a)))." + "\b\" \ "CONST Collect (_quote b)" + "B [a/\x]" \ "\\(_update_name x (\_. a)) \ B\" + "\x := a" \ "CONST Basic (_quote (\(_update_name x (\_. a))))" "IF b THEN c1 ELSE c2 FI" \ "CONST Cond \b\ c1 c2" - "WHILE b INV i DO c OD" \ "CONST While \b\ i c" - "WHILE b DO c OD" \ "WHILE b INV CONST undefined DO c OD" + "WHILE b INV i DO c OD" \ "CONST While \b\ i c" + "WHILE b DO c OD" \ "WHILE b INV CONST undefined DO c OD" parse_translation {* let @@ -328,12 +326,10 @@ text {* While statements --- with optional invariant. *} -lemma [intro?]: - "\ (P \ b) c P \ \ P (While b P c) (P \ -b)" +lemma [intro?]: "\ (P \ b) c P \ \ P (While b P c) (P \ -b)" by (rule while) -lemma [intro?]: - "\ (P \ b) c P \ \ P (While b undefined c) (P \ -b)" +lemma [intro?]: "\ (P \ b) c P \ \ P (While b undefined c) (P \ -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" diff -r d696adf157e6 -r bab10fb557c2 src/HOL/ROOT --- 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 diff -r d696adf157e6 -r bab10fb557c2 src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy --- /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 \ b : B}" + by simp + +lemma + "finite B ==> finite A' ==> finite {f a b| a b. a : A \ a : A' \ b : B}" + by simp + +lemma + "finite A ==> finite B ==> finite {f a b| a b. a : A \ b : B \ b : B'}" + by simp + +lemma + "finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \ b : B \ 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 \ b : B \ c : C \ 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 \ b : B \ c : C \ d : D \ e : E}" + by simp + +lemma + "finite A ==> finite B ==> finite C ==> finite D ==> finite E \ + finite {f a d c b e | e b c d a. b : B \ a : A \ e : E' \ c : C \ d : D \ e : E \ b : B'}" + by simp + +lemma + "\ finite A ; finite B ; finite C ; finite D \ + \ finite ({f a b c d| a b c d. a : A \ b : B \ c : C \ d : D})" + by simp + +lemma + "finite ((\(a,b,c,d). f a b c d) ` (A \ B \ C \ D)) + \ finite ({f a b c d| a b c d. a : A \ b : B \ c : C \ 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 \ b : B \ a \ Z}" + by simp + +lemma + "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \ b : B \ (x,y) \ R}" +by simp + +lemma + "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \ (x,y) \ R \ b : B}" +by simp + +lemma + "finite A ==> finite B ==> finite R ==> finite {f a (x, b) y| y b x a. a : A \ (x,y) \ R \ b : B}" +by simp + +lemma + "finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \ a : AA) \ b : B \ a \ 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 \ a : A2) \ (a : A3 \ (a : A4 \ a : A5))) \ b : B \ a \ 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 \ ?'B \ bool. \a b. x = Pair_Rep a b} + = finite ((\(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \ 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 \ x : B}" + +definition common_subsets :: "nat set => nat set => nat set set" +where + "common_subsets S1 S2 = {S. S \ S1 \ S \ 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 diff -r d696adf157e6 -r bab10fb557c2 src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy --- 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 \ b : B}" - by simp - -lemma - "finite B ==> finite A' ==> finite {f a b| a b. a : A \ a : A' \ b : B}" - by simp - -lemma - "finite A ==> finite B ==> finite {f a b| a b. a : A \ b : B \ b : B'}" - by simp - -lemma - "finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \ b : B \ 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 \ b : B \ c : C \ 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 \ b : B \ c : C \ d : D \ e : E}" - by simp - -lemma - "finite A ==> finite B ==> finite C ==> finite D ==> finite E \ - finite {f a d c b e | e b c d a. b : B \ a : A \ e : E' \ c : C \ d : D \ e : E \ b : B'}" - by simp - -lemma - "\ finite A ; finite B ; finite C ; finite D \ - \ finite ({f a b c d| a b c d. a : A \ b : B \ c : C \ d : D})" - by simp - -lemma - "finite ((\(a,b,c,d). f a b c d) ` (A \ B \ C \ D)) - \ finite ({f a b c d| a b c d. a : A \ b : B \ c : C \ 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 \ b : B \ a \ Z}" - by simp - -lemma - "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \ b : B \ (x,y) \ R}" -by simp - -lemma - "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \ (x,y) \ R \ b : B}" -by simp - -lemma - "finite A ==> finite B ==> finite R ==> finite {f a (x, b) y| y b x a. a : A \ (x,y) \ R \ b : B}" -by simp - -lemma - "finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \ a : AA) \ b : B \ a \ 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 \ a : A2) \ (a : A3 \ (a : A4 \ a : A5))) \ b : B \ a \ 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 \ ?'B \ bool. \a b. x = Pair_Rep a b} - = finite ((\(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \ 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 \ x : B}" - -definition common_subsets :: "nat set => nat set => nat set set" -where - "common_subsets S1 S2 = {S. S \ S1 \ S \ 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