# HG changeset patch # User blanchet # Date 1307385395 -7200 # Node ID c71657bbdbc0bb82d32e5108bd8856e751276620 # Parent c6c6c2bc6fe8da4ec2c4b8e68b5205fbee375413 tuned Metis examples diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/IsaMakefile Mon Jun 06 20:36:35 2011 +0200 @@ -706,11 +706,11 @@ HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz $(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \ - Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \ - Metis_Examples/BT.thy Metis_Examples/Clausify.thy \ - Metis_Examples/HO_Reas.thy Metis_Examples/Message.thy \ - Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \ - Metis_Examples/Typings.thy Metis_Examples/set.thy + Metis_Examples/Abstraction.thy Metis_Examples/Big_O.thy \ + Metis_Examples/Binary_Tree.thy Metis_Examples/Clausification.thy \ + Metis_Examples/Message.thy Metis_Examples/Proxies.thy \ + Metis_Examples/Sets.thy Metis_Examples/Tarski.thy \ + Metis_Examples/Trans_Closure.thy Metis_Examples/Type_Encodings.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Abstraction.thy --- a/src/HOL/Metis_Examples/Abstraction.thy Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Metis_Examples/Abstraction.thy Mon Jun 06 20:36:35 2011 +0200 @@ -1,10 +1,12 @@ (* Title: HOL/Metis_Examples/Abstraction.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen -Testing Metis. +Example featuring Metis's support for lambda-abstractions. *) +header {* Example Featuring Metis's Support for Lambda-Abstractions *} + theory Abstraction imports Main "~~/src/HOL/Library/FuncSet" begin @@ -93,7 +95,7 @@ declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Pi" ]] lemma - "(cl,f) \ (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) ==> + "(cl,f) \ (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) ==> f \ pset cl \ pset cl" proof - assume A1: "(cl, f) \ (SIGMA cl:CL. {f. f \ pset cl \ pset cl})" @@ -125,38 +127,38 @@ by auto declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Int" ]] -lemma "(cl,f) \ CLF ==> +lemma "(cl,f) \ CLF ==> CLF \ (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> f \ pset cl \ cl" by auto declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]] -lemma "(cl,f) \ CLF ==> +lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> f \ pset cl \ cl" by auto declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]] -lemma - "(cl,f) \ CLF ==> - CLF \ (SIGMA cl': CL. {f. f \ pset cl' \ pset cl'}) ==> +lemma + "(cl,f) \ CLF ==> + CLF \ (SIGMA cl': CL. {f. f \ pset cl' \ pset cl'}) ==> f \ pset cl \ pset cl" by fast declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]] -lemma - "(cl,f) \ CLF ==> - CLF = (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) ==> +lemma + "(cl,f) \ CLF ==> + CLF = (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) ==> f \ pset cl \ pset cl" by auto declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]] -lemma - "(cl,f) \ CLF ==> +lemma + "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL. {f. f \ pset cl \ pset cl & monotone f (pset cl) (order cl)}) ==> (f \ pset cl \ pset cl) & (monotone f (pset cl) (order cl))" by auto @@ -168,7 +170,7 @@ by auto declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipB" ]] -lemma "map (%w. (w -> w, w \ w)) xs = +lemma "map (%w. (w -> w, w \ w)) xs = zip (map (%w. w -> w) xs) (map (%w. w \ w) xs)" apply (induct xs) apply (metis Nil_is_map_conv zip_Nil) @@ -179,12 +181,12 @@ by (metis Collect_def image_subset_iff mem_def) declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenB" ]] -lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A +lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A ==> (\x. even x --> f (f (Suc(f x))) \ A)"; by (metis Collect_def imageI image_image image_subset_iff mem_def) declare [[ sledgehammer_problem_prefix = "Abstraction__image_curry" ]] -lemma "f \ (%u v. b \ u \ v) ` A ==> \u v. P (b \ u \ v) ==> P(f y)" +lemma "f \ (%u v. b \ u \ v) ` A ==> \u v. P (b \ u \ v) ==> P(f y)" (*sledgehammer*) by auto @@ -203,13 +205,13 @@ (*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*) apply (erule ssubst) apply (subst split_conv) -apply (rule SigmaI) +apply (rule SigmaI) apply (erule imageI) + txt{*subgoal 2*} apply (clarify ); -apply (simp add: ); -apply (rule rev_image_eqI) -apply (blast intro: elim:); +apply (simp add: ); +apply (rule rev_image_eqI) +apply (blast intro: elim:); apply (simp add: ); done @@ -224,8 +226,8 @@ declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesC" ]] lemma image_TimesC: - "(%(x,y). (x \ x, y \ y)) ` (A \ B) = - ((%x. x \ x) ` A) \ ((%y. y \ y) ` B)" + "(%(x,y). (x \ x, y \ y)) ` (A \ B) = + ((%x. x \ x) ` A) \ ((%y. y \ y) ` B)" (*sledgehammer*) by auto diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/BT.thy --- a/src/HOL/Metis_Examples/BT.thy Mon Jun 06 20:36:35 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,278 +0,0 @@ -(* Title: HOL/Metis_Examples/BT.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - -Testing Metis. -*) - -header {* Binary trees *} - -theory BT -imports Main -begin - -declare [[metis_new_skolemizer]] - -datatype 'a bt = - Lf - | Br 'a "'a bt" "'a bt" - -primrec n_nodes :: "'a bt => nat" where - "n_nodes Lf = 0" -| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" - -primrec n_leaves :: "'a bt => nat" where - "n_leaves Lf = Suc 0" -| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" - -primrec depth :: "'a bt => nat" where - "depth Lf = 0" -| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))" - -primrec reflect :: "'a bt => 'a bt" where - "reflect Lf = Lf" -| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" - -primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where - "bt_map f Lf = Lf" -| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" - -primrec preorder :: "'a bt => 'a list" where - "preorder Lf = []" -| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" - -primrec inorder :: "'a bt => 'a list" where - "inorder Lf = []" -| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" - -primrec postorder :: "'a bt => 'a list" where - "postorder Lf = []" -| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" - -primrec append :: "'a bt => 'a bt => 'a bt" where - "append Lf t = t" -| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)" - -text {* \medskip BT simplification *} - -declare [[ sledgehammer_problem_prefix = "BT__n_leaves_reflect" ]] - -lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" -proof (induct t) - case Lf thus ?case - proof - - let "?p\<^isub>1 x\<^isub>1" = "x\<^isub>1 \ n_leaves (reflect (Lf::'a bt))" - have "\ ?p\<^isub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1)) - hence "\ ?p\<^isub>1 (n_leaves (Lf::'a bt))" by (metis n_leaves.simps(1)) - thus "n_leaves (reflect (Lf::'a bt)) = n_leaves (Lf::'a bt)" by metis - qed -next - case (Br a t1 t2) thus ?case - by (metis n_leaves.simps(2) nat_add_commute reflect.simps(2)) -qed - -declare [[ sledgehammer_problem_prefix = "BT__n_nodes_reflect" ]] - -lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" -proof (induct t) - case Lf thus ?case by (metis reflect.simps(1)) -next - case (Br a t1 t2) thus ?case - by (metis add_commute n_nodes.simps(2) reflect.simps(2)) -qed - -declare [[ sledgehammer_problem_prefix = "BT__depth_reflect" ]] - -lemma depth_reflect: "depth (reflect t) = depth t" -apply (induct t) - apply (metis depth.simps(1) reflect.simps(1)) -by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2)) - -text {* -The famous relationship between the numbers of leaves and nodes. -*} - -declare [[ sledgehammer_problem_prefix = "BT__n_leaves_nodes" ]] - -lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" -apply (induct t) - apply (metis n_leaves.simps(1) n_nodes.simps(1)) -by auto - -declare [[ sledgehammer_problem_prefix = "BT__reflect_reflect_ident" ]] - -lemma reflect_reflect_ident: "reflect (reflect t) = t" -apply (induct t) - apply (metis reflect.simps(1)) -proof - - fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt" - assume A1: "reflect (reflect t1) = t1" - assume A2: "reflect (reflect t2) = t2" - have "\V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)" - using A1 by (metis reflect.simps(2)) - hence "\V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))" - by (metis reflect.simps(2)) - hence "\U. reflect (reflect (Br U t1 t2)) = Br U t1 t2" - using A2 by metis - thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast -qed - -declare [[ sledgehammer_problem_prefix = "BT__bt_map_ident" ]] - -lemma bt_map_ident: "bt_map (%x. x) = (%y. y)" -apply (rule ext) -apply (induct_tac y) - apply (metis bt_map.simps(1)) -by (metis bt_map.simps(2)) - -declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]] - -lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)" -apply (induct t) - apply (metis append.simps(1) bt_map.simps(1)) -by (metis append.simps(2) bt_map.simps(2)) - -declare [[ sledgehammer_problem_prefix = "BT__bt_map_compose" ]] - -lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)" -apply (induct t) - apply (metis bt_map.simps(1)) -by (metis bt_map.simps(2) o_eq_dest_lhs) - -declare [[ sledgehammer_problem_prefix = "BT__bt_map_reflect" ]] - -lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" -apply (induct t) - apply (metis bt_map.simps(1) reflect.simps(1)) -by (metis bt_map.simps(2) reflect.simps(2)) - -declare [[ sledgehammer_problem_prefix = "BT__preorder_bt_map" ]] - -lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" -apply (induct t) - apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1)) -by simp - -declare [[ sledgehammer_problem_prefix = "BT__inorder_bt_map" ]] - -lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" -proof (induct t) - case Lf thus ?case - proof - - have "map f [] = []" by (metis map.simps(1)) - hence "map f [] = inorder Lf" by (metis inorder.simps(1)) - hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1)) - thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1)) - qed -next - case (Br a t1 t2) thus ?case by simp -qed - -declare [[ sledgehammer_problem_prefix = "BT__postorder_bt_map" ]] - -lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" -apply (induct t) - apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1)) -by simp - -declare [[ sledgehammer_problem_prefix = "BT__depth_bt_map" ]] - -lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" -apply (induct t) - apply (metis bt_map.simps(1) depth.simps(1)) -by simp - -declare [[ sledgehammer_problem_prefix = "BT__n_leaves_bt_map" ]] - -lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" -apply (induct t) - apply (metis bt_map.simps(1) n_leaves.simps(1)) -proof - - fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt" - assume A1: "n_leaves (bt_map f t1) = n_leaves t1" - assume A2: "n_leaves (bt_map f t2) = n_leaves t2" - have "\V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V" - using A1 by (metis n_leaves.simps(2)) - hence "\V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)" - by (metis bt_map.simps(2)) - hence F1: "\U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2" - using A2 by metis - have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)" - by (metis n_leaves.simps(2)) - thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)" - using F1 by metis -qed - -declare [[ sledgehammer_problem_prefix = "BT__preorder_reflect" ]] - -lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" -apply (induct t) - apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1) - reflect.simps(1)) -apply simp -done - -declare [[ sledgehammer_problem_prefix = "BT__inorder_reflect" ]] - -lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" -apply (induct t) - apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1)) -by simp -(* Slow: -by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2) - reflect.simps(2) rev.simps(2) rev_append) -*) - -declare [[ sledgehammer_problem_prefix = "BT__postorder_reflect" ]] - -lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" -apply (induct t) - apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1) - reflect.simps(1)) -by (metis preorder_reflect reflect_reflect_ident rev_swap) - -text {* -Analogues of the standard properties of the append function for lists. -*} - -declare [[ sledgehammer_problem_prefix = "BT__append_assoc" ]] - -lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)" -apply (induct t1) - apply (metis append.simps(1)) -by (metis append.simps(2)) - -declare [[ sledgehammer_problem_prefix = "BT__append_Lf2" ]] - -lemma append_Lf2 [simp]: "append t Lf = t" -apply (induct t) - apply (metis append.simps(1)) -by (metis append.simps(2)) - -declare max_add_distrib_left [simp] - -declare [[ sledgehammer_problem_prefix = "BT__depth_append" ]] - -lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2" -apply (induct t1) - apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1)) -by simp - -declare [[ sledgehammer_problem_prefix = "BT__n_leaves_append" ]] - -lemma n_leaves_append [simp]: - "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" -apply (induct t1) - apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1) - semiring_norm(111)) -by (simp add: left_distrib) - -declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]] - -lemma (*bt_map_append:*) - "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" -apply (induct t1) - apply (metis append.simps(1) bt_map.simps(1)) -by (metis bt_map_append) - -end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/BigO.thy --- a/src/HOL/Metis_Examples/BigO.thy Mon Jun 06 20:36:35 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,966 +0,0 @@ -(* Title: HOL/Metis_Examples/BigO.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - -Testing Metis. -*) - -header {* Big O notation *} - -theory BigO -imports - "~~/src/HOL/Decision_Procs/Dense_Linear_Order" - Main - "~~/src/HOL/Library/Function_Algebras" - "~~/src/HOL/Library/Set_Algebras" -begin - -declare [[metis_new_skolemizer]] - -subsection {* Definitions *} - -definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where - "O(f::('a => 'b)) == {h. EX c. ALL x. abs (h x) <= c * abs (f x)}" - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_pos_const" ]] -lemma bigo_pos_const: "(EX (c::'a::linordered_idom). - ALL x. (abs (h x)) <= (c * (abs (f x)))) - = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" - apply auto - apply (case_tac "c = 0", simp) - apply (rule_tac x = "1" in exI, simp) - apply (rule_tac x = "abs c" in exI, auto) - apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult) - done - -(*** Now various verions with an increasing shrink factor ***) - -sledgehammer_params [isar_proof, isar_shrink_factor = 1] - -lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). - ALL x. (abs (h x)) <= (c * (abs (f x)))) - = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" - apply auto - apply (case_tac "c = 0", simp) - apply (rule_tac x = "1" in exI, simp) - apply (rule_tac x = "abs c" in exI, auto) -proof - - fix c :: 'a and x :: 'b - assume A1: "\x. \h x\ \ c * \f x\" - have F1: "\x\<^isub>1\'a\linordered_idom. 0 \ \x\<^isub>1\" by (metis abs_ge_zero) - have F2: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) - have F3: "\x\<^isub>1 x\<^isub>3. x\<^isub>3 \ \h x\<^isub>1\ \ x\<^isub>3 \ c * \f x\<^isub>1\" by (metis A1 order_trans) - have F4: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" - by (metis abs_mult) - have F5: "\x\<^isub>3 x\<^isub>1\'a\linordered_idom. 0 \ x\<^isub>1 \ \x\<^isub>3 * x\<^isub>1\ = \x\<^isub>3\ * x\<^isub>1" - by (metis abs_mult_pos) - hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = \1\ * x\<^isub>1" by (metis F2) - hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F2 abs_one) - hence "\x\<^isub>3. 0 \ \h x\<^isub>3\ \ \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis F3) - hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis F1) - hence "\x\<^isub>3. (0\'a) \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c\ * \f x\<^isub>3\" by (metis F5) - hence "\x\<^isub>3. (0\'a) \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c * f x\<^isub>3\" by (metis F4) - hence "\x\<^isub>3. c * \f x\<^isub>3\ = \c * f x\<^isub>3\" by (metis F1) - hence "\h x\ \ \c * f x\" by (metis A1) - thus "\h x\ \ \c\ * \f x\" by (metis F4) -qed - -sledgehammer_params [isar_proof, isar_shrink_factor = 2] - -lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). - ALL x. (abs (h x)) <= (c * (abs (f x)))) - = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" - apply auto - apply (case_tac "c = 0", simp) - apply (rule_tac x = "1" in exI, simp) - apply (rule_tac x = "abs c" in exI, auto) -proof - - fix c :: 'a and x :: 'b - assume A1: "\x. \h x\ \ c * \f x\" - have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) - have F2: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" - by (metis abs_mult) - have "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_mult_pos abs_one) - hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis A1 abs_ge_zero order_trans) - hence "\x\<^isub>3. 0 \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c * f x\<^isub>3\" by (metis F2 abs_mult_pos) - hence "\h x\ \ \c * f x\" by (metis A1 abs_ge_zero) - thus "\h x\ \ \c\ * \f x\" by (metis F2) -qed - -sledgehammer_params [isar_proof, isar_shrink_factor = 3] - -lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). - ALL x. (abs (h x)) <= (c * (abs (f x)))) - = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" - apply auto - apply (case_tac "c = 0", simp) - apply (rule_tac x = "1" in exI, simp) - apply (rule_tac x = "abs c" in exI, auto) -proof - - fix c :: 'a and x :: 'b - assume A1: "\x. \h x\ \ c * \f x\" - have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) - have F2: "\x\<^isub>3 x\<^isub>1\'a\linordered_idom. 0 \ x\<^isub>1 \ \x\<^isub>3 * x\<^isub>1\ = \x\<^isub>3\ * x\<^isub>1" by (metis abs_mult_pos) - hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_one) - hence "\x\<^isub>3. 0 \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c\ * \f x\<^isub>3\" by (metis F2 A1 abs_ge_zero order_trans) - thus "\h x\ \ \c\ * \f x\" by (metis A1 abs_mult abs_ge_zero) -qed - -sledgehammer_params [isar_proof, isar_shrink_factor = 4] - -lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). - ALL x. (abs (h x)) <= (c * (abs (f x)))) - = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" - apply auto - apply (case_tac "c = 0", simp) - apply (rule_tac x = "1" in exI, simp) - apply (rule_tac x = "abs c" in exI, auto) -proof - - fix c :: 'a and x :: 'b - assume A1: "\x. \h x\ \ c * \f x\" - have "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) - hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" - by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) - hence "\h x\ \ \c * f x\" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) - thus "\h x\ \ \c\ * \f x\" by (metis abs_mult) -qed - -sledgehammer_params [isar_proof, isar_shrink_factor = 1] - -lemma bigo_alt_def: "O(f) = - {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}" -by (auto simp add: bigo_def bigo_pos_const) - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_elt_subset" ]] -lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)" - apply (auto simp add: bigo_alt_def) - apply (rule_tac x = "ca * c" in exI) - apply (rule conjI) - apply (rule mult_pos_pos) - apply (assumption)+ -(*sledgehammer*) - apply (rule allI) - apply (drule_tac x = "xa" in spec)+ - apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))") - apply (erule order_trans) - apply (simp add: mult_ac) - apply (rule mult_left_mono, assumption) - apply (rule order_less_imp_le, assumption) -done - - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_refl" ]] -lemma bigo_refl [intro]: "f : O(f)" -apply (auto simp add: bigo_def) -by (metis mult_1 order_refl) - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_zero" ]] -lemma bigo_zero: "0 : O(g)" -apply (auto simp add: bigo_def func_zero) -by (metis mult_zero_left order_refl) - -lemma bigo_zero2: "O(%x.0) = {%x.0}" - by (auto simp add: bigo_def) - -lemma bigo_plus_self_subset [intro]: - "O(f) \ O(f) <= O(f)" - apply (auto simp add: bigo_alt_def set_plus_def) - apply (rule_tac x = "c + ca" in exI) - apply auto - apply (simp add: ring_distribs func_plus) - apply (blast intro:order_trans abs_triangle_ineq add_mono elim:) -done - -lemma bigo_plus_idemp [simp]: "O(f) \ O(f) = O(f)" - apply (rule equalityI) - apply (rule bigo_plus_self_subset) - apply (rule set_zero_plus2) - apply (rule bigo_zero) -done - -lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \ O(g)" - apply (rule subsetI) - apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def) - apply (subst bigo_pos_const [symmetric])+ - apply (rule_tac x = - "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI) - apply (rule conjI) - apply (rule_tac x = "c + c" in exI) - apply (clarsimp) - apply (auto) - apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)") - apply (erule_tac x = xa in allE) - apply (erule order_trans) - apply (simp) - apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") - apply (erule order_trans) - apply (simp add: ring_distribs) - apply (rule mult_left_mono) - apply assumption - apply (simp add: order_less_le) - apply (rule mult_left_mono) - apply (simp add: abs_triangle_ineq) - apply (simp add: order_less_le) - apply (rule mult_nonneg_nonneg) - apply (rule add_nonneg_nonneg) - apply auto - apply (rule_tac x = "%n. if (abs (f n)) < abs (g n) then x n else 0" - in exI) - apply (rule conjI) - apply (rule_tac x = "c + c" in exI) - apply auto - apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)") - apply (erule_tac x = xa in allE) - apply (erule order_trans) - apply (simp) - apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") - apply (erule order_trans) - apply (simp add: ring_distribs) - apply (rule mult_left_mono) - apply (simp add: order_less_le) - apply (simp add: order_less_le) - apply (rule mult_left_mono) - apply (rule abs_triangle_ineq) - apply (simp add: order_less_le) -apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff) - apply (rule ext) - apply (auto simp add: if_splits linorder_not_le) -done - -lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \ B <= O(f)" - apply (subgoal_tac "A \ B <= O(f) \ O(f)") - apply (erule order_trans) - apply simp - apply (auto del: subsetI simp del: bigo_plus_idemp) -done - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq" ]] -lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> - O(f + g) = O(f) \ O(g)" - apply (rule equalityI) - apply (rule bigo_plus_subset) - apply (simp add: bigo_alt_def set_plus_def func_plus) - apply clarify -(*sledgehammer*) - apply (rule_tac x = "max c ca" in exI) - apply (rule conjI) - apply (metis Orderings.less_max_iff_disj) - apply clarify - apply (drule_tac x = "xa" in spec)+ - apply (subgoal_tac "0 <= f xa + g xa") - apply (simp add: ring_distribs) - apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)") - apply (subgoal_tac "abs(a xa) + abs(b xa) <= - max c ca * f xa + max c ca * g xa") - apply (blast intro: order_trans) - defer 1 - apply (rule abs_triangle_ineq) - apply (metis add_nonneg_nonneg) - apply (rule add_mono) -using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]] - apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6)) - apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans) -done - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt" ]] -lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> - f : O(g)" - apply (auto simp add: bigo_def) -(* Version 1: one-line proof *) - apply (metis abs_le_D1 linorder_class.not_less order_less_le Orderings.xt1(12) abs_mult) - done - -lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> - f : O(g)" -apply (auto simp add: bigo_def) -(* Version 2: structured proof *) -proof - - assume "\x. f x \ c * g x" - thus "\c. \x. f x \ c * \g x\" by (metis abs_mult abs_ge_self order_trans) -qed - -text{*So here is the easier (and more natural) problem using transitivity*} -declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]] -lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" -apply (auto simp add: bigo_def) -(* Version 1: one-line proof *) -by (metis abs_ge_self abs_mult order_trans) - -text{*So here is the easier (and more natural) problem using transitivity*} -declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]] -lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" - apply (auto simp add: bigo_def) -(* Version 2: structured proof *) -proof - - assume "\x. f x \ c * g x" - thus "\c. \x. f x \ c * \g x\" by (metis abs_mult abs_ge_self order_trans) -qed - -lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> - f : O(g)" - apply (erule bigo_bounded_alt [of f 1 g]) - apply simp -done - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded2" ]] -lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==> - f : lb +o O(g)" -apply (rule set_minus_imp_plus) -apply (rule bigo_bounded) - apply (auto simp add: diff_minus fun_Compl_def func_plus) - prefer 2 - apply (drule_tac x = x in spec)+ - apply (metis add_right_mono add_commute diff_add_cancel diff_minus_eq_add le_less order_trans) -proof - - fix x :: 'a - assume "\x. lb x \ f x" - thus "(0\'b) \ f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le) -qed - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs" ]] -lemma bigo_abs: "(%x. abs(f x)) =o O(f)" -apply (unfold bigo_def) -apply auto -by (metis mult_1 order_refl) - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs2" ]] -lemma bigo_abs2: "f =o O(%x. abs(f x))" -apply (unfold bigo_def) -apply auto -by (metis mult_1 order_refl) - -lemma bigo_abs3: "O(f) = O(%x. abs(f x))" -proof - - have F1: "\v u. u \ O(v) \ O(u) \ O(v)" by (metis bigo_elt_subset) - have F2: "\u. (\R. \u R\) \ O(u)" by (metis bigo_abs) - have "\u. u \ O(\R. \u R\)" by (metis bigo_abs2) - thus "O(f) = O(\x. \f x\)" using F1 F2 by auto -qed - -lemma bigo_abs4: "f =o g +o O(h) ==> - (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)" - apply (drule set_plus_imp_minus) - apply (rule set_minus_imp_plus) - apply (subst fun_diff_def) -proof - - assume a: "f - g : O(h)" - have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))" - by (rule bigo_abs2) - also have "... <= O(%x. abs (f x - g x))" - apply (rule bigo_elt_subset) - apply (rule bigo_bounded) - apply force - apply (rule allI) - apply (rule abs_triangle_ineq3) - done - also have "... <= O(f - g)" - apply (rule bigo_elt_subset) - apply (subst fun_diff_def) - apply (rule bigo_abs) - done - also have "... <= O(h)" - using a by (rule bigo_elt_subset) - finally show "(%x. abs (f x) - abs (g x)) : O(h)". -qed - -lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" -by (unfold bigo_def, auto) - -lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \ O(h)" -proof - - assume "f : g +o O(h)" - also have "... <= O(g) \ O(h)" - by (auto del: subsetI) - also have "... = O(%x. abs(g x)) \ O(%x. abs(h x))" - apply (subst bigo_abs3 [symmetric])+ - apply (rule refl) - done - also have "... = O((%x. abs(g x)) + (%x. abs(h x)))" - by (rule bigo_plus_eq [symmetric], auto) - finally have "f : ...". - then have "O(f) <= ..." - by (elim bigo_elt_subset) - also have "... = O(%x. abs(g x)) \ O(%x. abs(h x))" - by (rule bigo_plus_eq, auto) - finally show ?thesis - by (simp add: bigo_abs3 [symmetric]) -qed - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult" ]] -lemma bigo_mult [intro]: "O(f)\O(g) <= O(f * g)" - apply (rule subsetI) - apply (subst bigo_def) - apply (auto simp del: abs_mult mult_ac - simp add: bigo_alt_def set_times_def func_times) -(*sledgehammer*) - apply (rule_tac x = "c * ca" in exI) - apply(rule allI) - apply(erule_tac x = x in allE)+ - apply(subgoal_tac "c * ca * abs(f x * g x) = - (c * abs(f x)) * (ca * abs(g x))") -using [[ sledgehammer_problem_prefix = "BigO__bigo_mult_simpler" ]] -prefer 2 -apply (metis mult_assoc mult_left_commute - abs_of_pos mult_left_commute - abs_mult mult_pos_pos) - apply (erule ssubst) - apply (subst abs_mult) -(* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since - abs_mult has just been done *) -by (metis abs_ge_zero mult_mono') - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult2" ]] -lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)" - apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult) -(*sledgehammer*) - apply (rule_tac x = c in exI) - apply clarify - apply (drule_tac x = x in spec) -using [[ sledgehammer_problem_prefix = "BigO__bigo_mult2_simpler" ]] -(*sledgehammer [no luck]*) - apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))") - apply (simp add: mult_ac) - apply (rule mult_left_mono, assumption) - apply (rule abs_ge_zero) -done - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult3" ]] -lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)" -by (metis bigo_mult set_rev_mp set_times_intro) - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult4" ]] -lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)" -by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib) - - -lemma bigo_mult5: "ALL x. f x ~= 0 ==> - O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)" -proof - - assume a: "ALL x. f x ~= 0" - show "O(f * g) <= f *o O(g)" - proof - fix h - assume h: "h : O(f * g)" - then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)" - by auto - also have "... <= O((%x. 1 / f x) * (f * g))" - by (rule bigo_mult2) - also have "(%x. 1 / f x) * (f * g) = g" - apply (simp add: func_times) - apply (rule ext) - apply (simp add: a h nonzero_divide_eq_eq mult_ac) - done - finally have "(%x. (1::'b) / f x) * h : O(g)". - then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)" - by auto - also have "f * ((%x. (1::'b) / f x) * h) = h" - apply (simp add: func_times) - apply (rule ext) - apply (simp add: a h nonzero_divide_eq_eq mult_ac) - done - finally show "h : f *o O(g)". - qed -qed - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult6" ]] -lemma bigo_mult6: "ALL x. f x ~= 0 ==> - O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)" -by (metis bigo_mult2 bigo_mult5 order_antisym) - -(*proof requires relaxing relevance: 2007-01-25*) -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult7" ]] - declare bigo_mult6 [simp] -lemma bigo_mult7: "ALL x. f x ~= 0 ==> - O(f * g) <= O(f::'a => ('b::linordered_field)) \ O(g)" -(*sledgehammer*) - apply (subst bigo_mult6) - apply assumption - apply (rule set_times_mono3) - apply (rule bigo_refl) -done - declare bigo_mult6 [simp del] - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult8" ]] - declare bigo_mult7[intro!] -lemma bigo_mult8: "ALL x. f x ~= 0 ==> - O(f * g) = O(f::'a => ('b::linordered_field)) \ O(g)" -by (metis bigo_mult bigo_mult7 order_antisym_conv) - -lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)" - by (auto simp add: bigo_def fun_Compl_def) - -lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)" - apply (rule set_minus_imp_plus) - apply (drule set_plus_imp_minus) - apply (drule bigo_minus) - apply (simp add: diff_minus) -done - -lemma bigo_minus3: "O(-f) = O(f)" - by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel) - -lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)" -proof - - assume a: "f : O(g)" - show "f +o O(g) <= O(g)" - proof - - have "f : O(f)" by auto - then have "f +o O(g) <= O(f) \ O(g)" - by (auto del: subsetI) - also have "... <= O(g) \ O(g)" - proof - - from a have "O(f) <= O(g)" by (auto del: subsetI) - thus ?thesis by (auto del: subsetI) - qed - also have "... <= O(g)" by (simp add: bigo_plus_idemp) - finally show ?thesis . - qed -qed - -lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)" -proof - - assume a: "f : O(g)" - show "O(g) <= f +o O(g)" - proof - - from a have "-f : O(g)" by auto - then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1) - then have "f +o (-f +o O(g)) <= f +o O(g)" by auto - also have "f +o (-f +o O(g)) = O(g)" - by (simp add: set_plus_rearranges) - finally show ?thesis . - qed -qed - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_absorb" ]] -lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)" -by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff) - -lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)" - apply (subgoal_tac "f +o A <= f +o O(g)") - apply force+ -done - -lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)" - apply (subst set_minus_plus [symmetric]) - apply (subgoal_tac "g - f = - (f - g)") - apply (erule ssubst) - apply (rule bigo_minus) - apply (subst set_minus_plus) - apply assumption - apply (simp add: diff_minus add_ac) -done - -lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))" - apply (rule iffI) - apply (erule bigo_add_commute_imp)+ -done - -lemma bigo_const1: "(%x. c) : O(%x. 1)" -by (auto simp add: bigo_def mult_ac) - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const2" ]] -lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)" -by (metis bigo_const1 bigo_elt_subset) - -lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)" -(* "thus" had to be replaced by "show" with an explicit reference to "F1" *) -proof - - have F1: "\u. (\Q. u) \ O(\Q. 1)" by (metis bigo_const1) - show "O(\x. c) \ O(\x. 1)" by (metis F1 bigo_elt_subset) -qed - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const3" ]] -lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)" -apply (simp add: bigo_def) -by (metis abs_eq_0 left_inverse order_refl) - -lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)" -by (rule bigo_elt_subset, rule bigo_const3, assumption) - -lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==> - O(%x. c) = O(%x. 1)" -by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption) - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult1" ]] -lemma bigo_const_mult1: "(%x. c * f x) : O(f)" - apply (simp add: bigo_def abs_mult) -by (metis le_less) - -lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)" -by (rule bigo_elt_subset, rule bigo_const_mult1) - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult3" ]] -lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)" - apply (simp add: bigo_def) -(*sledgehammer [no luck]*) - apply (rule_tac x = "abs(inverse c)" in exI) - apply (simp only: abs_mult [symmetric] mult_assoc [symmetric]) -apply (subst left_inverse) -apply (auto ) -done - -lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==> - O(f) <= O(%x. c * f x)" -by (rule bigo_elt_subset, rule bigo_const_mult3, assumption) - -lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==> - O(%x. c * f x) = O(f)" -by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4) - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult5" ]] -lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==> - (%x. c) *o O(f) = O(f)" - apply (auto del: subsetI) - apply (rule order_trans) - apply (rule bigo_mult2) - apply (simp add: func_times) - apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times) - apply (rule_tac x = "%y. inverse c * x y" in exI) - apply (rename_tac g d) - apply safe - apply (rule_tac [2] ext) - prefer 2 - apply simp - apply (simp add: mult_assoc [symmetric] abs_mult) - (* couldn't get this proof without the step above *) -proof - - fix g :: "'b \ 'a" and d :: 'a - assume A1: "c \ (0\'a)" - assume A2: "\x\'b. \g x\ \ d * \f x\" - have F1: "inverse \c\ = \inverse c\" using A1 by (metis nonzero_abs_inverse) - have F2: "(0\'a) < \c\" using A1 by (metis zero_less_abs_iff) - have "(0\'a) < \c\ \ (0\'a) < \inverse c\" using F1 by (metis positive_imp_inverse_positive) - hence "(0\'a) < \inverse c\" using F2 by metis - hence F3: "(0\'a) \ \inverse c\" by (metis order_le_less) - have "\(u\'a) SKF\<^isub>7\'a \ 'b. \g (SKF\<^isub>7 (\inverse c\ * u))\ \ u * \f (SKF\<^isub>7 (\inverse c\ * u))\" - using A2 by metis - hence F4: "\(u\'a) SKF\<^isub>7\'a \ 'b. \g (SKF\<^isub>7 (\inverse c\ * u))\ \ u * \f (SKF\<^isub>7 (\inverse c\ * u))\ \ (0\'a) \ \inverse c\" - using F3 by metis - hence "\(v\'a) (u\'a) SKF\<^isub>7\'a \ 'b. \inverse c\ * \g (SKF\<^isub>7 (u * v))\ \ u * (v * \f (SKF\<^isub>7 (u * v))\)" - by (metis comm_mult_left_mono) - thus "\ca\'a. \x\'b. \inverse c\ * \g x\ \ ca * \f x\" - using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono) -qed - - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult6" ]] -lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)" - apply (auto intro!: subsetI - simp add: bigo_def elt_set_times_def func_times - simp del: abs_mult mult_ac) -(*sledgehammer*) - apply (rule_tac x = "ca * (abs c)" in exI) - apply (rule allI) - apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))") - apply (erule ssubst) - apply (subst abs_mult) - apply (rule mult_left_mono) - apply (erule spec) - apply simp - apply(simp add: mult_ac) -done - -lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)" -proof - - assume "f =o O(g)" - then have "(%x. c) * f =o (%x. c) *o O(g)" - by auto - also have "(%x. c) * f = (%x. c * f x)" - by (simp add: func_times) - also have "(%x. c) *o O(g) <= O(g)" - by (auto del: subsetI) - finally show ?thesis . -qed - -lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))" -by (unfold bigo_def, auto) - -lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o - O(%x. h(k x))" - apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def - func_plus) - apply (erule bigo_compose1) -done - -subsection {* Setsum *} - -lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==> - EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==> - (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)" - apply (auto simp add: bigo_def) - apply (rule_tac x = "abs c" in exI) - apply (subst abs_of_nonneg) back back - apply (rule setsum_nonneg) - apply force - apply (subst setsum_right_distrib) - apply (rule allI) - apply (rule order_trans) - apply (rule setsum_abs) - apply (rule setsum_mono) -apply (blast intro: order_trans mult_right_mono abs_ge_self) -done - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum1" ]] -lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> - EX c. ALL x y. abs(f x y) <= c * (h x y) ==> - (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)" - apply (rule bigo_setsum_main) -(*sledgehammer*) - apply force - apply clarsimp - apply (rule_tac x = c in exI) - apply force -done - -lemma bigo_setsum2: "ALL y. 0 <= h y ==> - EX c. ALL y. abs(f y) <= c * (h y) ==> - (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)" -by (rule bigo_setsum1, auto) - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum3" ]] -lemma bigo_setsum3: "f =o O(h) ==> - (%x. SUM y : A x. (l x y) * f(k x y)) =o - O(%x. SUM y : A x. abs(l x y * h(k x y)))" - apply (rule bigo_setsum1) - apply (rule allI)+ - apply (rule abs_ge_zero) - apply (unfold bigo_def) - apply (auto simp add: abs_mult) -(*sledgehammer*) - apply (rule_tac x = c in exI) - apply (rule allI)+ - apply (subst mult_left_commute) - apply (rule mult_left_mono) - apply (erule spec) - apply (rule abs_ge_zero) -done - -lemma bigo_setsum4: "f =o g +o O(h) ==> - (%x. SUM y : A x. l x y * f(k x y)) =o - (%x. SUM y : A x. l x y * g(k x y)) +o - O(%x. SUM y : A x. abs(l x y * h(k x y)))" - apply (rule set_minus_imp_plus) - apply (subst fun_diff_def) - apply (subst setsum_subtractf [symmetric]) - apply (subst right_diff_distrib [symmetric]) - apply (rule bigo_setsum3) - apply (subst fun_diff_def [symmetric]) - apply (erule set_plus_imp_minus) -done - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum5" ]] -lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> - ALL x. 0 <= h x ==> - (%x. SUM y : A x. (l x y) * f(k x y)) =o - O(%x. SUM y : A x. (l x y) * h(k x y))" - apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) = - (%x. SUM y : A x. abs((l x y) * h(k x y)))") - apply (erule ssubst) - apply (erule bigo_setsum3) - apply (rule ext) - apply (rule setsum_cong2) - apply (thin_tac "f \ O(h)") -apply (metis abs_of_nonneg zero_le_mult_iff) -done - -lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==> - ALL x. 0 <= h x ==> - (%x. SUM y : A x. (l x y) * f(k x y)) =o - (%x. SUM y : A x. (l x y) * g(k x y)) +o - O(%x. SUM y : A x. (l x y) * h(k x y))" - apply (rule set_minus_imp_plus) - apply (subst fun_diff_def) - apply (subst setsum_subtractf [symmetric]) - apply (subst right_diff_distrib [symmetric]) - apply (rule bigo_setsum5) - apply (subst fun_diff_def [symmetric]) - apply (drule set_plus_imp_minus) - apply auto -done - -subsection {* Misc useful stuff *} - -lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==> - A \ B <= O(f)" - apply (subst bigo_plus_idemp [symmetric]) - apply (rule set_plus_mono2) - apply assumption+ -done - -lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)" - apply (subst bigo_plus_idemp [symmetric]) - apply (rule set_plus_intro) - apply assumption+ -done - -lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==> - (%x. c) * f =o O(h) ==> f =o O(h)" - apply (rule subsetD) - apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)") - apply assumption - apply (rule bigo_const_mult6) - apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)") - apply (erule ssubst) - apply (erule set_times_intro2) - apply (simp add: func_times) -done - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_fix" ]] -lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==> - f =o O(h)" - apply (simp add: bigo_alt_def) -(*sledgehammer*) - apply clarify - apply (rule_tac x = c in exI) - apply safe - apply (case_tac "x = 0") -apply (metis abs_ge_zero abs_zero order_less_le split_mult_pos_le) - apply (subgoal_tac "x = Suc (x - 1)") - apply metis - apply simp - done - - -lemma bigo_fix2: - "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> - f 0 = g 0 ==> f =o g +o O(h)" - apply (rule set_minus_imp_plus) - apply (rule bigo_fix) - apply (subst fun_diff_def) - apply (subst fun_diff_def [symmetric]) - apply (rule set_plus_imp_minus) - apply simp - apply (simp add: fun_diff_def) -done - -subsection {* Less than or equal to *} - -definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl " ALL x. abs (g x) <= abs (f x) ==> - g =o O(h)" - apply (unfold bigo_def) - apply clarsimp -apply (blast intro: order_trans) -done - -lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==> - g =o O(h)" - apply (erule bigo_lesseq1) -apply (blast intro: abs_ge_self order_trans) -done - -lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==> - g =o O(h)" - apply (erule bigo_lesseq2) - apply (rule allI) - apply (subst abs_of_nonneg) - apply (erule spec)+ -done - -lemma bigo_lesseq4: "f =o O(h) ==> - ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==> - g =o O(h)" - apply (erule bigo_lesseq1) - apply (rule allI) - apply (subst abs_of_nonneg) - apply (erule spec)+ -done - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso1" ]] -lemma bigo_lesso1: "ALL x. f x <= g x ==> f x. max (f x - g x) 0) = 0" - thus "(\x. max (f x - g x) 0) \ O(h)" by (metis bigo_zero) -next - show "\x\'a. f x \ g x \ (\x\'a. max (f x - g x) (0\'b)) = (0\'a \ 'b)" - apply (unfold func_zero) - apply (rule ext) - by (simp split: split_max) -qed - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso2" ]] -lemma bigo_lesso2: "f =o g +o O(h) ==> - ALL x. 0 <= k x ==> ALL x. k x <= f x ==> - k x\'a. k x \ f x" - hence F1: "\x\<^isub>1\'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2) - assume "(0\'b) \ k x - g x" - hence F2: "max (0\'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2) - have F3: "\x\<^isub>1\'b. x\<^isub>1 \ \x\<^isub>1\" by (metis abs_le_iff le_less) - have "\(x\<^isub>2\'b) x\<^isub>1\'b. max x\<^isub>1 x\<^isub>2 \ x\<^isub>2 \ max x\<^isub>1 x\<^isub>2 \ x\<^isub>1" by (metis le_less le_max_iff_disj) - hence "\(x\<^isub>3\'b) (x\<^isub>2\'b) x\<^isub>1\'b. x\<^isub>1 - x\<^isub>2 \ x\<^isub>3 - x\<^isub>2 \ x\<^isub>3 \ x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE) - hence "k x - g x \ f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute) - hence "k x - g x \ \f x - g x\" by (metis F3 le_max_iff_disj min_max.sup_absorb2) - thus "max (k x - g x) (0\'b) \ \f x - g x\" by (metis F2 min_max.sup_commute) -next - show "\x\'a. - \\x\'a. (0\'b) \ k x; \x\'a. k x \ f x; \ (0\'b) \ k x - g x\ - \ max (k x - g x) (0\'b) \ \f x - g x\" - by (metis abs_ge_zero le_cases min_max.sup_absorb2) -qed - -declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3" ]] -lemma bigo_lesso3: "f =o g +o O(h) ==> - ALL x. 0 <= k x ==> ALL x. g x <= k x ==> - f 'b::linordered_field) ==> - g =o h +o O(k) ==> f - EX C. ALL x. f x <= g x + C * abs(h x)" - apply (simp only: lesso_def bigo_alt_def) - apply clarsimp - apply (metis abs_if abs_mult add_commute diff_le_eq less_not_permute) -done - -end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Big_O.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Metis_Examples/Big_O.thy Mon Jun 06 20:36:35 2011 +0200 @@ -0,0 +1,966 @@ +(* Title: HOL/Metis_Examples/Big_O.thy + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + +Metis example featuring the Big O notation. +*) + +header {* Metis Example Featuring the Big O Notation *} + +theory Big_O +imports + "~~/src/HOL/Decision_Procs/Dense_Linear_Order" + Main + "~~/src/HOL/Library/Function_Algebras" + "~~/src/HOL/Library/Set_Algebras" +begin + +declare [[metis_new_skolemizer]] + +subsection {* Definitions *} + +definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where + "O(f::('a => 'b)) == {h. EX c. ALL x. abs (h x) <= c * abs (f x)}" + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_pos_const" ]] +lemma bigo_pos_const: "(EX (c::'a::linordered_idom). + ALL x. (abs (h x)) <= (c * (abs (f x)))) + = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" + apply auto + apply (case_tac "c = 0", simp) + apply (rule_tac x = "1" in exI, simp) + apply (rule_tac x = "abs c" in exI, auto) + apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult) + done + +(*** Now various verions with an increasing shrink factor ***) + +sledgehammer_params [isar_proof, isar_shrink_factor = 1] + +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). + ALL x. (abs (h x)) <= (c * (abs (f x)))) + = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" + apply auto + apply (case_tac "c = 0", simp) + apply (rule_tac x = "1" in exI, simp) + apply (rule_tac x = "abs c" in exI, auto) +proof - + fix c :: 'a and x :: 'b + assume A1: "\x. \h x\ \ c * \f x\" + have F1: "\x\<^isub>1\'a\linordered_idom. 0 \ \x\<^isub>1\" by (metis abs_ge_zero) + have F2: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) + have F3: "\x\<^isub>1 x\<^isub>3. x\<^isub>3 \ \h x\<^isub>1\ \ x\<^isub>3 \ c * \f x\<^isub>1\" by (metis A1 order_trans) + have F4: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" + by (metis abs_mult) + have F5: "\x\<^isub>3 x\<^isub>1\'a\linordered_idom. 0 \ x\<^isub>1 \ \x\<^isub>3 * x\<^isub>1\ = \x\<^isub>3\ * x\<^isub>1" + by (metis abs_mult_pos) + hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = \1\ * x\<^isub>1" by (metis F2) + hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F2 abs_one) + hence "\x\<^isub>3. 0 \ \h x\<^isub>3\ \ \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis F3) + hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis F1) + hence "\x\<^isub>3. (0\'a) \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c\ * \f x\<^isub>3\" by (metis F5) + hence "\x\<^isub>3. (0\'a) \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c * f x\<^isub>3\" by (metis F4) + hence "\x\<^isub>3. c * \f x\<^isub>3\ = \c * f x\<^isub>3\" by (metis F1) + hence "\h x\ \ \c * f x\" by (metis A1) + thus "\h x\ \ \c\ * \f x\" by (metis F4) +qed + +sledgehammer_params [isar_proof, isar_shrink_factor = 2] + +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). + ALL x. (abs (h x)) <= (c * (abs (f x)))) + = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" + apply auto + apply (case_tac "c = 0", simp) + apply (rule_tac x = "1" in exI, simp) + apply (rule_tac x = "abs c" in exI, auto) +proof - + fix c :: 'a and x :: 'b + assume A1: "\x. \h x\ \ c * \f x\" + have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) + have F2: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" + by (metis abs_mult) + have "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_mult_pos abs_one) + hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis A1 abs_ge_zero order_trans) + hence "\x\<^isub>3. 0 \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c * f x\<^isub>3\" by (metis F2 abs_mult_pos) + hence "\h x\ \ \c * f x\" by (metis A1 abs_ge_zero) + thus "\h x\ \ \c\ * \f x\" by (metis F2) +qed + +sledgehammer_params [isar_proof, isar_shrink_factor = 3] + +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). + ALL x. (abs (h x)) <= (c * (abs (f x)))) + = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" + apply auto + apply (case_tac "c = 0", simp) + apply (rule_tac x = "1" in exI, simp) + apply (rule_tac x = "abs c" in exI, auto) +proof - + fix c :: 'a and x :: 'b + assume A1: "\x. \h x\ \ c * \f x\" + have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) + have F2: "\x\<^isub>3 x\<^isub>1\'a\linordered_idom. 0 \ x\<^isub>1 \ \x\<^isub>3 * x\<^isub>1\ = \x\<^isub>3\ * x\<^isub>1" by (metis abs_mult_pos) + hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_one) + hence "\x\<^isub>3. 0 \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c\ * \f x\<^isub>3\" by (metis F2 A1 abs_ge_zero order_trans) + thus "\h x\ \ \c\ * \f x\" by (metis A1 abs_mult abs_ge_zero) +qed + +sledgehammer_params [isar_proof, isar_shrink_factor = 4] + +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). + ALL x. (abs (h x)) <= (c * (abs (f x)))) + = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" + apply auto + apply (case_tac "c = 0", simp) + apply (rule_tac x = "1" in exI, simp) + apply (rule_tac x = "abs c" in exI, auto) +proof - + fix c :: 'a and x :: 'b + assume A1: "\x. \h x\ \ c * \f x\" + have "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) + hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" + by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) + hence "\h x\ \ \c * f x\" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) + thus "\h x\ \ \c\ * \f x\" by (metis abs_mult) +qed + +sledgehammer_params [isar_proof, isar_shrink_factor = 1] + +lemma bigo_alt_def: "O(f) = + {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}" +by (auto simp add: bigo_def bigo_pos_const) + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_elt_subset" ]] +lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)" + apply (auto simp add: bigo_alt_def) + apply (rule_tac x = "ca * c" in exI) + apply (rule conjI) + apply (rule mult_pos_pos) + apply (assumption)+ +(*sledgehammer*) + apply (rule allI) + apply (drule_tac x = "xa" in spec)+ + apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))") + apply (erule order_trans) + apply (simp add: mult_ac) + apply (rule mult_left_mono, assumption) + apply (rule order_less_imp_le, assumption) +done + + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_refl" ]] +lemma bigo_refl [intro]: "f : O(f)" +apply (auto simp add: bigo_def) +by (metis mult_1 order_refl) + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_zero" ]] +lemma bigo_zero: "0 : O(g)" +apply (auto simp add: bigo_def func_zero) +by (metis mult_zero_left order_refl) + +lemma bigo_zero2: "O(%x.0) = {%x.0}" + by (auto simp add: bigo_def) + +lemma bigo_plus_self_subset [intro]: + "O(f) \ O(f) <= O(f)" + apply (auto simp add: bigo_alt_def set_plus_def) + apply (rule_tac x = "c + ca" in exI) + apply auto + apply (simp add: ring_distribs func_plus) + apply (blast intro:order_trans abs_triangle_ineq add_mono elim:) +done + +lemma bigo_plus_idemp [simp]: "O(f) \ O(f) = O(f)" + apply (rule equalityI) + apply (rule bigo_plus_self_subset) + apply (rule set_zero_plus2) + apply (rule bigo_zero) +done + +lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \ O(g)" + apply (rule subsetI) + apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def) + apply (subst bigo_pos_const [symmetric])+ + apply (rule_tac x = + "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI) + apply (rule conjI) + apply (rule_tac x = "c + c" in exI) + apply (clarsimp) + apply (auto) + apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)") + apply (erule_tac x = xa in allE) + apply (erule order_trans) + apply (simp) + apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") + apply (erule order_trans) + apply (simp add: ring_distribs) + apply (rule mult_left_mono) + apply assumption + apply (simp add: order_less_le) + apply (rule mult_left_mono) + apply (simp add: abs_triangle_ineq) + apply (simp add: order_less_le) + apply (rule mult_nonneg_nonneg) + apply (rule add_nonneg_nonneg) + apply auto + apply (rule_tac x = "%n. if (abs (f n)) < abs (g n) then x n else 0" + in exI) + apply (rule conjI) + apply (rule_tac x = "c + c" in exI) + apply auto + apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)") + apply (erule_tac x = xa in allE) + apply (erule order_trans) + apply (simp) + apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") + apply (erule order_trans) + apply (simp add: ring_distribs) + apply (rule mult_left_mono) + apply (simp add: order_less_le) + apply (simp add: order_less_le) + apply (rule mult_left_mono) + apply (rule abs_triangle_ineq) + apply (simp add: order_less_le) +apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff) + apply (rule ext) + apply (auto simp add: if_splits linorder_not_le) +done + +lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \ B <= O(f)" + apply (subgoal_tac "A \ B <= O(f) \ O(f)") + apply (erule order_trans) + apply simp + apply (auto del: subsetI simp del: bigo_plus_idemp) +done + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq" ]] +lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> + O(f + g) = O(f) \ O(g)" + apply (rule equalityI) + apply (rule bigo_plus_subset) + apply (simp add: bigo_alt_def set_plus_def func_plus) + apply clarify +(*sledgehammer*) + apply (rule_tac x = "max c ca" in exI) + apply (rule conjI) + apply (metis Orderings.less_max_iff_disj) + apply clarify + apply (drule_tac x = "xa" in spec)+ + apply (subgoal_tac "0 <= f xa + g xa") + apply (simp add: ring_distribs) + apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)") + apply (subgoal_tac "abs(a xa) + abs(b xa) <= + max c ca * f xa + max c ca * g xa") + apply (blast intro: order_trans) + defer 1 + apply (rule abs_triangle_ineq) + apply (metis add_nonneg_nonneg) + apply (rule add_mono) +using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]] + apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6)) + apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans) +done + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt" ]] +lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> + f : O(g)" + apply (auto simp add: bigo_def) +(* Version 1: one-line proof *) + apply (metis abs_le_D1 linorder_class.not_less order_less_le Orderings.xt1(12) abs_mult) + done + +lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> + f : O(g)" +apply (auto simp add: bigo_def) +(* Version 2: structured proof *) +proof - + assume "\x. f x \ c * g x" + thus "\c. \x. f x \ c * \g x\" by (metis abs_mult abs_ge_self order_trans) +qed + +text{*So here is the easier (and more natural) problem using transitivity*} +declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]] +lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" +apply (auto simp add: bigo_def) +(* Version 1: one-line proof *) +by (metis abs_ge_self abs_mult order_trans) + +text{*So here is the easier (and more natural) problem using transitivity*} +declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]] +lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" + apply (auto simp add: bigo_def) +(* Version 2: structured proof *) +proof - + assume "\x. f x \ c * g x" + thus "\c. \x. f x \ c * \g x\" by (metis abs_mult abs_ge_self order_trans) +qed + +lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> + f : O(g)" + apply (erule bigo_bounded_alt [of f 1 g]) + apply simp +done + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded2" ]] +lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==> + f : lb +o O(g)" +apply (rule set_minus_imp_plus) +apply (rule bigo_bounded) + apply (auto simp add: diff_minus fun_Compl_def func_plus) + prefer 2 + apply (drule_tac x = x in spec)+ + apply (metis add_right_mono add_commute diff_add_cancel diff_minus_eq_add le_less order_trans) +proof - + fix x :: 'a + assume "\x. lb x \ f x" + thus "(0\'b) \ f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le) +qed + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs" ]] +lemma bigo_abs: "(%x. abs(f x)) =o O(f)" +apply (unfold bigo_def) +apply auto +by (metis mult_1 order_refl) + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs2" ]] +lemma bigo_abs2: "f =o O(%x. abs(f x))" +apply (unfold bigo_def) +apply auto +by (metis mult_1 order_refl) + +lemma bigo_abs3: "O(f) = O(%x. abs(f x))" +proof - + have F1: "\v u. u \ O(v) \ O(u) \ O(v)" by (metis bigo_elt_subset) + have F2: "\u. (\R. \u R\) \ O(u)" by (metis bigo_abs) + have "\u. u \ O(\R. \u R\)" by (metis bigo_abs2) + thus "O(f) = O(\x. \f x\)" using F1 F2 by auto +qed + +lemma bigo_abs4: "f =o g +o O(h) ==> + (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)" + apply (drule set_plus_imp_minus) + apply (rule set_minus_imp_plus) + apply (subst fun_diff_def) +proof - + assume a: "f - g : O(h)" + have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))" + by (rule bigo_abs2) + also have "... <= O(%x. abs (f x - g x))" + apply (rule bigo_elt_subset) + apply (rule bigo_bounded) + apply force + apply (rule allI) + apply (rule abs_triangle_ineq3) + done + also have "... <= O(f - g)" + apply (rule bigo_elt_subset) + apply (subst fun_diff_def) + apply (rule bigo_abs) + done + also have "... <= O(h)" + using a by (rule bigo_elt_subset) + finally show "(%x. abs (f x) - abs (g x)) : O(h)". +qed + +lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" +by (unfold bigo_def, auto) + +lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \ O(h)" +proof - + assume "f : g +o O(h)" + also have "... <= O(g) \ O(h)" + by (auto del: subsetI) + also have "... = O(%x. abs(g x)) \ O(%x. abs(h x))" + apply (subst bigo_abs3 [symmetric])+ + apply (rule refl) + done + also have "... = O((%x. abs(g x)) + (%x. abs(h x)))" + by (rule bigo_plus_eq [symmetric], auto) + finally have "f : ...". + then have "O(f) <= ..." + by (elim bigo_elt_subset) + also have "... = O(%x. abs(g x)) \ O(%x. abs(h x))" + by (rule bigo_plus_eq, auto) + finally show ?thesis + by (simp add: bigo_abs3 [symmetric]) +qed + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult" ]] +lemma bigo_mult [intro]: "O(f)\O(g) <= O(f * g)" + apply (rule subsetI) + apply (subst bigo_def) + apply (auto simp del: abs_mult mult_ac + simp add: bigo_alt_def set_times_def func_times) +(*sledgehammer*) + apply (rule_tac x = "c * ca" in exI) + apply(rule allI) + apply(erule_tac x = x in allE)+ + apply(subgoal_tac "c * ca * abs(f x * g x) = + (c * abs(f x)) * (ca * abs(g x))") +using [[ sledgehammer_problem_prefix = "BigO__bigo_mult_simpler" ]] +prefer 2 +apply (metis mult_assoc mult_left_commute + abs_of_pos mult_left_commute + abs_mult mult_pos_pos) + apply (erule ssubst) + apply (subst abs_mult) +(* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since + abs_mult has just been done *) +by (metis abs_ge_zero mult_mono') + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult2" ]] +lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)" + apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult) +(*sledgehammer*) + apply (rule_tac x = c in exI) + apply clarify + apply (drule_tac x = x in spec) +using [[ sledgehammer_problem_prefix = "BigO__bigo_mult2_simpler" ]] +(*sledgehammer [no luck]*) + apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))") + apply (simp add: mult_ac) + apply (rule mult_left_mono, assumption) + apply (rule abs_ge_zero) +done + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult3" ]] +lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)" +by (metis bigo_mult set_rev_mp set_times_intro) + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult4" ]] +lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)" +by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib) + + +lemma bigo_mult5: "ALL x. f x ~= 0 ==> + O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)" +proof - + assume a: "ALL x. f x ~= 0" + show "O(f * g) <= f *o O(g)" + proof + fix h + assume h: "h : O(f * g)" + then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)" + by auto + also have "... <= O((%x. 1 / f x) * (f * g))" + by (rule bigo_mult2) + also have "(%x. 1 / f x) * (f * g) = g" + apply (simp add: func_times) + apply (rule ext) + apply (simp add: a h nonzero_divide_eq_eq mult_ac) + done + finally have "(%x. (1::'b) / f x) * h : O(g)". + then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)" + by auto + also have "f * ((%x. (1::'b) / f x) * h) = h" + apply (simp add: func_times) + apply (rule ext) + apply (simp add: a h nonzero_divide_eq_eq mult_ac) + done + finally show "h : f *o O(g)". + qed +qed + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult6" ]] +lemma bigo_mult6: "ALL x. f x ~= 0 ==> + O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)" +by (metis bigo_mult2 bigo_mult5 order_antisym) + +(*proof requires relaxing relevance: 2007-01-25*) +declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult7" ]] + declare bigo_mult6 [simp] +lemma bigo_mult7: "ALL x. f x ~= 0 ==> + O(f * g) <= O(f::'a => ('b::linordered_field)) \ O(g)" +(*sledgehammer*) + apply (subst bigo_mult6) + apply assumption + apply (rule set_times_mono3) + apply (rule bigo_refl) +done + declare bigo_mult6 [simp del] + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult8" ]] + declare bigo_mult7[intro!] +lemma bigo_mult8: "ALL x. f x ~= 0 ==> + O(f * g) = O(f::'a => ('b::linordered_field)) \ O(g)" +by (metis bigo_mult bigo_mult7 order_antisym_conv) + +lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)" + by (auto simp add: bigo_def fun_Compl_def) + +lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)" + apply (rule set_minus_imp_plus) + apply (drule set_plus_imp_minus) + apply (drule bigo_minus) + apply (simp add: diff_minus) +done + +lemma bigo_minus3: "O(-f) = O(f)" + by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel) + +lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)" +proof - + assume a: "f : O(g)" + show "f +o O(g) <= O(g)" + proof - + have "f : O(f)" by auto + then have "f +o O(g) <= O(f) \ O(g)" + by (auto del: subsetI) + also have "... <= O(g) \ O(g)" + proof - + from a have "O(f) <= O(g)" by (auto del: subsetI) + thus ?thesis by (auto del: subsetI) + qed + also have "... <= O(g)" by (simp add: bigo_plus_idemp) + finally show ?thesis . + qed +qed + +lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)" +proof - + assume a: "f : O(g)" + show "O(g) <= f +o O(g)" + proof - + from a have "-f : O(g)" by auto + then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1) + then have "f +o (-f +o O(g)) <= f +o O(g)" by auto + also have "f +o (-f +o O(g)) = O(g)" + by (simp add: set_plus_rearranges) + finally show ?thesis . + qed +qed + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_absorb" ]] +lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)" +by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff) + +lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)" + apply (subgoal_tac "f +o A <= f +o O(g)") + apply force+ +done + +lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)" + apply (subst set_minus_plus [symmetric]) + apply (subgoal_tac "g - f = - (f - g)") + apply (erule ssubst) + apply (rule bigo_minus) + apply (subst set_minus_plus) + apply assumption + apply (simp add: diff_minus add_ac) +done + +lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))" + apply (rule iffI) + apply (erule bigo_add_commute_imp)+ +done + +lemma bigo_const1: "(%x. c) : O(%x. 1)" +by (auto simp add: bigo_def mult_ac) + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_const2" ]] +lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)" +by (metis bigo_const1 bigo_elt_subset) + +lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)" +(* "thus" had to be replaced by "show" with an explicit reference to "F1" *) +proof - + have F1: "\u. (\Q. u) \ O(\Q. 1)" by (metis bigo_const1) + show "O(\x. c) \ O(\x. 1)" by (metis F1 bigo_elt_subset) +qed + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_const3" ]] +lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)" +apply (simp add: bigo_def) +by (metis abs_eq_0 left_inverse order_refl) + +lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)" +by (rule bigo_elt_subset, rule bigo_const3, assumption) + +lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==> + O(%x. c) = O(%x. 1)" +by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption) + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult1" ]] +lemma bigo_const_mult1: "(%x. c * f x) : O(f)" + apply (simp add: bigo_def abs_mult) +by (metis le_less) + +lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)" +by (rule bigo_elt_subset, rule bigo_const_mult1) + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult3" ]] +lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)" + apply (simp add: bigo_def) +(*sledgehammer [no luck]*) + apply (rule_tac x = "abs(inverse c)" in exI) + apply (simp only: abs_mult [symmetric] mult_assoc [symmetric]) +apply (subst left_inverse) +apply (auto ) +done + +lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==> + O(f) <= O(%x. c * f x)" +by (rule bigo_elt_subset, rule bigo_const_mult3, assumption) + +lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==> + O(%x. c * f x) = O(f)" +by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4) + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult5" ]] +lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==> + (%x. c) *o O(f) = O(f)" + apply (auto del: subsetI) + apply (rule order_trans) + apply (rule bigo_mult2) + apply (simp add: func_times) + apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times) + apply (rule_tac x = "%y. inverse c * x y" in exI) + apply (rename_tac g d) + apply safe + apply (rule_tac [2] ext) + prefer 2 + apply simp + apply (simp add: mult_assoc [symmetric] abs_mult) + (* couldn't get this proof without the step above *) +proof - + fix g :: "'b \ 'a" and d :: 'a + assume A1: "c \ (0\'a)" + assume A2: "\x\'b. \g x\ \ d * \f x\" + have F1: "inverse \c\ = \inverse c\" using A1 by (metis nonzero_abs_inverse) + have F2: "(0\'a) < \c\" using A1 by (metis zero_less_abs_iff) + have "(0\'a) < \c\ \ (0\'a) < \inverse c\" using F1 by (metis positive_imp_inverse_positive) + hence "(0\'a) < \inverse c\" using F2 by metis + hence F3: "(0\'a) \ \inverse c\" by (metis order_le_less) + have "\(u\'a) SKF\<^isub>7\'a \ 'b. \g (SKF\<^isub>7 (\inverse c\ * u))\ \ u * \f (SKF\<^isub>7 (\inverse c\ * u))\" + using A2 by metis + hence F4: "\(u\'a) SKF\<^isub>7\'a \ 'b. \g (SKF\<^isub>7 (\inverse c\ * u))\ \ u * \f (SKF\<^isub>7 (\inverse c\ * u))\ \ (0\'a) \ \inverse c\" + using F3 by metis + hence "\(v\'a) (u\'a) SKF\<^isub>7\'a \ 'b. \inverse c\ * \g (SKF\<^isub>7 (u * v))\ \ u * (v * \f (SKF\<^isub>7 (u * v))\)" + by (metis comm_mult_left_mono) + thus "\ca\'a. \x\'b. \inverse c\ * \g x\ \ ca * \f x\" + using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono) +qed + + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult6" ]] +lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)" + apply (auto intro!: subsetI + simp add: bigo_def elt_set_times_def func_times + simp del: abs_mult mult_ac) +(*sledgehammer*) + apply (rule_tac x = "ca * (abs c)" in exI) + apply (rule allI) + apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))") + apply (erule ssubst) + apply (subst abs_mult) + apply (rule mult_left_mono) + apply (erule spec) + apply simp + apply(simp add: mult_ac) +done + +lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)" +proof - + assume "f =o O(g)" + then have "(%x. c) * f =o (%x. c) *o O(g)" + by auto + also have "(%x. c) * f = (%x. c * f x)" + by (simp add: func_times) + also have "(%x. c) *o O(g) <= O(g)" + by (auto del: subsetI) + finally show ?thesis . +qed + +lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))" +by (unfold bigo_def, auto) + +lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o + O(%x. h(k x))" + apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def + func_plus) + apply (erule bigo_compose1) +done + +subsection {* Setsum *} + +lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==> + EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==> + (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)" + apply (auto simp add: bigo_def) + apply (rule_tac x = "abs c" in exI) + apply (subst abs_of_nonneg) back back + apply (rule setsum_nonneg) + apply force + apply (subst setsum_right_distrib) + apply (rule allI) + apply (rule order_trans) + apply (rule setsum_abs) + apply (rule setsum_mono) +apply (blast intro: order_trans mult_right_mono abs_ge_self) +done + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum1" ]] +lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> + EX c. ALL x y. abs(f x y) <= c * (h x y) ==> + (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)" + apply (rule bigo_setsum_main) +(*sledgehammer*) + apply force + apply clarsimp + apply (rule_tac x = c in exI) + apply force +done + +lemma bigo_setsum2: "ALL y. 0 <= h y ==> + EX c. ALL y. abs(f y) <= c * (h y) ==> + (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)" +by (rule bigo_setsum1, auto) + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum3" ]] +lemma bigo_setsum3: "f =o O(h) ==> + (%x. SUM y : A x. (l x y) * f(k x y)) =o + O(%x. SUM y : A x. abs(l x y * h(k x y)))" + apply (rule bigo_setsum1) + apply (rule allI)+ + apply (rule abs_ge_zero) + apply (unfold bigo_def) + apply (auto simp add: abs_mult) +(*sledgehammer*) + apply (rule_tac x = c in exI) + apply (rule allI)+ + apply (subst mult_left_commute) + apply (rule mult_left_mono) + apply (erule spec) + apply (rule abs_ge_zero) +done + +lemma bigo_setsum4: "f =o g +o O(h) ==> + (%x. SUM y : A x. l x y * f(k x y)) =o + (%x. SUM y : A x. l x y * g(k x y)) +o + O(%x. SUM y : A x. abs(l x y * h(k x y)))" + apply (rule set_minus_imp_plus) + apply (subst fun_diff_def) + apply (subst setsum_subtractf [symmetric]) + apply (subst right_diff_distrib [symmetric]) + apply (rule bigo_setsum3) + apply (subst fun_diff_def [symmetric]) + apply (erule set_plus_imp_minus) +done + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum5" ]] +lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> + ALL x. 0 <= h x ==> + (%x. SUM y : A x. (l x y) * f(k x y)) =o + O(%x. SUM y : A x. (l x y) * h(k x y))" + apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) = + (%x. SUM y : A x. abs((l x y) * h(k x y)))") + apply (erule ssubst) + apply (erule bigo_setsum3) + apply (rule ext) + apply (rule setsum_cong2) + apply (thin_tac "f \ O(h)") +apply (metis abs_of_nonneg zero_le_mult_iff) +done + +lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==> + ALL x. 0 <= h x ==> + (%x. SUM y : A x. (l x y) * f(k x y)) =o + (%x. SUM y : A x. (l x y) * g(k x y)) +o + O(%x. SUM y : A x. (l x y) * h(k x y))" + apply (rule set_minus_imp_plus) + apply (subst fun_diff_def) + apply (subst setsum_subtractf [symmetric]) + apply (subst right_diff_distrib [symmetric]) + apply (rule bigo_setsum5) + apply (subst fun_diff_def [symmetric]) + apply (drule set_plus_imp_minus) + apply auto +done + +subsection {* Misc useful stuff *} + +lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==> + A \ B <= O(f)" + apply (subst bigo_plus_idemp [symmetric]) + apply (rule set_plus_mono2) + apply assumption+ +done + +lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)" + apply (subst bigo_plus_idemp [symmetric]) + apply (rule set_plus_intro) + apply assumption+ +done + +lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==> + (%x. c) * f =o O(h) ==> f =o O(h)" + apply (rule subsetD) + apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)") + apply assumption + apply (rule bigo_const_mult6) + apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)") + apply (erule ssubst) + apply (erule set_times_intro2) + apply (simp add: func_times) +done + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_fix" ]] +lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==> + f =o O(h)" + apply (simp add: bigo_alt_def) +(*sledgehammer*) + apply clarify + apply (rule_tac x = c in exI) + apply safe + apply (case_tac "x = 0") +apply (metis abs_ge_zero abs_zero order_less_le split_mult_pos_le) + apply (subgoal_tac "x = Suc (x - 1)") + apply metis + apply simp + done + + +lemma bigo_fix2: + "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> + f 0 = g 0 ==> f =o g +o O(h)" + apply (rule set_minus_imp_plus) + apply (rule bigo_fix) + apply (subst fun_diff_def) + apply (subst fun_diff_def [symmetric]) + apply (rule set_plus_imp_minus) + apply simp + apply (simp add: fun_diff_def) +done + +subsection {* Less than or equal to *} + +definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl " ALL x. abs (g x) <= abs (f x) ==> + g =o O(h)" + apply (unfold bigo_def) + apply clarsimp +apply (blast intro: order_trans) +done + +lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==> + g =o O(h)" + apply (erule bigo_lesseq1) +apply (blast intro: abs_ge_self order_trans) +done + +lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==> + g =o O(h)" + apply (erule bigo_lesseq2) + apply (rule allI) + apply (subst abs_of_nonneg) + apply (erule spec)+ +done + +lemma bigo_lesseq4: "f =o O(h) ==> + ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==> + g =o O(h)" + apply (erule bigo_lesseq1) + apply (rule allI) + apply (subst abs_of_nonneg) + apply (erule spec)+ +done + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso1" ]] +lemma bigo_lesso1: "ALL x. f x <= g x ==> f x. max (f x - g x) 0) = 0" + thus "(\x. max (f x - g x) 0) \ O(h)" by (metis bigo_zero) +next + show "\x\'a. f x \ g x \ (\x\'a. max (f x - g x) (0\'b)) = (0\'a \ 'b)" + apply (unfold func_zero) + apply (rule ext) + by (simp split: split_max) +qed + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso2" ]] +lemma bigo_lesso2: "f =o g +o O(h) ==> + ALL x. 0 <= k x ==> ALL x. k x <= f x ==> + k x\'a. k x \ f x" + hence F1: "\x\<^isub>1\'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2) + assume "(0\'b) \ k x - g x" + hence F2: "max (0\'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2) + have F3: "\x\<^isub>1\'b. x\<^isub>1 \ \x\<^isub>1\" by (metis abs_le_iff le_less) + have "\(x\<^isub>2\'b) x\<^isub>1\'b. max x\<^isub>1 x\<^isub>2 \ x\<^isub>2 \ max x\<^isub>1 x\<^isub>2 \ x\<^isub>1" by (metis le_less le_max_iff_disj) + hence "\(x\<^isub>3\'b) (x\<^isub>2\'b) x\<^isub>1\'b. x\<^isub>1 - x\<^isub>2 \ x\<^isub>3 - x\<^isub>2 \ x\<^isub>3 \ x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE) + hence "k x - g x \ f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute) + hence "k x - g x \ \f x - g x\" by (metis F3 le_max_iff_disj min_max.sup_absorb2) + thus "max (k x - g x) (0\'b) \ \f x - g x\" by (metis F2 min_max.sup_commute) +next + show "\x\'a. + \\x\'a. (0\'b) \ k x; \x\'a. k x \ f x; \ (0\'b) \ k x - g x\ + \ max (k x - g x) (0\'b) \ \f x - g x\" + by (metis abs_ge_zero le_cases min_max.sup_absorb2) +qed + +declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3" ]] +lemma bigo_lesso3: "f =o g +o O(h) ==> + ALL x. 0 <= k x ==> ALL x. g x <= k x ==> + f 'b::linordered_field) ==> + g =o h +o O(k) ==> f + EX C. ALL x. f x <= g x + C * abs(h x)" + apply (simp only: lesso_def bigo_alt_def) + apply clarsimp + apply (metis abs_if abs_mult add_commute diff_le_eq less_not_permute) +done + +end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Binary_Tree.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Metis_Examples/Binary_Tree.thy Mon Jun 06 20:36:35 2011 +0200 @@ -0,0 +1,278 @@ +(* Title: HOL/Metis_Examples/Binary_Tree.thy + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + +Metis example featuring binary trees. +*) + +header {* Metis Example Featuring Binary Trees *} + +theory Binary_Tree +imports Main +begin + +declare [[metis_new_skolemizer]] + +datatype 'a bt = + Lf + | Br 'a "'a bt" "'a bt" + +primrec n_nodes :: "'a bt => nat" where + "n_nodes Lf = 0" +| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" + +primrec n_leaves :: "'a bt => nat" where + "n_leaves Lf = Suc 0" +| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" + +primrec depth :: "'a bt => nat" where + "depth Lf = 0" +| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))" + +primrec reflect :: "'a bt => 'a bt" where + "reflect Lf = Lf" +| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" + +primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where + "bt_map f Lf = Lf" +| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" + +primrec preorder :: "'a bt => 'a list" where + "preorder Lf = []" +| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" + +primrec inorder :: "'a bt => 'a list" where + "inorder Lf = []" +| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" + +primrec postorder :: "'a bt => 'a list" where + "postorder Lf = []" +| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" + +primrec append :: "'a bt => 'a bt => 'a bt" where + "append Lf t = t" +| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)" + +text {* \medskip BT simplification *} + +declare [[ sledgehammer_problem_prefix = "BT__n_leaves_reflect" ]] + +lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" +proof (induct t) + case Lf thus ?case + proof - + let "?p\<^isub>1 x\<^isub>1" = "x\<^isub>1 \ n_leaves (reflect (Lf::'a bt))" + have "\ ?p\<^isub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1)) + hence "\ ?p\<^isub>1 (n_leaves (Lf::'a bt))" by (metis n_leaves.simps(1)) + thus "n_leaves (reflect (Lf::'a bt)) = n_leaves (Lf::'a bt)" by metis + qed +next + case (Br a t1 t2) thus ?case + by (metis n_leaves.simps(2) nat_add_commute reflect.simps(2)) +qed + +declare [[ sledgehammer_problem_prefix = "BT__n_nodes_reflect" ]] + +lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" +proof (induct t) + case Lf thus ?case by (metis reflect.simps(1)) +next + case (Br a t1 t2) thus ?case + by (metis add_commute n_nodes.simps(2) reflect.simps(2)) +qed + +declare [[ sledgehammer_problem_prefix = "BT__depth_reflect" ]] + +lemma depth_reflect: "depth (reflect t) = depth t" +apply (induct t) + apply (metis depth.simps(1) reflect.simps(1)) +by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2)) + +text {* +The famous relationship between the numbers of leaves and nodes. +*} + +declare [[ sledgehammer_problem_prefix = "BT__n_leaves_nodes" ]] + +lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" +apply (induct t) + apply (metis n_leaves.simps(1) n_nodes.simps(1)) +by auto + +declare [[ sledgehammer_problem_prefix = "BT__reflect_reflect_ident" ]] + +lemma reflect_reflect_ident: "reflect (reflect t) = t" +apply (induct t) + apply (metis reflect.simps(1)) +proof - + fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt" + assume A1: "reflect (reflect t1) = t1" + assume A2: "reflect (reflect t2) = t2" + have "\V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)" + using A1 by (metis reflect.simps(2)) + hence "\V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))" + by (metis reflect.simps(2)) + hence "\U. reflect (reflect (Br U t1 t2)) = Br U t1 t2" + using A2 by metis + thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast +qed + +declare [[ sledgehammer_problem_prefix = "BT__bt_map_ident" ]] + +lemma bt_map_ident: "bt_map (%x. x) = (%y. y)" +apply (rule ext) +apply (induct_tac y) + apply (metis bt_map.simps(1)) +by (metis bt_map.simps(2)) + +declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]] + +lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)" +apply (induct t) + apply (metis append.simps(1) bt_map.simps(1)) +by (metis append.simps(2) bt_map.simps(2)) + +declare [[ sledgehammer_problem_prefix = "BT__bt_map_compose" ]] + +lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)" +apply (induct t) + apply (metis bt_map.simps(1)) +by (metis bt_map.simps(2) o_eq_dest_lhs) + +declare [[ sledgehammer_problem_prefix = "BT__bt_map_reflect" ]] + +lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" +apply (induct t) + apply (metis bt_map.simps(1) reflect.simps(1)) +by (metis bt_map.simps(2) reflect.simps(2)) + +declare [[ sledgehammer_problem_prefix = "BT__preorder_bt_map" ]] + +lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" +apply (induct t) + apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1)) +by simp + +declare [[ sledgehammer_problem_prefix = "BT__inorder_bt_map" ]] + +lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" +proof (induct t) + case Lf thus ?case + proof - + have "map f [] = []" by (metis map.simps(1)) + hence "map f [] = inorder Lf" by (metis inorder.simps(1)) + hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1)) + thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1)) + qed +next + case (Br a t1 t2) thus ?case by simp +qed + +declare [[ sledgehammer_problem_prefix = "BT__postorder_bt_map" ]] + +lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" +apply (induct t) + apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1)) +by simp + +declare [[ sledgehammer_problem_prefix = "BT__depth_bt_map" ]] + +lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" +apply (induct t) + apply (metis bt_map.simps(1) depth.simps(1)) +by simp + +declare [[ sledgehammer_problem_prefix = "BT__n_leaves_bt_map" ]] + +lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" +apply (induct t) + apply (metis bt_map.simps(1) n_leaves.simps(1)) +proof - + fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt" + assume A1: "n_leaves (bt_map f t1) = n_leaves t1" + assume A2: "n_leaves (bt_map f t2) = n_leaves t2" + have "\V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V" + using A1 by (metis n_leaves.simps(2)) + hence "\V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)" + by (metis bt_map.simps(2)) + hence F1: "\U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2" + using A2 by metis + have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)" + by (metis n_leaves.simps(2)) + thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)" + using F1 by metis +qed + +declare [[ sledgehammer_problem_prefix = "BT__preorder_reflect" ]] + +lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" +apply (induct t) + apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1) + reflect.simps(1)) +apply simp +done + +declare [[ sledgehammer_problem_prefix = "BT__inorder_reflect" ]] + +lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" +apply (induct t) + apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1)) +by simp +(* Slow: +by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2) + reflect.simps(2) rev.simps(2) rev_append) +*) + +declare [[ sledgehammer_problem_prefix = "BT__postorder_reflect" ]] + +lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" +apply (induct t) + apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1) + reflect.simps(1)) +by (metis preorder_reflect reflect_reflect_ident rev_swap) + +text {* +Analogues of the standard properties of the append function for lists. +*} + +declare [[ sledgehammer_problem_prefix = "BT__append_assoc" ]] + +lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)" +apply (induct t1) + apply (metis append.simps(1)) +by (metis append.simps(2)) + +declare [[ sledgehammer_problem_prefix = "BT__append_Lf2" ]] + +lemma append_Lf2 [simp]: "append t Lf = t" +apply (induct t) + apply (metis append.simps(1)) +by (metis append.simps(2)) + +declare max_add_distrib_left [simp] + +declare [[ sledgehammer_problem_prefix = "BT__depth_append" ]] + +lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2" +apply (induct t1) + apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1)) +by simp + +declare [[ sledgehammer_problem_prefix = "BT__n_leaves_append" ]] + +lemma n_leaves_append [simp]: + "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" +apply (induct t1) + apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1) + semiring_norm(111)) +by (simp add: left_distrib) + +declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]] + +lemma (*bt_map_append:*) + "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" +apply (induct t1) + apply (metis append.simps(1) bt_map.simps(1)) +by (metis bt_map_append) + +end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Clausification.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Metis_Examples/Clausification.thy Mon Jun 06 20:36:35 2011 +0200 @@ -0,0 +1,150 @@ +(* Title: HOL/Metis_Examples/Clausification.thy + Author: Jasmin Blanchette, TU Muenchen + +Example that exercises Metis's Clausifier. +*) + +header {* Example that Exercises Metis's Clausifier *} + +theory Clausification +imports Complex_Main +begin + +(* FIXME: shouldn't need this *) +declare [[unify_search_bound = 100]] +declare [[unify_trace_bound = 100]] + + +text {* Definitional CNF for facts *} + +declare [[meson_max_clauses = 10]] + +axiomatization q :: "nat \ nat \ bool" where +qax: "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" + +declare [[metis_new_skolemizer = false]] + +lemma "\b. \a. (q b a \ q a b)" +by (metis qax) + +lemma "\b. \a. (q b a \ q a b)" +by (metisFT qax) + +lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" +by (metis qax) + +lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" +by (metisFT qax) + +declare [[metis_new_skolemizer]] + +lemma "\b. \a. (q b a \ q a b)" +by (metis qax) + +lemma "\b. \a. (q b a \ q a b)" +by (metisFT qax) + +lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" +by (metis qax) + +lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" +by (metisFT qax) + +declare [[meson_max_clauses = 60]] + +axiomatization r :: "nat \ nat \ bool" where +rax: "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ + (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ + (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ + (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" + +declare [[metis_new_skolemizer = false]] + +lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" +by (metis rax) + +lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" +by (metisFT rax) + +declare [[metis_new_skolemizer]] + +lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" +by (metis rax) + +lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" +by (metisFT rax) + +lemma "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ + (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ + (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ + (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" +by (metis rax) + +lemma "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ + (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ + (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ + (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" +by (metisFT rax) + + +text {* Definitional CNF for goal *} + +axiomatization p :: "nat \ nat \ bool" where +pax: "\b. \a. (p b a \ p 0 0 \ p 1 a) \ (p 0 1 \ p 1 0 \ p a b)" + +declare [[metis_new_skolemizer = false]] + +lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ + (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" +by (metis pax) + +lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ + (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" +by (metisFT pax) + +declare [[metis_new_skolemizer]] + +lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ + (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" +by (metis pax) + +lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ + (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" +by (metisFT pax) + + +text {* New Skolemizer *} + +declare [[metis_new_skolemizer]] + +lemma + fixes x :: real + assumes fn_le: "!!n. f n \ x" and 1: "f ----> lim f" + shows "lim f \ x" +by (metis 1 LIMSEQ_le_const2 fn_le) + +definition + bounded :: "'a::metric_space set \ bool" where + "bounded S \ (\x eee. \y\S. dist x y \ eee)" + +lemma "bounded T \ S \ T ==> bounded S" +by (metis bounded_def subset_eq) + +lemma + assumes a: "Quotient R Abs Rep" + shows "symp R" +using a unfolding Quotient_def using sympI +by metisFT + +lemma + "(\x \ set xs. P x) \ + (\ys x zs. xs = ys @ x # zs \ P x \ (\z \ set zs. \ P z))" +by (metis split_list_last_prop [where P = P] in_set_conv_decomp) + +lemma ex_tl: "EX ys. tl ys = xs" +using tl.simps(2) by fast + +lemma "(\ys\nat list. tl ys = xs) \ (\bs\int list. tl bs = as)" +by (metis ex_tl) + +end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Clausify.thy --- a/src/HOL/Metis_Examples/Clausify.thy Mon Jun 06 20:36:35 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,148 +0,0 @@ -(* Title: HOL/Metis_Examples/Clausify.thy - Author: Jasmin Blanchette, TU Muenchen - -Testing Metis's clausifier. -*) - -theory Clausify -imports Complex_Main -begin - -(* FIXME: shouldn't need this *) -declare [[unify_search_bound = 100]] -declare [[unify_trace_bound = 100]] - - -text {* Definitional CNF for facts *} - -declare [[meson_max_clauses = 10]] - -axiomatization q :: "nat \ nat \ bool" where -qax: "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" - -declare [[metis_new_skolemizer = false]] - -lemma "\b. \a. (q b a \ q a b)" -by (metis qax) - -lemma "\b. \a. (q b a \ q a b)" -by (metisFT qax) - -lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" -by (metis qax) - -lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" -by (metisFT qax) - -declare [[metis_new_skolemizer]] - -lemma "\b. \a. (q b a \ q a b)" -by (metis qax) - -lemma "\b. \a. (q b a \ q a b)" -by (metisFT qax) - -lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" -by (metis qax) - -lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" -by (metisFT qax) - -declare [[meson_max_clauses = 60]] - -axiomatization r :: "nat \ nat \ bool" where -rax: "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ - (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ - (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ - (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" - -declare [[metis_new_skolemizer = false]] - -lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" -by (metis rax) - -lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" -by (metisFT rax) - -declare [[metis_new_skolemizer]] - -lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" -by (metis rax) - -lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" -by (metisFT rax) - -lemma "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ - (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ - (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ - (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" -by (metis rax) - -lemma "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ - (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ - (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ - (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" -by (metisFT rax) - - -text {* Definitional CNF for goal *} - -axiomatization p :: "nat \ nat \ bool" where -pax: "\b. \a. (p b a \ p 0 0 \ p 1 a) \ (p 0 1 \ p 1 0 \ p a b)" - -declare [[metis_new_skolemizer = false]] - -lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ - (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" -by (metis pax) - -lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ - (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" -by (metisFT pax) - -declare [[metis_new_skolemizer]] - -lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ - (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" -by (metis pax) - -lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ - (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" -by (metisFT pax) - - -text {* New Skolemizer *} - -declare [[metis_new_skolemizer]] - -lemma - fixes x :: real - assumes fn_le: "!!n. f n \ x" and 1: "f ----> lim f" - shows "lim f \ x" -by (metis 1 LIMSEQ_le_const2 fn_le) - -definition - bounded :: "'a::metric_space set \ bool" where - "bounded S \ (\x eee. \y\S. dist x y \ eee)" - -lemma "bounded T \ S \ T ==> bounded S" -by (metis bounded_def subset_eq) - -lemma - assumes a: "Quotient R Abs Rep" - shows "symp R" -using a unfolding Quotient_def using sympI -by metisFT - -lemma - "(\x \ set xs. P x) \ - (\ys x zs. xs = ys @ x # zs \ P x \ (\z \ set zs. \ P z))" -by (metis split_list_last_prop [where P = P] in_set_conv_decomp) - -lemma ex_tl: "EX ys. tl ys = xs" -using tl.simps(2) by fast - -lemma "(\ys\nat list. tl ys = xs) \ (\bs\int list. tl bs = as)" -by (metis ex_tl) - -end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/HO_Reas.thy --- a/src/HOL/Metis_Examples/HO_Reas.thy Mon Jun 06 20:36:35 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,262 +0,0 @@ -(* Title: HOL/Metis_Examples/HO_Reas.thy - Author: Jasmin Blanchette, TU Muenchen - -Testing Metis's and Sledgehammer's higher-order reasoning capabilities. -*) - -theory HO_Reas -imports Typings -begin - -declare [[metis_new_skolemizer]] - -sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0] - -text {* Extensionality and set constants *} - -lemma plus_1_not_0: "n + (1\nat) \ 0" -by simp - -definition inc :: "nat \ nat" where -"inc x = x + 1" - -lemma "inc \ (\y. 0)" -sledgehammer [expect = some] (inc_def plus_1_not_0) -by (metis_eXhaust inc_def plus_1_not_0) - -lemma "inc = (\y. y + 1)" -sledgehammer [expect = some] (inc_def) -by (metis_eXhaust inc_def) - -definition add_swap :: "nat \ nat \ nat" where -"add_swap = (\x y. y + x)" - -lemma "add_swap m n = n + m" -sledgehammer [expect = some] (add_swap_def) -by (metis_eXhaust add_swap_def) - -definition "A = {xs\'a list. True}" - -lemma "xs \ A" -sledgehammer [expect = some] -by (metis_eXhaust A_def Collect_def mem_def) - -definition "B (y::int) \ y \ 0" -definition "C (y::int) \ y \ 1" - -lemma int_le_0_imp_le_1: "x \ (0::int) \ x \ 1" -by linarith - -lemma "B \ C" -sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some] -by (metis_eXhaust B_def C_def int_le_0_imp_le_1 predicate1I) - - -text {* Proxies for logical constants *} - -lemma "id (op =) x x" -sledgehammer [type_sys = erased, expect = none] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = none] (id_apply) (* unfortunate *) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metisX id_apply) - -lemma "id True" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "\ id False" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "x = id True \ x = id False" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id x = id True \ id x = id False" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "P True \ P False \ P x" -sledgehammer [type_sys = erased, expect = none] () -sledgehammer [type_sys = poly_args, expect = none] () -sledgehammer [type_sys = poly_tags?, expect = some] () -sledgehammer [type_sys = poly_tags, expect = some] () -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] () -sledgehammer [type_sys = mangled_tags?, expect = some] () -sledgehammer [type_sys = mangled_tags, expect = some] () -sledgehammer [type_sys = mangled_preds?, expect = some] () -sledgehammer [type_sys = mangled_preds, expect = some] () -by metisX - -lemma "id (\ a) \ \ id a" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id (\ \ a) \ id a" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id (\ (id (\ a))) \ id a" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id (a \ b) \ id a" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id (a \ b) \ id b" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id a \ id b \ id (a \ b)" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id a \ id (a \ b)" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id b \ id (a \ b)" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id (\ a) \ id (\ b) \ id (\ (a \ b))" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id (\ a) \ id (a \ b)" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -lemma "id (a \ b) \ id (\ a \ b)" -sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) - -end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Message.thy --- a/src/HOL/Metis_Examples/Message.thy Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Metis_Examples/Message.thy Mon Jun 06 20:36:35 2011 +0200 @@ -1,10 +1,12 @@ (* Title: HOL/Metis_Examples/Message.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen -Testing Metis. +Metis example featuring message authentication. *) +header {* Metis Example Featuring Message Authentication *} + theory Message imports Main begin @@ -135,7 +137,7 @@ lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H" by (unfold keysFor_def, auto) -lemma keysFor_insert_Crypt [simp]: +lemma keysFor_insert_Crypt [simp]: "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)" by (unfold keysFor_def, auto) @@ -149,13 +151,13 @@ subsection{*Inductive relation "parts"*} lemma MPair_parts: - "[| {|X,Y|} \ parts H; + "[| {|X,Y|} \ parts H; [| X \ parts H; Y \ parts H |] ==> P |] ==> P" -by (blast dest: parts.Fst parts.Snd) +by (blast dest: parts.Fst parts.Snd) declare MPair_parts [elim!] parts.Body [dest!] text{*NB These two rules are UNSAFE in the formal sense, as they discard the - compound message. They work well on THIS FILE. + compound message. They work well on THIS FILE. @{text MPair_parts} is left as SAFE because it speeds up proofs. The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*} @@ -218,9 +220,9 @@ NOTE: the UN versions are no longer used!*} -text{*This allows @{text blast} to simplify occurrences of +text{*This allows @{text blast} to simplify occurrences of @{term "parts(G\H)"} in the assumption.*} -lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] +lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] declare in_parts_UnE [elim!] lemma parts_insert_subset: "insert X (parts H) \ parts(insert X H)" @@ -235,13 +237,13 @@ by blast lemma parts_subset_iff [simp]: "(parts G \ parts H) = (G \ parts H)" -apply (rule iffI) +apply (rule iffI) apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing) apply (metis parts_idem parts_mono) done lemma parts_trans: "[| X\ parts G; G \ parts H |] ==> X\ parts H" -by (blast dest: parts_mono); +by (blast dest: parts_mono); lemma parts_cut: "[|Y\ parts (insert X G); X\ parts H|] ==> Y\ parts(G \ H)" by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI) @@ -254,36 +256,36 @@ lemma parts_insert_Agent [simp]: "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)" -apply (rule parts_insert_eq_I) -apply (erule parts.induct, auto) +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) done lemma parts_insert_Nonce [simp]: "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)" -apply (rule parts_insert_eq_I) -apply (erule parts.induct, auto) +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) done lemma parts_insert_Number [simp]: "parts (insert (Number N) H) = insert (Number N) (parts H)" -apply (rule parts_insert_eq_I) -apply (erule parts.induct, auto) +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) done lemma parts_insert_Key [simp]: "parts (insert (Key K) H) = insert (Key K) (parts H)" -apply (rule parts_insert_eq_I) -apply (erule parts.induct, auto) +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) done lemma parts_insert_Hash [simp]: "parts (insert (Hash X) H) = insert (Hash X) (parts H)" -apply (rule parts_insert_eq_I) -apply (erule parts.induct, auto) +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) done lemma parts_insert_Crypt [simp]: - "parts (insert (Crypt K X) H) = + "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))" apply (rule equalityI) apply (rule subsetI) @@ -292,7 +294,7 @@ done lemma parts_insert_MPair [simp]: - "parts (insert {|X,Y|} H) = + "parts (insert {|X,Y|} H) = insert {|X,Y|} (parts (insert X (insert Y H)))" apply (rule equalityI) apply (rule subsetI) @@ -306,7 +308,7 @@ done lemma msg_Nonce_supply: "\N. \n. N\n --> Nonce n \ parts {msg}" -apply (induct_tac "msg") +apply (induct_tac "msg") apply (simp_all add: parts_insert2) apply (metis Suc_n_not_le_n) apply (metis le_trans linorder_linear) @@ -325,21 +327,21 @@ Inj [intro,simp] : "X \ H ==> X \ analz H" | Fst: "{|X,Y|} \ analz H ==> X \ analz H" | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" - | Decrypt [dest]: + | Decrypt [dest]: "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" text{*Monotonicity; Lemma 1 of Lowe's paper*} lemma analz_mono: "G\H ==> analz(G) \ analz(H)" apply auto -apply (erule analz.induct) -apply (auto dest: analz.Fst analz.Snd) +apply (erule analz.induct) +apply (auto dest: analz.Fst analz.Snd) done text{*Making it safe speeds up proofs*} lemma MPair_analz [elim!]: - "[| {|X,Y|} \ analz H; - [| X \ analz H; Y \ analz H |] ==> P + "[| {|X,Y|} \ analz H; + [| X \ analz H; Y \ analz H |] ==> P |] ==> P" by (blast dest: analz.Fst analz.Snd) @@ -376,7 +378,7 @@ apply (erule analz.induct, blast+) done -text{*Converse fails: we can analz more from the union than from the +text{*Converse fails: we can analz more from the union than from the separate parts, as a key in one might decrypt a message in the other*} lemma analz_Un: "analz(G) \ analz(H) \ analz(G \ H)" by (intro Un_least analz_mono Un_upper1 Un_upper2) @@ -390,39 +392,39 @@ lemma analz_insert_Agent [simp]: "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)" -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done lemma analz_insert_Nonce [simp]: "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)" -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done lemma analz_insert_Number [simp]: "analz (insert (Number N) H) = insert (Number N) (analz H)" -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done lemma analz_insert_Hash [simp]: "analz (insert (Hash X) H) = insert (Hash X) (analz H)" -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done text{*Can only pull out Keys if they are not needed to decrypt the rest*} -lemma analz_insert_Key [simp]: - "K \ keysFor (analz H) ==> +lemma analz_insert_Key [simp]: + "K \ keysFor (analz H) ==> analz (insert (Key K) H) = insert (Key K) (analz H)" apply (unfold keysFor_def) -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done lemma analz_insert_MPair [simp]: - "analz (insert {|X,Y|} H) = + "analz (insert {|X,Y|} H) = insert {|X,Y|} (analz (insert X (insert Y H)))" apply (rule equalityI) apply (rule subsetI) @@ -433,22 +435,22 @@ text{*Can pull out enCrypted message if the Key is not known*} lemma analz_insert_Crypt: - "Key (invKey K) \ analz H + "Key (invKey K) \ analz H ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)" -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done -lemma lemma1: "Key (invKey K) \ analz H ==> - analz (insert (Crypt K X) H) \ - insert (Crypt K X) (analz (insert X H))" +lemma lemma1: "Key (invKey K) \ analz H ==> + analz (insert (Crypt K X) H) \ + insert (Crypt K X) (analz (insert X H))" apply (rule subsetI) apply (erule_tac x = x in analz.induct, auto) done -lemma lemma2: "Key (invKey K) \ analz H ==> - insert (Crypt K X) (analz (insert X H)) \ +lemma lemma2: "Key (invKey K) \ analz H ==> + insert (Crypt K X) (analz (insert X H)) \ analz (insert (Crypt K X) H)" apply auto apply (erule_tac x = x in analz.induct, auto) @@ -456,26 +458,26 @@ done lemma analz_insert_Decrypt: - "Key (invKey K) \ analz H ==> - analz (insert (Crypt K X) H) = + "Key (invKey K) \ analz H ==> + analz (insert (Crypt K X) H) = insert (Crypt K X) (analz (insert X H))" by (intro equalityI lemma1 lemma2) text{*Case analysis: either the message is secure, or it is not! Effective, but can cause subgoals to blow up! Use with @{text "split_if"}; apparently @{text "split_tac"} does not cope with patterns such as @{term"analz (insert -(Crypt K X) H)"} *} +(Crypt K X) H)"} *} lemma analz_Crypt_if [simp]: - "analz (insert (Crypt K X) H) = - (if (Key (invKey K) \ analz H) - then insert (Crypt K X) (analz (insert X H)) + "analz (insert (Crypt K X) H) = + (if (Key (invKey K) \ analz H) + then insert (Crypt K X) (analz (insert X H)) else insert (Crypt K X) (analz H))" by (simp add: analz_insert_Crypt analz_insert_Decrypt) text{*This rule supposes "for the sake of argument" that we have the key.*} lemma analz_insert_Crypt_subset: - "analz (insert (Crypt K X) H) \ + "analz (insert (Crypt K X) H) \ insert (Crypt K X) (analz (insert X H))" apply (rule subsetI) apply (erule analz.induct, auto) @@ -498,8 +500,8 @@ lemma analz_subset_iff [simp]: "(analz G \ analz H) = (G \ analz H)" apply (rule iffI) -apply (iprover intro: subset_trans analz_increasing) -apply (frule analz_mono, simp) +apply (iprover intro: subset_trans analz_increasing) +apply (frule analz_mono, simp) done lemma analz_trans: "[| X\ analz G; G \ analz H |] ==> X\ analz H" @@ -525,7 +527,7 @@ text{*A congruence rule for "analz" *} lemma analz_subset_cong: - "[| analz G \ analz G'; analz H \ analz H' |] + "[| analz G \ analz G'; analz H \ analz H' |] ==> analz (G \ H) \ analz (G' \ H')" apply simp apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono) @@ -533,9 +535,9 @@ lemma analz_cong: - "[| analz G = analz G'; analz H = analz H' + "[| analz G = analz G'; analz H = analz H' |] ==> analz (G \ H) = analz (G' \ H')" -by (intro equalityI analz_subset_cong, simp_all) +by (intro equalityI analz_subset_cong, simp_all) lemma analz_insert_cong: "analz H = analz H' ==> analz(insert X H) = analz(insert X H')" @@ -579,9 +581,9 @@ text{*Monotonicity*} lemma synth_mono: "G\H ==> synth(G) \ synth(H)" - by (auto, erule synth.induct, auto) + by (auto, erule synth.induct, auto) -text{*NO @{text Agent_synth}, as any Agent name can be synthesized. +text{*NO @{text Agent_synth}, as any Agent name can be synthesized. The same holds for @{term Number}*} inductive_cases Nonce_synth [elim!]: "Nonce n \ synth H" inductive_cases Key_synth [elim!]: "Key K \ synth H" @@ -595,7 +597,7 @@ subsubsection{*Unions *} -text{*Converse fails: we can synth more from the union than from the +text{*Converse fails: we can synth more from the union than from the separate parts, building a compound message using elements of each.*} lemma synth_Un: "synth(G) \ synth(H) \ synth(G \ H)" by (intro Un_least synth_mono Un_upper1 Un_upper2) @@ -613,8 +615,8 @@ lemma synth_subset_iff [simp]: "(synth G \ synth H) = (G \ synth H)" apply (rule iffI) -apply (iprover intro: subset_trans synth_increasing) -apply (frule synth_mono, simp add: synth_idem) +apply (iprover intro: subset_trans synth_increasing) +apply (frule synth_mono, simp add: synth_idem) done lemma synth_trans: "[| X\ synth G; G \ synth H |] ==> X\ synth H" @@ -644,7 +646,7 @@ by blast -lemma keysFor_synth [simp]: +lemma keysFor_synth [simp]: "keysFor (synth H) = keysFor H \ invKey`{K. Key K \ H}" by (unfold keysFor_def, blast) @@ -706,7 +708,7 @@ qed lemma Fake_parts_insert: - "X \ synth (analz H) ==> + "X \ synth (analz H) ==> parts (insert X H) \ synth (analz H) \ parts H" proof - assume A1: "X \ synth (analz H)" @@ -735,11 +737,11 @@ qed lemma Fake_parts_insert_in_Un: - "[|Z \ parts (insert X H); X: synth (analz H)|] + "[|Z \ parts (insert X H); X: synth (analz H)|] ==> Z \ synth (analz H) \ parts H"; by (blast dest: Fake_parts_insert [THEN subsetD, dest]) -declare analz_mono [intro] synth_mono [intro] +declare analz_mono [intro] synth_mono [intro] lemma Fake_analz_insert: "X \ synth (analz G) ==> @@ -748,7 +750,7 @@ analz_mono analz_synth_Un insert_absorb) lemma Fake_analz_insert_simpler: - "X \ synth (analz G) ==> + "X \ synth (analz G) ==> analz (insert X H) \ synth (analz G) \ analz (G \ H)" apply (rule subsetI) apply (subgoal_tac "x \ analz (synth (analz G) \ H) ") diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Proxies.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:36:35 2011 +0200 @@ -0,0 +1,264 @@ +(* Title: HOL/Metis_Examples/Proxies.thy + Author: Jasmin Blanchette, TU Muenchen + +Example that exercises Metis's and Sledgehammer's logical symbol proxies for +rudimentary higher-order reasoning. +*) + +header {* +Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for +Rudimentary Higher-Order Reasoning. +*} + +theory Proxies +imports Type_Encodings +begin + +text {* Extensionality and set constants *} + +lemma plus_1_not_0: "n + (1\nat) \ 0" +by simp + +definition inc :: "nat \ nat" where +"inc x = x + 1" + +lemma "inc \ (\y. 0)" +sledgehammer [expect = some] (inc_def plus_1_not_0) +by (metis_eXhaust inc_def plus_1_not_0) + +lemma "inc = (\y. y + 1)" +sledgehammer [expect = some] (inc_def) +by (metis_eXhaust inc_def) + +definition add_swap :: "nat \ nat \ nat" where +"add_swap = (\x y. y + x)" + +lemma "add_swap m n = n + m" +sledgehammer [expect = some] (add_swap_def) +by (metis_eXhaust add_swap_def) + +definition "A = {xs\'a list. True}" + +lemma "xs \ A" +sledgehammer [expect = some] +by (metis_eXhaust A_def Collect_def mem_def) + +definition "B (y::int) \ y \ 0" +definition "C (y::int) \ y \ 1" + +lemma int_le_0_imp_le_1: "x \ (0::int) \ x \ 1" +by linarith + +lemma "B \ C" +sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some] +by (metis_eXhaust B_def C_def int_le_0_imp_le_1 predicate1I) + + +text {* Proxies for logical constants *} + +lemma "id (op =) x x" +sledgehammer [type_sys = erased, expect = none] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = none] (id_apply) (* unfortunate *) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metisX id_apply) + +lemma "id True" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "\ id False" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "x = id True \ x = id False" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id x = id True \ id x = id False" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "P True \ P False \ P x" +sledgehammer [type_sys = erased, expect = none] () +sledgehammer [type_sys = poly_args, expect = none] () +sledgehammer [type_sys = poly_tags?, expect = some] () +sledgehammer [type_sys = poly_tags, expect = some] () +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] () +sledgehammer [type_sys = mangled_tags?, expect = some] () +sledgehammer [type_sys = mangled_tags, expect = some] () +sledgehammer [type_sys = mangled_preds?, expect = some] () +sledgehammer [type_sys = mangled_preds, expect = some] () +by metisX + +lemma "id (\ a) \ \ id a" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id (\ \ a) \ id a" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id (\ (id (\ a))) \ id a" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id (a \ b) \ id a" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id (a \ b) \ id b" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id a \ id b \ id (a \ b)" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id a \ id (a \ b)" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id b \ id (a \ b)" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id (\ a) \ id (\ b) \ id (\ (a \ b))" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id (\ a) \ id (a \ b)" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +lemma "id (a \ b) \ id (\ a \ b)" +sledgehammer [type_sys = erased, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) +sledgehammer [type_sys = poly_tags, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) +sledgehammer [type_sys = poly_preds, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) +sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) +by (metis_eXhaust id_apply) + +end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/ROOT.ML --- a/src/HOL/Metis_Examples/ROOT.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Metis_Examples/ROOT.ML Mon Jun 06 20:36:35 2011 +0200 @@ -5,5 +5,5 @@ Testing Metis and Sledgehammer. *) -use_thys ["Abstraction", "BigO", "BT", "Clausify", "HO_Reas", "Message", - "Tarski", "TransClosure", "Typings", "set"]; +use_thys ["Abstraction", "Big_O", "Binary_Tree", "Clausification", "Message", + "Proxies", "Tarski", "Trans_Closure", "Sets"]; diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Sets.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Metis_Examples/Sets.thy Mon Jun 06 20:36:35 2011 +0200 @@ -0,0 +1,204 @@ +(* Title: HOL/Metis_Examples/Sets.thy + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + +Metis example featuring typed set theory. +*) + +header {* Metis Example Featuring Typed Set Theory *} + +theory Sets +imports Main +begin + +declare [[metis_new_skolemizer]] + +lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) & + (S(x,y) | ~S(y,z) | Q(Z,Z)) & + (Q(X,y) | ~Q(y,Z) | S(X,X))" +by metis + +lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" +by metis + +sledgehammer_params [isar_proof, isar_shrink_factor = 1] + +(*multiple versions of this example*) +lemma (*equal_union: *) + "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" +proof - + have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>1 \ x\<^isub>2" by (metis Un_commute Un_upper2) + have F2a: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 = x\<^isub>2 \ x\<^isub>1" by (metis Un_commute subset_Un_eq) + have F2: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis F2a subset_Un_eq) + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume AA1: "Y \ Z \ X" + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } + moreover + { assume AAA1: "Y \ X \ Y \ Z \ X" + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" + hence "Y \ Z \ X \ X \ Y \ Z" by (metis Un_subset_iff) + hence "Y \ Z \ X \ \ X \ Y \ Z" by (metis F2) + hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1) } + moreover + { assume "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } + moreover + { assume AAA1: "Y \ X \ Y \ Z \ X" + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" + hence "Y \ Z \ X \ X \ Y \ Z" by (metis Un_subset_iff) + hence "Y \ Z \ X \ \ X \ Y \ Z" by (metis F2) + hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by blast } + moreover + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by metis +qed + +sledgehammer_params [isar_proof, isar_shrink_factor = 2] + +lemma (*equal_union: *) + "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" +proof - + have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) + { assume AA1: "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" + { assume AAA1: "Y \ X \ Y \ Z \ X" + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume "Y \ Z \ X \ X \ Y \ Z" + hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1 Un_commute Un_upper2) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1 Un_subset_iff) } + moreover + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_subset_iff) } + moreover + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } + moreover + { assume AA1: "Y \ X \ Y \ Z \ X" + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume "Y \ Z \ X \ X \ Y \ Z" + hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1 Un_commute Un_upper2) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_subset_iff) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by metis +qed + +sledgehammer_params [isar_proof, isar_shrink_factor = 3] + +lemma (*equal_union: *) + "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" +proof - + have F1a: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 = x\<^isub>2 \ x\<^isub>1" by (metis Un_commute subset_Un_eq) + have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis F1a subset_Un_eq) + { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } + moreover + { assume AA1: "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" + { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) +qed + +sledgehammer_params [isar_proof, isar_shrink_factor = 4] + +lemma (*equal_union: *) + "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" +proof - + have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } + moreover + { assume AA1: "Y \ X \ Y \ Z \ X" + { assume "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_subset_iff Un_upper2) +qed + +sledgehammer_params [isar_proof, isar_shrink_factor = 1] + +lemma (*equal_union: *) + "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" +by (metis Un_least Un_upper1 Un_upper2 set_eq_subset) + +lemma "(X = Y \ Z) = (X \ Y \ X \ Z \ (\V. V \ Y \ V \ Z \ V \ X))" +by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym) + +lemma fixedpoint: "\!x. f (g x) = x \ \!y. g (f y) = y" +by metis + +lemma (* fixedpoint: *) "\!x. f (g x) = x \ \!y. g (f y) = y" +proof - + assume "\!x\'a. f (g x) = x" + thus "\!y\'b. g (f y) = y" by metis +qed + +lemma (* singleton_example_2: *) + "\x \ S. \S \ x \ \z. S \ {z}" +by (metis Set.subsetI Union_upper insertCI set_eq_subset) + +lemma (* singleton_example_2: *) + "\x \ S. \S \ x \ \z. S \ {z}" +by (metis Set.subsetI Union_upper insert_iff set_eq_subset) + +lemma singleton_example_2: + "\x \ S. \S \ x \ \z. S \ {z}" +proof - + assume "\x \ S. \S \ x" + hence "\x\<^isub>1. x\<^isub>1 \ \S \ x\<^isub>1 \ S \ x\<^isub>1 = \S" by (metis set_eq_subset) + hence "\x\<^isub>1. x\<^isub>1 \ S \ x\<^isub>1 = \S" by (metis Union_upper) + hence "\x\<^isub>1\('a \ bool) \ bool. \S \ x\<^isub>1 \ S \ x\<^isub>1" by (metis subsetI) + hence "\x\<^isub>1\('a \ bool) \ bool. S \ insert (\S) x\<^isub>1" by (metis insert_iff) + thus "\z. S \ {z}" by metis +qed + +text {* + From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages + 293-314. +*} + +(* Notes: (1) The numbering doesn't completely agree with the paper. + (2) We must rename set variables to avoid type clashes. *) +lemma "\B. (\x \ B. x \ (0::int))" + "D \ F \ \G. \A \ G. \B \ F. A \ B" + "P a \ \A. (\x \ A. P x) \ (\y. y \ A)" + "a < b \ b < (c::int) \ \B. a \ B \ b \ B \ c \ B" + "P (f b) \ \s A. (\x \ A. P x) \ f s \ A" + "P (f b) \ \s A. (\x \ A. P x) \ f s \ A" + "\A. a \ A" + "(\C. (0, 0) \ C \ (\x y. (x, y) \ C \ (Suc x, Suc y) \ C) \ (n, m) \ C) \ Q n \ Q m" + apply (metis all_not_in_conv) + apply (metis all_not_in_conv) + apply (metis mem_def) + apply (metis less_int_def singleton_iff) + apply (metis mem_def) + apply (metis mem_def) + apply (metis all_not_in_conv) +by (metis pair_in_Id_conv) + +end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Tarski.thy --- a/src/HOL/Metis_Examples/Tarski.thy Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Metis_Examples/Tarski.thy Mon Jun 06 20:36:35 2011 +0200 @@ -1,11 +1,11 @@ (* Title: HOL/Metis_Examples/Tarski.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen -Testing Metis. +Metis example featuring the full theorem of Tarski. *) -header {* The Full Theorem of Tarski *} +header {* Metis Example Featuring the Full Theorem of Tarski *} theory Tarski imports Main "~~/src/HOL/Library/FuncSet" @@ -260,7 +260,7 @@ by (simp add: dual_def) lemma (in PO) monotone_dual: - "monotone f (pset cl) (order cl) + "monotone f (pset cl) (order cl) ==> monotone f (pset (dual cl)) (order(dual cl))" by (simp add: monotone_def dualA_iff dualr_iff) @@ -436,7 +436,7 @@ lemma (in CLF) CLF_dual: "(dual cl, f) \ CLF_set" apply (simp del: dualA_iff) apply (simp) -done +done declare (in CLF) CLF_set_def[simp del] CL_dualCL[simp del] monotone_dual[simp del] dualA_iff[simp del] @@ -459,7 +459,7 @@ (*never proved, 2007-01-22*) declare [[ sledgehammer_problem_prefix = "Tarski__CLF_lubH_le_flubH" ]] - declare CL.lub_least[intro] CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] PO.transE[intro] PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] + declare CL.lub_least[intro] CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] PO.transE[intro] PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] lemma (in CLF) lubH_le_flubH: "H = {x. (x, f x) \ r & x \ A} ==> (lub H cl, f (lub H cl)) \ r" apply (rule lub_least, fast) @@ -480,15 +480,15 @@ apply (rule lub_upper, fast) apply assumption done - declare CL.lub_least[rule del] CLF.f_in_funcset[rule del] - funcset_mem[rule del] CL.lub_in_lattice[rule del] - PO.transE[rule del] PO.monotoneE[rule del] - CLF.monotone_f[rule del] CL.lub_upper[rule del] + declare CL.lub_least[rule del] CLF.f_in_funcset[rule del] + funcset_mem[rule del] CL.lub_in_lattice[rule del] + PO.transE[rule del] PO.monotoneE[rule del] + CLF.monotone_f[rule del] CL.lub_upper[rule del] (*never proved, 2007-01-22*) declare [[ sledgehammer_problem_prefix = "Tarski__CLF_flubH_le_lubH" ]] declare CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] - PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] + PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] CLF.lubH_le_flubH[simp] lemma (in CLF) flubH_le_lubH: "[| H = {x. (x, f x) \ r & x \ A} |] ==> (f (lub H cl), lub H cl) \ r" @@ -498,14 +498,14 @@ apply (rule conjI) using [[ sledgehammer_problem_prefix = "Tarski__CLF_flubH_le_lubH_simpler" ]] (*??no longer terminates, with combinators -apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2) +apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2) *) apply (metis CO_refl_on lubH_le_flubH monotoneE [OF monotone_f] refl_onD1 refl_onD2) apply (metis CO_refl_on lubH_le_flubH refl_onD2) done - declare CLF.f_in_funcset[rule del] funcset_mem[rule del] - CL.lub_in_lattice[rule del] PO.monotoneE[rule del] - CLF.monotone_f[rule del] CL.lub_upper[rule del] + declare CLF.f_in_funcset[rule del] funcset_mem[rule del] + CL.lub_in_lattice[rule del] PO.monotoneE[rule del] + CLF.monotone_f[rule del] CL.lub_upper[rule del] CLF.lubH_le_flubH[simp del] @@ -577,7 +577,7 @@ subsection {* Tarski fixpoint theorem 1, first part *} declare [[ sledgehammer_problem_prefix = "Tarski__CLF_T_thm_1_lub" ]] - declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro] + declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro] CLF.fixf_le_lubH[simp] CLF.lubH_least_fixf[simp] lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \ r & x \ A} cl" (*sledgehammer;*) @@ -585,7 +585,7 @@ apply (simp add: P_def) apply (rule lubI) using [[ sledgehammer_problem_prefix = "Tarski__CLF_T_thm_1_lub_simpler" ]] -apply (metis P_def fix_subset) +apply (metis P_def fix_subset) apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def) (*??no longer terminates, with combinators apply (metis P_def fix_def fixf_le_lubH) @@ -594,13 +594,13 @@ apply (simp add: fixf_le_lubH) apply (simp add: lubH_least_fixf) done - declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del] + declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del] CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del] (*never proved, 2007-01-22*) declare [[ sledgehammer_problem_prefix = "Tarski__CLF_glbH_is_fixp" ]] - declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro] + declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro] PO.dualPO[intro] CL.CL_dualCL[intro] PO.dualr_iff[simp] lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \ r & x \ A} ==> glb H cl \ P" -- {* Tarski for glb *} @@ -618,7 +618,7 @@ apply (rule CLF_dual) apply (simp add: dualr_iff dualA_iff) done - declare glb_dual_lub[simp del] PO.dualA_iff[rule del] CLF.lubH_is_fixp[rule del] + declare glb_dual_lub[simp del] PO.dualA_iff[rule del] CLF.lubH_is_fixp[rule del] PO.dualPO[rule del] CL.CL_dualCL[rule del] PO.dualr_iff[simp del] @@ -645,11 +645,11 @@ declare (in CLF) CO_refl_on[simp del] refl_on_def [simp del] declare [[ sledgehammer_problem_prefix = "Tarski__interval_subset" ]] - declare (in CLF) rel_imp_elem[intro] + declare (in CLF) rel_imp_elem[intro] declare interval_def [simp] lemma (in CLF) interval_subset: "[| a \ A; b \ A |] ==> interval r a b \ A" by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq) - declare (in CLF) rel_imp_elem[rule del] + declare (in CLF) rel_imp_elem[rule del] declare interval_def [simp del] @@ -682,7 +682,7 @@ declare [[ sledgehammer_problem_prefix = "Tarski__L_in_interval" ]] (*ALL THEOREMS*) lemma (in CLF) L_in_interval: "[| a \ A; b \ A; S \ interval r a b; - S \ {}; isLub S cl L; interval r a b \ {} |] ==> L \ interval r a b" + S \ {}; isLub S cl L; interval r a b \ {} |] ==> L \ interval r a b" (*WON'T TERMINATE apply (metis CO_trans intervalI interval_lemma1 interval_lemma2 isLub_least isLub_upper subset_empty subset_iff trans_def) *) @@ -807,7 +807,7 @@ (*sledgehammer; *) apply (simp add: Bot_def least_def) apply (rule_tac a="glb A cl" in someI2) -apply (simp_all add: glb_in_lattice glb_lower +apply (simp_all add: glb_in_lattice glb_lower r_def [symmetric] A_def [symmetric]) done @@ -827,14 +827,14 @@ apply (simp add: Top_def greatest_def) apply (rule_tac a="lub A cl" in someI2) apply (rule someI2) -apply (simp_all add: lub_in_lattice lub_upper +apply (simp_all add: lub_in_lattice lub_upper r_def [symmetric] A_def [symmetric]) done (*never proved, 2007-01-22*) -declare [[ sledgehammer_problem_prefix = "Tarski__Bot_prop" ]] (*ALL THEOREMS*) +declare [[ sledgehammer_problem_prefix = "Tarski__Bot_prop" ]] (*ALL THEOREMS*) lemma (in CLF) Bot_prop: "x \ A ==> (Bot cl, x) \ r" -(*sledgehammer*) +(*sledgehammer*) apply (simp add: Bot_dual_Top r_def) apply (rule dualr_iff [THEN subst]) apply (simp add: CLF.Top_prop [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] @@ -842,12 +842,12 @@ done declare [[ sledgehammer_problem_prefix = "Tarski__Bot_in_lattice" ]] (*ALL THEOREMS*) -lemma (in CLF) Top_intv_not_empty: "x \ A ==> interval r x (Top cl) \ {}" +lemma (in CLF) Top_intv_not_empty: "x \ A ==> interval r x (Top cl) \ {}" apply (metis Top_in_lattice Top_prop empty_iff intervalI reflE) done declare [[ sledgehammer_problem_prefix = "Tarski__Bot_intv_not_empty" ]] (*ALL THEOREMS*) -lemma (in CLF) Bot_intv_not_empty: "x \ A ==> interval r (Bot cl) x \ {}" +lemma (in CLF) Bot_intv_not_empty: "x \ A ==> interval r (Bot cl) x \ {}" apply (metis Bot_prop ex_in_conv intervalI reflE rel_imp_elem) done @@ -862,7 +862,7 @@ declare (in Tarski) P_def[simp] Y_ss [simp] declare fix_subset [intro] subset_trans [intro] lemma (in Tarski) Y_subset_A: "Y \ A" -(*sledgehammer*) +(*sledgehammer*) apply (rule subset_trans [OF _ fix_subset]) apply (rule Y_ss [simplified P_def]) done @@ -876,7 +876,7 @@ (*never proved, 2007-01-22*) declare [[ sledgehammer_problem_prefix = "Tarski__lubY_le_flubY" ]] (*ALL THEOREMS*) lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \ r" -(*sledgehammer*) +(*sledgehammer*) apply (rule lub_least) apply (rule Y_subset_A) apply (rule f_in_funcset [THEN funcset_mem]) @@ -900,7 +900,7 @@ (*first proved 2007-01-25 after relaxing relevance*) declare [[ sledgehammer_problem_prefix = "Tarski__intY1_subset" ]] (*ALL THEOREMS*) lemma (in Tarski) intY1_subset: "intY1 \ A" -(*sledgehammer*) +(*sledgehammer*) apply (unfold intY1_def) apply (rule interval_subset) apply (rule lubY_in_A) @@ -912,7 +912,7 @@ (*never proved, 2007-01-22*) declare [[ sledgehammer_problem_prefix = "Tarski__intY1_f_closed" ]] (*ALL THEOREMS*) lemma (in Tarski) intY1_f_closed: "x \ intY1 \ f x \ intY1" -(*sledgehammer*) +(*sledgehammer*) apply (simp add: intY1_def interval_def) apply (rule conjI) apply (rule transE) @@ -925,7 +925,7 @@ apply (rule lubY_in_A) apply (simp add: intY1_def interval_def intY1_elem) apply (simp add: intY1_def interval_def) --- {* @{text "(f x, Top cl) \ r"} *} +-- {* @{text "(f x, Top cl) \ r"} *} apply (rule Top_prop) apply (rule f_in_funcset [THEN funcset_mem]) apply (simp add: intY1_def interval_def intY1_elem) @@ -949,7 +949,7 @@ declare [[ sledgehammer_problem_prefix = "Tarski__intY1_is_cl" ]] (*ALL THEOREMS*) lemma (in Tarski) intY1_is_cl: "(| pset = intY1, order = induced intY1 r |) \ CompleteLattice" -(*sledgehammer*) +(*sledgehammer*) apply (unfold intY1_def) apply (rule interv_is_compl_latt) apply (rule lubY_in_A) @@ -961,7 +961,7 @@ (*never proved, 2007-01-22*) declare [[ sledgehammer_problem_prefix = "Tarski__v_in_P" ]] (*ALL THEOREMS*) lemma (in Tarski) v_in_P: "v \ P" -(*sledgehammer*) +(*sledgehammer*) apply (unfold P_def) apply (rule_tac A = "intY1" in fixf_subset) apply (rule intY1_subset) @@ -985,7 +985,7 @@ declare [[ sledgehammer_problem_prefix = "Tarski__fz_in_int_rel" ]] (*ALL THEOREMS*) lemma (in Tarski) f'z_in_int_rel: "[| z \ P; \y\Y. (y, z) \ induced P r |] - ==> ((%x: intY1. f x) z, z) \ induced intY1 r" + ==> ((%x: intY1. f x) z, z) \ induced intY1 r" apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval) done @@ -998,7 +998,7 @@ -- {* @{text "v \ P"} *} apply (simp add: v_in_P) apply (rule conjI) -(*sledgehammer*) +(*sledgehammer*) -- {* @{text v} is lub *} -- {* @{text "1. \y:Y. (y, v) \ induced P r"} *} apply (rule ballI) @@ -1021,12 +1021,12 @@ apply (unfold v_def) (*never proved, 2007-01-22*) using [[ sledgehammer_problem_prefix = "Tarski__tarski_full_lemma_simpler" ]] -(*sledgehammer*) +(*sledgehammer*) apply (rule indE) apply (rule_tac [2] intY1_subset) (*never proved, 2007-01-22*) using [[ sledgehammer_problem_prefix = "Tarski__tarski_full_lemma_simplest" ]] -(*sledgehammer*) +(*sledgehammer*) apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified]) apply (simp add: CL_imp_PO intY1_is_cl) apply force @@ -1049,12 +1049,12 @@ CompleteLatticeI_simp [intro] theorem (in CLF) Tarski_full: "(| pset = P, order = induced P r|) \ CompleteLattice" -(*sledgehammer*) +(*sledgehammer*) apply (rule CompleteLatticeI_simp) apply (rule fixf_po, clarify) (*never proved, 2007-01-22*) using [[ sledgehammer_problem_prefix = "Tarski__Tarski_full_simpler" ]] -(*sledgehammer*) +(*sledgehammer*) apply (simp add: P_def A_def r_def) apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl) diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/TransClosure.thy --- a/src/HOL/Metis_Examples/TransClosure.thy Mon Jun 06 20:36:35 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,64 +0,0 @@ -(* Title: HOL/Metis_Examples/TransClosure.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - -Testing Metis. -*) - -theory TransClosure -imports Main -begin - -declare [[metis_new_skolemizer]] - -type_synonym addr = nat - -datatype val - = Unit -- "dummy result value of void expressions" - | Null -- "null reference" - | Bool bool -- "Boolean value" - | Intg int -- "integer value" - | Addr addr -- "addresses of objects in the heap" - -consts R :: "(addr \ addr) set" - -consts f :: "addr \ val" - -lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b, c) \ R\<^sup>*\ - \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" -(* sledgehammer *) -proof - - assume A1: "f c = Intg x" - assume A2: "\y. f b = Intg y \ y \ x" - assume A3: "(a, b) \ R\<^sup>*" - assume A4: "(b, c) \ R\<^sup>*" - have F1: "f c \ f b" using A2 A1 by metis - have F2: "\u. (b, u) \ R \ (a, u) \ R\<^sup>*" using A3 by (metis transitive_closure_trans(6)) - have F3: "\x. (b, x b c R) \ R \ c = b" using A4 by (metis converse_rtranclE) - have "c \ b" using F1 by metis - hence "\u. (b, u) \ R" using F3 by metis - thus "\c. (b, c) \ R \ (a, c) \ R\<^sup>*" using F2 by metis -qed - -lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b,c) \ R\<^sup>*\ - \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" -(* sledgehammer [isar_proof, isar_shrink_factor = 2] *) -proof - - assume A1: "f c = Intg x" - assume A2: "\y. f b = Intg y \ y \ x" - assume A3: "(a, b) \ R\<^sup>*" - assume A4: "(b, c) \ R\<^sup>*" - have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def) - hence F1: "(a, b) \ R\<^sup>*" by (metis mem_def) - have "b \ c" using A1 A2 by metis - hence "\x\<^isub>1. (b, x\<^isub>1) \ R" using A4 by (metis converse_rtranclE) - thus "\c. (b, c) \ R \ (a, c) \ R\<^sup>*" using F1 by (metis transitive_closure_trans(6)) -qed - -lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b, c) \ R\<^sup>*\ - \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" -apply (erule_tac x = b in converse_rtranclE) - apply metis -by (metis transitive_closure_trans(6)) - -end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Trans_Closure.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy Mon Jun 06 20:36:35 2011 +0200 @@ -0,0 +1,66 @@ +(* Title: HOL/Metis_Examples/Trans_Closure.thy + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + +Metis example featuring the transitive closure. +*) + +header {* Metis Example Featuring the Transitive Closure *} + +theory Trans_Closure +imports Main +begin + +declare [[metis_new_skolemizer]] + +type_synonym addr = nat + +datatype val + = Unit -- "dummy result value of void expressions" + | Null -- "null reference" + | Bool bool -- "Boolean value" + | Intg int -- "integer value" + | Addr addr -- "addresses of objects in the heap" + +consts R :: "(addr \ addr) set" + +consts f :: "addr \ val" + +lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b, c) \ R\<^sup>*\ + \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" +(* sledgehammer *) +proof - + assume A1: "f c = Intg x" + assume A2: "\y. f b = Intg y \ y \ x" + assume A3: "(a, b) \ R\<^sup>*" + assume A4: "(b, c) \ R\<^sup>*" + have F1: "f c \ f b" using A2 A1 by metis + have F2: "\u. (b, u) \ R \ (a, u) \ R\<^sup>*" using A3 by (metis transitive_closure_trans(6)) + have F3: "\x. (b, x b c R) \ R \ c = b" using A4 by (metis converse_rtranclE) + have "c \ b" using F1 by metis + hence "\u. (b, u) \ R" using F3 by metis + thus "\c. (b, c) \ R \ (a, c) \ R\<^sup>*" using F2 by metis +qed + +lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b,c) \ R\<^sup>*\ + \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" +(* sledgehammer [isar_proof, isar_shrink_factor = 2] *) +proof - + assume A1: "f c = Intg x" + assume A2: "\y. f b = Intg y \ y \ x" + assume A3: "(a, b) \ R\<^sup>*" + assume A4: "(b, c) \ R\<^sup>*" + have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def) + hence F1: "(a, b) \ R\<^sup>*" by (metis mem_def) + have "b \ c" using A1 A2 by metis + hence "\x\<^isub>1. (b, x\<^isub>1) \ R" using A4 by (metis converse_rtranclE) + thus "\c. (b, c) \ R \ (a, c) \ R\<^sup>*" using F1 by (metis transitive_closure_trans(6)) +qed + +lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b, c) \ R\<^sup>*\ + \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" +apply (erule_tac x = b in converse_rtranclE) + apply metis +by (metis transitive_closure_trans(6)) + +end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Type_Encodings.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Mon Jun 06 20:36:35 2011 +0200 @@ -0,0 +1,86 @@ +(* Title: HOL/Metis_Examples/Type_Encodings.thy + Author: Jasmin Blanchette, TU Muenchen + +Example that exercises Metis's (and hence Sledgehammer's) type encodings. +*) + +header {* +Example that Exercises Metis's (and Hence Sledgehammer's) Type Encodings +*} + +theory Type_Encodings +imports Main +begin + +declare [[metis_new_skolemizer]] + +sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0] + + +text {* Setup for testing Metis exhaustively *} + +lemma fork: "P \ P \ P" by assumption + +ML {* +open ATP_Translate + +val polymorphisms = [Polymorphic, Monomorphic, Mangled_Monomorphic] +val levels = + [All_Types, Nonmonotonic_Types, Finite_Types, Const_Arg_Types, No_Types] +val heaviness = [Heavyweight, Lightweight] +val type_syss = + (levels |> map Simple_Types) @ + (map_product pair levels heaviness + (* The following two families of type systems are too incomplete for our + tests. *) + |> remove (op =) (Nonmonotonic_Types, Heavyweight) + |> remove (op =) (Finite_Types, Heavyweight) + |> map_product pair polymorphisms + |> map_product (fn constr => fn (poly, (level, heaviness)) => + constr (poly, level, heaviness)) + [Preds, Tags]) + +fun metis_eXhaust_tac ctxt ths = + let + fun tac [] st = all_tac st + | tac (type_sys :: type_syss) st = + st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *) + |> ((if null type_syss then all_tac else rtac @{thm fork} 1) + THEN Metis_Tactics.metisX_tac ctxt (SOME type_sys) ths 1 + THEN COND (has_fewer_prems 2) all_tac no_tac + THEN tac type_syss) + in tac end +*} + +method_setup metis_eXhaust = {* + Attrib.thms >> + (fn ths => fn ctxt => SIMPLE_METHOD (metis_eXhaust_tac ctxt ths type_syss)) +*} "exhaustively run the new Metis with all type encodings" + + +text {* Miscellaneous tests *} + +lemma "x = y \ y = x" +by metis_eXhaust + +lemma "[a] = [1 + 1] \ a = 1 + (1::int)" +by (metis_eXhaust last.simps) + +lemma "map Suc [0] = [Suc 0]" +by (metis_eXhaust map.simps) + +lemma "map Suc [1 + 1] = [Suc 2]" +by (metis_eXhaust map.simps nat_1_add_1) + +lemma "map Suc [2] = [Suc (1 + 1)]" +by (metis_eXhaust map.simps nat_1_add_1) + +definition "null xs = (xs = [])" + +lemma "P (null xs) \ null xs \ xs = []" +by (metis_eXhaust null_def) + +lemma "(0::nat) + 0 = 0" +by (metis_eXhaust arithmetic_simps(38)) + +end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Typings.thy --- a/src/HOL/Metis_Examples/Typings.thy Mon Jun 06 20:36:35 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,77 +0,0 @@ -(* Title: HOL/Metis_Examples/Typings.thy - Author: Jasmin Blanchette, TU Muenchen - -Testing the new Metis's (and hence Sledgehammer's) type translations. -*) - -theory Typings -imports Main -begin - -text {* Setup for testing Metis exhaustively *} - -lemma fork: "P \ P \ P" by assumption - -ML {* -open ATP_Translate - -val polymorphisms = [Polymorphic, Monomorphic, Mangled_Monomorphic] -val levels = - [All_Types, Nonmonotonic_Types, Finite_Types, Const_Arg_Types, No_Types] -val heaviness = [Heavyweight, Lightweight] -val type_syss = - (levels |> map Simple_Types) @ - (map_product pair levels heaviness - (* The following two families of type systems are too incomplete for our - tests. *) - |> remove (op =) (Nonmonotonic_Types, Heavyweight) - |> remove (op =) (Finite_Types, Heavyweight) - |> map_product pair polymorphisms - |> map_product (fn constr => fn (poly, (level, heaviness)) => - constr (poly, level, heaviness)) - [Preds, Tags]) - -fun metis_eXhaust_tac ctxt ths = - let - fun tac [] st = all_tac st - | tac (type_sys :: type_syss) st = - st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *) - |> ((if null type_syss then all_tac else rtac @{thm fork} 1) - THEN Metis_Tactics.metisX_tac ctxt (SOME type_sys) ths 1 - THEN COND (has_fewer_prems 2) all_tac no_tac - THEN tac type_syss) - in tac end -*} - -method_setup metis_eXhaust = {* - Attrib.thms >> - (fn ths => fn ctxt => SIMPLE_METHOD (metis_eXhaust_tac ctxt ths type_syss)) -*} "exhaustively run the new Metis with all type encodings" - - -text {* Metis tests *} - -lemma "x = y \ y = x" -by metis_eXhaust - -lemma "[a] = [1 + 1] \ a = 1 + (1::int)" -by (metis_eXhaust last.simps) - -lemma "map Suc [0] = [Suc 0]" -by (metis_eXhaust map.simps) - -lemma "map Suc [1 + 1] = [Suc 2]" -by (metis_eXhaust map.simps nat_1_add_1) - -lemma "map Suc [2] = [Suc (1 + 1)]" -by (metis_eXhaust map.simps nat_1_add_1) - -definition "null xs = (xs = [])" - -lemma "P (null xs) \ null xs \ xs = []" -by (metis_eXhaust null_def) - -lemma "(0::nat) + 0 = 0" -by (metis_eXhaust arithmetic_simps(38)) - -end diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/set.thy --- a/src/HOL/Metis_Examples/set.thy Mon Jun 06 20:36:35 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,202 +0,0 @@ -(* Title: HOL/Metis_Examples/set.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - -Testing Metis. -*) - -theory set -imports Main -begin - -declare [[metis_new_skolemizer]] - -lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) & - (S(x,y) | ~S(y,z) | Q(Z,Z)) & - (Q(X,y) | ~Q(y,Z) | S(X,X))" -by metis - -lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" -by metis - -sledgehammer_params [isar_proof, isar_shrink_factor = 1] - -(*multiple versions of this example*) -lemma (*equal_union: *) - "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" -proof - - have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>1 \ x\<^isub>2" by (metis Un_commute Un_upper2) - have F2a: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 = x\<^isub>2 \ x\<^isub>1" by (metis Un_commute subset_Un_eq) - have F2: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis F2a subset_Un_eq) - { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - moreover - { assume AA1: "Y \ Z \ X" - { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } - moreover - { assume AAA1: "Y \ X \ Y \ Z \ X" - { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - moreover - { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" - hence "Y \ Z \ X \ X \ Y \ Z" by (metis Un_subset_iff) - hence "Y \ Z \ X \ \ X \ Y \ Z" by (metis F2) - hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1) - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1) } - moreover - { assume "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" - { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } - moreover - { assume AAA1: "Y \ X \ Y \ Z \ X" - { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - moreover - { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" - hence "Y \ Z \ X \ X \ Y \ Z" by (metis Un_subset_iff) - hence "Y \ Z \ X \ \ X \ Y \ Z" by (metis F2) - hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1) - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by blast } - moreover - { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } - ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by metis -qed - -sledgehammer_params [isar_proof, isar_shrink_factor = 2] - -lemma (*equal_union: *) - "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" -proof - - have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) - { assume AA1: "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" - { assume AAA1: "Y \ X \ Y \ Z \ X" - { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - moreover - { assume "Y \ Z \ X \ X \ Y \ Z" - hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1 Un_commute Un_upper2) - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1 Un_subset_iff) } - moreover - { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_subset_iff) } - moreover - { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - moreover - { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } - moreover - { assume AA1: "Y \ X \ Y \ Z \ X" - { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - moreover - { assume "Y \ Z \ X \ X \ Y \ Z" - hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1 Un_commute Un_upper2) - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_subset_iff) } - ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by metis -qed - -sledgehammer_params [isar_proof, isar_shrink_factor = 3] - -lemma (*equal_union: *) - "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" -proof - - have F1a: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 = x\<^isub>2 \ x\<^isub>1" by (metis Un_commute subset_Un_eq) - have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis F1a subset_Un_eq) - { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } - moreover - { assume AA1: "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" - { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) } - ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) -qed - -sledgehammer_params [isar_proof, isar_shrink_factor = 4] - -lemma (*equal_union: *) - "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" -proof - - have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) - { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } - moreover - { assume AA1: "Y \ X \ Y \ Z \ X" - { assume "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) } - ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_subset_iff Un_upper2) -qed - -sledgehammer_params [isar_proof, isar_shrink_factor = 1] - -lemma (*equal_union: *) - "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" -by (metis Un_least Un_upper1 Un_upper2 set_eq_subset) - -lemma "(X = Y \ Z) = (X \ Y \ X \ Z \ (\V. V \ Y \ V \ Z \ V \ X))" -by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym) - -lemma fixedpoint: "\!x. f (g x) = x \ \!y. g (f y) = y" -by metis - -lemma (* fixedpoint: *) "\!x. f (g x) = x \ \!y. g (f y) = y" -proof - - assume "\!x\'a. f (g x) = x" - thus "\!y\'b. g (f y) = y" by metis -qed - -lemma (* singleton_example_2: *) - "\x \ S. \S \ x \ \z. S \ {z}" -by (metis Set.subsetI Union_upper insertCI set_eq_subset) - -lemma (* singleton_example_2: *) - "\x \ S. \S \ x \ \z. S \ {z}" -by (metis Set.subsetI Union_upper insert_iff set_eq_subset) - -lemma singleton_example_2: - "\x \ S. \S \ x \ \z. S \ {z}" -proof - - assume "\x \ S. \S \ x" - hence "\x\<^isub>1. x\<^isub>1 \ \S \ x\<^isub>1 \ S \ x\<^isub>1 = \S" by (metis set_eq_subset) - hence "\x\<^isub>1. x\<^isub>1 \ S \ x\<^isub>1 = \S" by (metis Union_upper) - hence "\x\<^isub>1\('a \ bool) \ bool. \S \ x\<^isub>1 \ S \ x\<^isub>1" by (metis subsetI) - hence "\x\<^isub>1\('a \ bool) \ bool. S \ insert (\S) x\<^isub>1" by (metis insert_iff) - thus "\z. S \ {z}" by metis -qed - -text {* - From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages - 293-314. -*} - -(* Notes: (1) The numbering doesn't completely agree with the paper. - (2) We must rename set variables to avoid type clashes. *) -lemma "\B. (\x \ B. x \ (0::int))" - "D \ F \ \G. \A \ G. \B \ F. A \ B" - "P a \ \A. (\x \ A. P x) \ (\y. y \ A)" - "a < b \ b < (c::int) \ \B. a \ B \ b \ B \ c \ B" - "P (f b) \ \s A. (\x \ A. P x) \ f s \ A" - "P (f b) \ \s A. (\x \ A. P x) \ f s \ A" - "\A. a \ A" - "(\C. (0, 0) \ C \ (\x y. (x, y) \ C \ (Suc x, Suc y) \ C) \ (n, m) \ C) \ Q n \ Q m" - apply (metis all_not_in_conv) - apply (metis all_not_in_conv) - apply (metis mem_def) - apply (metis less_int_def singleton_iff) - apply (metis mem_def) - apply (metis mem_def) - apply (metis all_not_in_conv) -by (metis pair_in_Id_conv) - -end