changeset 41836 | c9d788ff7940 |
parent 41807 | ab5d2d81f9fb |
child 41839 | 421a795cee05 |
41835:9712fae15200 | 41836:c9d788ff7940 |
---|---|
33 next |
33 next |
34 assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y" |
34 assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y" |
35 then obtain "x" and "y" where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+ |
35 then obtain "x" and "y" where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+ |
36 from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast |
36 from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast |
37 with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast |
37 with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast |
38 qed |
|
39 |
|
40 (* generate a list from i to j*) |
|
41 consts iupt :: "int \<times> int \<Rightarrow> int list" |
|
42 recdef iupt "measure (\<lambda> (i,j). nat (j-i +1))" |
|
43 "iupt (i,j) = (if j <i then [] else (i# iupt(i+1, j)))" |
|
44 |
|
45 lemma iupt_set: "set (iupt(i,j)) = {i .. j}" |
|
46 proof(induct rule: iupt.induct) |
|
47 case (1 a b) |
|
48 show ?case |
|
49 using 1 by (simp add: simp_from_to) |
|
50 qed |
38 qed |
51 |
39 |
52 lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)" |
40 lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)" |
53 using Nat.gr0_conv_Suc |
41 using Nat.gr0_conv_Suc |
54 by clarsimp |
42 by clarsimp |
3536 in map (\<lambda> ((p,n,t),(q,m,s)). (And p q, n+m, Add t s)) [(a,b). a\<leftarrow>acs,b\<leftarrow>bcs])" |
3524 in map (\<lambda> ((p,n,t),(q,m,s)). (And p q, n+m, Add t s)) [(a,b). a\<leftarrow>acs,b\<leftarrow>bcs])" |
3537 "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))" |
3525 "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))" |
3538 "rsplit0 (Neg a) = map (\<lambda> (p,n,s). (p,-n,Neg s)) (rsplit0 a)" |
3526 "rsplit0 (Neg a) = map (\<lambda> (p,n,s). (p,-n,Neg s)) (rsplit0 a)" |
3539 "rsplit0 (Floor a) = foldl (op @) [] (map |
3527 "rsplit0 (Floor a) = foldl (op @) [] (map |
3540 (\<lambda> (p,n,s). if n=0 then [(p,0,Floor s)] |
3528 (\<lambda> (p,n,s). if n=0 then [(p,0,Floor s)] |
3541 else (map (\<lambda> j. (fp p n s j, 0, Add (Floor s) (C j))) (if n > 0 then iupt (0,n) else iupt(n,0)))) |
3529 else (map (\<lambda> j. (fp p n s j, 0, Add (Floor s) (C j))) (if n > 0 then [0 .. n] else [n .. 0]))) |
3542 (rsplit0 a))" |
3530 (rsplit0 a))" |
3543 "rsplit0 (CN 0 c a) = map (\<lambda> (p,n,s). (p,n+c,s)) (rsplit0 a)" |
3531 "rsplit0 (CN 0 c a) = map (\<lambda> (p,n,s). (p,n+c,s)) (rsplit0 a)" |
3544 "rsplit0 (CN m c a) = map (\<lambda> (p,n,s). (p,n,CN m c s)) (rsplit0 a)" |
3532 "rsplit0 (CN m c a) = map (\<lambda> (p,n,s). (p,n,CN m c s)) (rsplit0 a)" |
3545 "rsplit0 (CF c t s) = rsplit0 (Add (Mul c (Floor t)) s)" |
3533 "rsplit0 (CF c t s) = rsplit0 (Add (Mul c (Floor t)) s)" |
3546 "rsplit0 (Mul c a) = map (\<lambda> (p,n,s). (p,c*n,Mul c s)) (rsplit0 a)" |
3534 "rsplit0 (Mul c a) = map (\<lambda> (p,n,s). (p,c*n,Mul c s)) (rsplit0 a)" |
3560 (is "\<forall> (p,n,s) \<in> ?SS t. (?I p \<longrightarrow> ?N t = ?N (CN 0 n s)) \<and> _ \<and> _ ") |
3548 (is "\<forall> (p,n,s) \<in> ?SS t. (?I p \<longrightarrow> ?N t = ?N (CN 0 n s)) \<and> _ \<and> _ ") |
3561 proof(induct t rule: rsplit0.induct) |
3549 proof(induct t rule: rsplit0.induct) |
3562 case (5 a) |
3550 case (5 a) |
3563 let ?p = "\<lambda> (p,n,s) j. fp p n s j" |
3551 let ?p = "\<lambda> (p,n,s) j. fp p n s j" |
3564 let ?f = "(\<lambda> (p,n,s) j. (?p (p,n,s) j, (0::int),Add (Floor s) (C j)))" |
3552 let ?f = "(\<lambda> (p,n,s) j. (?p (p,n,s) j, (0::int),Add (Floor s) (C j)))" |
3565 let ?J = "\<lambda> n. if n>0 then iupt (0,n) else iupt (n,0)" |
3553 let ?J = "\<lambda> n. if n>0 then [0..n] else [n..0]" |
3566 let ?ff=" (\<lambda> (p,n,s). if n= 0 then [(p,0,Floor s)] else map (?f (p,n,s)) (?J n))" |
3554 let ?ff=" (\<lambda> (p,n,s). if n= 0 then [(p,0,Floor s)] else map (?f (p,n,s)) (?J n))" |
3567 have int_cases: "\<forall> (i::int). i= 0 \<or> i < 0 \<or> i > 0" by arith |
3555 have int_cases: "\<forall> (i::int). i= 0 \<or> i < 0 \<or> i > 0" by arith |
3568 have U1: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = |
3556 have U1: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = |
3569 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)]))" by auto |
3557 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)]))" by auto |
3570 have U2': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0}. |
3558 have U2': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0}. |
3571 ?ff (p,n,s) = map (?f(p,n,s)) (iupt(0,n))" by auto |
3559 ?ff (p,n,s) = map (?f(p,n,s)) [0..n]" by auto |
3572 hence U2: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = |
3560 hence U2: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = |
3573 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). |
3561 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). |
3574 set (map (?f(p,n,s)) (iupt(0,n)))))" |
3562 set (map (?f(p,n,s)) [0..n])))" |
3575 proof- |
3563 proof- |
3576 fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g |
3564 fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g |
3577 assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c" |
3565 assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c" |
3578 thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))" |
3566 thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))" |
3579 by (auto simp add: split_def) |
3567 by (auto simp add: split_def) |
3580 qed |
3568 qed |
3581 have U3': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0}. ?ff (p,n,s) = map (?f(p,n,s)) (iupt(n,0))" |
3569 have U3': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0}. ?ff (p,n,s) = map (?f(p,n,s)) [n..0]" |
3582 by auto |
3570 by auto |
3583 hence U3: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = |
3571 hence U3: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = |
3584 (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n<0} (\<lambda>(p,n,s). set (map (?f(p,n,s)) (iupt(n,0)))))" |
3572 (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n<0} (\<lambda>(p,n,s). set (map (?f(p,n,s)) [n..0])))" |
3585 proof- |
3573 proof- |
3586 fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g |
3574 fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g |
3587 assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c" |
3575 assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c" |
3588 thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))" |
3576 thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))" |
3589 by (auto simp add: split_def) |
3577 by (auto simp add: split_def) |
3590 qed |
3578 qed |
3591 have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" |
3579 have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" |
3592 by (auto simp add: foldl_conv_concat simp del: iupt.simps) |
3580 by (auto simp add: foldl_conv_concat) |
3593 also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast |
3581 also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast |
3594 also have "\<dots> = |
3582 also have "\<dots> = |
3595 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un |
3583 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un |
3596 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un |
3584 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un |
3597 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))))" |
3585 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))))" |
3598 using int_cases[rule_format] by blast |
3586 using int_cases[rule_format] by blast |
3599 also have "\<dots> = |
3587 also have "\<dots> = |
3600 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un |
3588 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un |
3601 (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n>0} (\<lambda>(p,n,s). set(map(?f(p,n,s)) (iupt(0,n))))) Un |
3589 (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n>0} (\<lambda>(p,n,s). set(map(?f(p,n,s)) [0..n]))) Un |
3602 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). |
3590 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). |
3603 set (map (?f(p,n,s)) (iupt(n,0))))))" by (simp only: U1 U2 U3) |
3591 set (map (?f(p,n,s)) [n..0]))))" by (simp only: U1 U2 U3) |
3604 also have "\<dots> = |
3592 also have "\<dots> = |
3605 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un |
3593 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un |
3606 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un |
3594 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un |
3607 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {n .. 0})))" |
3595 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {n .. 0})))" |
3608 by (simp only: set_map iupt_set set.simps) |
3596 by (simp only: set_map set_upto set.simps) |
3609 also have "\<dots> = |
3597 also have "\<dots> = |
3610 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un |
3598 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un |
3611 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un |
3599 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un |
3612 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast |
3600 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast |
3613 finally |
3601 finally |
3721 ultimately show ?case by blast |
3709 ultimately show ?case by blast |
3722 next |
3710 next |
3723 case (5 a) |
3711 case (5 a) |
3724 let ?p = "\<lambda> (p,n,s) j. fp p n s j" |
3712 let ?p = "\<lambda> (p,n,s) j. fp p n s j" |
3725 let ?f = "(\<lambda> (p,n,s) j. (?p (p,n,s) j, (0::int),(Add (Floor s) (C j))))" |
3713 let ?f = "(\<lambda> (p,n,s) j. (?p (p,n,s) j, (0::int),(Add (Floor s) (C j))))" |
3726 let ?J = "\<lambda> n. if n>0 then iupt (0,n) else iupt (n,0)" |
3714 let ?J = "\<lambda> n. if n>0 then [0..n] else [n..0]" |
3727 let ?ff=" (\<lambda> (p,n,s). if n= 0 then [(p,0,Floor s)] else map (?f (p,n,s)) (?J n))" |
3715 let ?ff=" (\<lambda> (p,n,s). if n= 0 then [(p,0,Floor s)] else map (?f (p,n,s)) (?J n))" |
3728 have int_cases: "\<forall> (i::int). i= 0 \<or> i < 0 \<or> i > 0" by arith |
3716 have int_cases: "\<forall> (i::int). i= 0 \<or> i < 0 \<or> i > 0" by arith |
3729 have U1: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)]))" by auto |
3717 have U1: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)]))" by auto |
3730 have U2': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0}. ?ff (p,n,s) = map (?f(p,n,s)) (iupt(0,n))" |
3718 have U2': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0}. ?ff (p,n,s) = map (?f(p,n,s)) [0..n]" |
3731 by auto |
3719 by auto |
3732 hence U2: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) (iupt(0,n)))))" |
3720 hence U2: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [0..n])))" |
3733 proof- |
3721 proof- |
3734 fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g |
3722 fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g |
3735 assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c" |
3723 assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c" |
3736 thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))" |
3724 thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))" |
3737 by (auto simp add: split_def) |
3725 by (auto simp add: split_def) |
3738 qed |
3726 qed |
3739 have U3': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0}. ?ff (p,n,s) = map (?f(p,n,s)) (iupt(n,0))" |
3727 have U3': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0}. ?ff (p,n,s) = map (?f(p,n,s)) [n..0]" |
3740 by auto |
3728 by auto |
3741 hence U3: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) (iupt(n,0)))))" |
3729 hence U3: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [n..0])))" |
3742 proof- |
3730 proof- |
3743 fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g |
3731 fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g |
3744 assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c" |
3732 assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c" |
3745 thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))" |
3733 thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))" |
3746 by (auto simp add: split_def) |
3734 by (auto simp add: split_def) |
3747 qed |
3735 qed |
3748 |
3736 |
3749 have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat simp del: iupt.simps) |
3737 have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat) |
3750 also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast |
3738 also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast |
3751 also have "\<dots> = |
3739 also have "\<dots> = |
3752 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un |
3740 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un |
3753 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un |
3741 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un |
3754 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))))" |
3742 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))))" |
3755 using int_cases[rule_format] by blast |
3743 using int_cases[rule_format] by blast |
3756 also have "\<dots> = |
3744 also have "\<dots> = |
3757 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un |
3745 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un |
3758 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) (iupt(0,n))))) Un |
3746 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [0..n]))) Un |
3759 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) (iupt(n,0))))))" by (simp only: U1 U2 U3) |
3747 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [n..0]))))" by (simp only: U1 U2 U3) |
3760 also have "\<dots> = |
3748 also have "\<dots> = |
3761 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un |
3749 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un |
3762 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un |
3750 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un |
3763 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {n .. 0})))" |
3751 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {n .. 0})))" |
3764 by (simp only: set_map iupt_set set.simps) |
3752 by (simp only: set_map set_upto set.simps) |
3765 also have "\<dots> = |
3753 also have "\<dots> = |
3766 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un |
3754 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un |
3767 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un |
3755 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un |
3768 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast |
3756 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast |
3769 finally |
3757 finally |
4021 qed |
4009 qed |
4022 |
4010 |
4023 definition |
4011 definition |
4024 DVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" |
4012 DVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" |
4025 where |
4013 where |
4026 DVDJ_def: "DVDJ i n s = (foldr disj (map (\<lambda> j. conj (Eq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) F)" |
4014 DVDJ_def: "DVDJ i n s = (foldr disj (map (\<lambda> j. conj (Eq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))) [0..n - 1]) F)" |
4027 |
4015 |
4028 definition |
4016 definition |
4029 NDVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" |
4017 NDVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" |
4030 where |
4018 where |
4031 NDVDJ_def: "NDVDJ i n s = (foldr conj (map (\<lambda> j. disj (NEq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) T)" |
4019 NDVDJ_def: "NDVDJ i n s = (foldr conj (map (\<lambda> j. disj (NEq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor (Neg s))))) [0..n - 1]) T)" |
4032 |
4020 |
4033 lemma DVDJ_DVD: |
4021 lemma DVDJ_DVD: |
4034 assumes xp:"x\<ge> 0" and x1: "x < 1" and np:"real n > 0" |
4022 assumes xp:"x\<ge> 0" and x1: "x < 1" and np:"real n > 0" |
4035 shows "Ifm (x#bs) (DVDJ i n s) = Ifm (x#bs) (Dvd i (CN 0 n s))" |
4023 shows "Ifm (x#bs) (DVDJ i n s) = Ifm (x#bs) (Dvd i (CN 0 n s))" |
4036 proof- |
4024 proof- |
4037 let ?f = "\<lambda> j. conj (Eq(CN 0 n (Add s (Sub(Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))" |
4025 let ?f = "\<lambda> j. conj (Eq(CN 0 n (Add s (Sub(Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))" |
4038 let ?s= "Inum (x#bs) s" |
4026 let ?s= "Inum (x#bs) s" |
4039 from foldr_disj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"] |
4027 from foldr_disj_map[where xs="[0..n - 1]" and bs="x#bs" and f="?f"] |
4040 have "Ifm (x#bs) (DVDJ i n s) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" |
4028 have "Ifm (x#bs) (DVDJ i n s) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" |
4041 by (simp add: iupt_set np DVDJ_def del: iupt.simps) |
4029 by (simp add: np DVDJ_def) |
4042 also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_minus[symmetric]) |
4030 also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_minus[symmetric]) |
4043 also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] |
4031 also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] |
4044 have "\<dots> = (real i rdvd real n * x - (-?s))" by simp |
4032 have "\<dots> = (real i rdvd real n * x - (-?s))" by simp |
4045 finally show ?thesis by simp |
4033 finally show ?thesis by simp |
4046 qed |
4034 qed |
4049 assumes xp:"x\<ge> 0" and x1: "x < 1" and np:"real n > 0" |
4037 assumes xp:"x\<ge> 0" and x1: "x < 1" and np:"real n > 0" |
4050 shows "Ifm (x#bs) (NDVDJ i n s) = Ifm (x#bs) (NDvd i (CN 0 n s))" |
4038 shows "Ifm (x#bs) (NDVDJ i n s) = Ifm (x#bs) (NDvd i (CN 0 n s))" |
4051 proof- |
4039 proof- |
4052 let ?f = "\<lambda> j. disj(NEq(CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor(Neg s))))" |
4040 let ?f = "\<lambda> j. disj(NEq(CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor(Neg s))))" |
4053 let ?s= "Inum (x#bs) s" |
4041 let ?s= "Inum (x#bs) s" |
4054 from foldr_conj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"] |
4042 from foldr_conj_map[where xs="[0..n - 1]" and bs="x#bs" and f="?f"] |
4055 have "Ifm (x#bs) (NDVDJ i n s) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" |
4043 have "Ifm (x#bs) (NDVDJ i n s) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" |
4056 by (simp add: iupt_set np NDVDJ_def del: iupt.simps) |
4044 by (simp add: np NDVDJ_def) |
4057 also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_minus[symmetric]) |
4045 also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_minus[symmetric]) |
4058 also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] |
4046 also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] |
4059 have "\<dots> = (\<not> (real i rdvd real n * x - (-?s)))" by simp |
4047 have "\<dots> = (\<not> (real i rdvd real n * x - (-?s)))" by simp |
4060 finally show ?thesis by simp |
4048 finally show ?thesis by simp |
4061 qed |
4049 qed |
5420 qed |
5408 qed |
5421 (* Cooper's Algorithm *) |
5409 (* Cooper's Algorithm *) |
5422 |
5410 |
5423 definition cooper :: "fm \<Rightarrow> fm" where |
5411 definition cooper :: "fm \<Rightarrow> fm" where |
5424 "cooper p \<equiv> |
5412 "cooper p \<equiv> |
5425 (let (q,B,d) = unit p; js = iupt (1,d); |
5413 (let (q,B,d) = unit p; js = [1..d]; |
5426 mq = simpfm (minusinf q); |
5414 mq = simpfm (minusinf q); |
5427 md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) js |
5415 md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) js |
5428 in if md = T then T else |
5416 in if md = T then T else |
5429 (let qd = evaldjf (\<lambda> t. simpfm (subst0 t q)) |
5417 (let qd = evaldjf (\<lambda> t. simpfm (subst0 t q)) |
5430 (remdups (map (\<lambda> (b,j). simpnum (Add b (C j))) |
5418 (remdups (map (\<lambda> (b,j). simpnum (Add b (C j))) |
5437 |
5425 |
5438 let ?I = "\<lambda> (x::int) p. Ifm (real x#bs) p" |
5426 let ?I = "\<lambda> (x::int) p. Ifm (real x#bs) p" |
5439 let ?q = "fst (unit p)" |
5427 let ?q = "fst (unit p)" |
5440 let ?B = "fst (snd(unit p))" |
5428 let ?B = "fst (snd(unit p))" |
5441 let ?d = "snd (snd (unit p))" |
5429 let ?d = "snd (snd (unit p))" |
5442 let ?js = "iupt (1,?d)" |
5430 let ?js = "[1..?d]" |
5443 let ?mq = "minusinf ?q" |
5431 let ?mq = "minusinf ?q" |
5444 let ?smq = "simpfm ?mq" |
5432 let ?smq = "simpfm ?mq" |
5445 let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js" |
5433 let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js" |
5446 fix i |
5434 fix i |
5447 let ?N = "\<lambda> t. Inum (real (i::int)#bs) t" |
5435 let ?N = "\<lambda> t. Inum (real (i::int)#bs) t" |
5474 from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp |
5462 from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp |
5475 from mdb qdb |
5463 from mdb qdb |
5476 have mdqdb: "bound0 (disj ?md ?qd)" by (simp only: disj_def, cases "?md=T \<or> ?qd=T", simp_all) |
5464 have mdqdb: "bound0 (disj ?md ?qd)" by (simp only: disj_def, cases "?md=T \<or> ?qd=T", simp_all) |
5477 from trans [OF pq_ex cp_thm'[OF lq uq dd dp]] B |
5465 from trans [OF pq_ex cp_thm'[OF lq uq dd dp]] B |
5478 have "?lhs = (\<exists> j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists> b\<in> ?N ` set ?B. Ifm ((b+ real j)#bs) ?q))" by auto |
5466 have "?lhs = (\<exists> j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists> b\<in> ?N ` set ?B. Ifm ((b+ real j)#bs) ?q))" by auto |
5479 also have "\<dots> = ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> (b,j) \<in> (?N ` set ?B \<times> set ?js). Ifm ((b+ real j)#bs) ?q))" apply (simp only: iupt_set simpfm) by auto |
5467 also have "\<dots> = ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> (b,j) \<in> (?N ` set ?B \<times> set ?js). Ifm ((b+ real j)#bs) ?q))" by auto |
5480 also have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> (\<lambda> (b,j). ?N (Add b (C j))) ` set ?bjs. Ifm (t #bs) ?q))" by simp |
5468 also have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> (\<lambda> (b,j). ?N (Add b (C j))) ` set ?bjs. Ifm (t #bs) ?q))" by simp |
5481 also have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> (\<lambda> (b,j). ?N (simpnum (Add b (C j)))) ` set ?bjs. Ifm (t #bs) ?q))" by (simp only: simpnum_ci) |
5469 also have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> (\<lambda> (b,j). ?N (simpnum (Add b (C j)))) ` set ?bjs. Ifm (t #bs) ?q))" by (simp only: simpnum_ci) |
5482 also have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> set ?sbjs. Ifm (?N t #bs) ?q))" |
5470 also have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> set ?sbjs. Ifm (?N t #bs) ?q))" |
5483 by (auto simp add: split_def) |
5471 by (auto simp add: split_def) |
5484 also have "\<dots> = ((\<exists> j\<in> set ?js. (\<lambda> j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or> (\<exists> t \<in> set (remdups ?sbjs). (\<lambda> t. ?I i (simpfm (subst0 t ?q))) t))" by (simp only: simpfm subst0_I[OF qfq] simpfm Inum.simps subst0_I[OF qfmq] set_remdups) |
5472 also have "\<dots> = ((\<exists> j\<in> set ?js. (\<lambda> j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or> (\<exists> t \<in> set (remdups ?sbjs). (\<lambda> t. ?I i (simpfm (subst0 t ?q))) t))" by (simp only: simpfm subst0_I[OF qfq] simpfm Inum.simps subst0_I[OF qfmq] set_remdups) |
5623 } |
5611 } |
5624 ultimately show ?thes by blast |
5612 ultimately show ?thes by blast |
5625 qed |
5613 qed |
5626 |
5614 |
5627 definition stage :: "fm \<Rightarrow> int \<Rightarrow> (num \<times> int) \<Rightarrow> fm" where |
5615 definition stage :: "fm \<Rightarrow> int \<Rightarrow> (num \<times> int) \<Rightarrow> fm" where |
5628 "stage p d \<equiv> (\<lambda> (e,c). evaldjf (\<lambda> j. simpfm (\<sigma> p c (Add e (C j)))) (iupt (1,c*d)))" |
5616 "stage p d \<equiv> (\<lambda> (e,c). evaldjf (\<lambda> j. simpfm (\<sigma> p c (Add e (C j)))) [1..c*d])" |
5629 lemma stage: |
5617 lemma stage: |
5630 shows "Ifm bs (stage p d (e,c)) = (\<exists> j\<in>{1 .. c*d}. Ifm bs (\<sigma> p c (Add e (C j))))" |
5618 shows "Ifm bs (stage p d (e,c)) = (\<exists> j\<in>{1 .. c*d}. Ifm bs (\<sigma> p c (Add e (C j))))" |
5631 by (unfold stage_def split_def ,simp only: evaldjf_ex iupt_set simpfm) simp |
5619 by (unfold stage_def split_def ,simp only: evaldjf_ex simpfm) simp |
5632 |
5620 |
5633 lemma stage_nb: assumes lp: "iszlfm p (a#bs)" and cp: "c >0" and nb:"numbound0 e" |
5621 lemma stage_nb: assumes lp: "iszlfm p (a#bs)" and cp: "c >0" and nb:"numbound0 e" |
5634 shows "bound0 (stage p d (e,c))" |
5622 shows "bound0 (stage p d (e,c))" |
5635 proof- |
5623 proof- |
5636 let ?f = "\<lambda> j. simpfm (\<sigma> p c (Add e (C j)))" |
5624 let ?f = "\<lambda> j. simpfm (\<sigma> p c (Add e (C j)))" |
5637 have th: "\<forall> j\<in> set (iupt(1,c*d)). bound0 (?f j)" |
5625 have th: "\<forall> j\<in> set [1..c*d]. bound0 (?f j)" |
5638 proof |
5626 proof |
5639 fix j |
5627 fix j |
5640 from nb have nb':"numbound0 (Add e (C j))" by simp |
5628 from nb have nb':"numbound0 (Add e (C j))" by simp |
5641 from simpfm_bound0[OF \<sigma>_nb[OF lp nb', where k="c"]] |
5629 from simpfm_bound0[OF \<sigma>_nb[OF lp nb', where k="c"]] |
5642 show "bound0 (simpfm (\<sigma> p c (Add e (C j))))" . |
5630 show "bound0 (simpfm (\<sigma> p c (Add e (C j))))" . |
5646 |
5634 |
5647 definition redlove :: "fm \<Rightarrow> fm" where |
5635 definition redlove :: "fm \<Rightarrow> fm" where |
5648 "redlove p \<equiv> |
5636 "redlove p \<equiv> |
5649 (let (q,B,d) = chooset p; |
5637 (let (q,B,d) = chooset p; |
5650 mq = simpfm (minusinf q); |
5638 mq = simpfm (minusinf q); |
5651 md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) (iupt (1,d)) |
5639 md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) [1..d] |
5652 in if md = T then T else |
5640 in if md = T then T else |
5653 (let qd = evaldjf (stage q d) B |
5641 (let qd = evaldjf (stage q d) B |
5654 in decr (disj md qd)))" |
5642 in decr (disj md qd)))" |
5655 |
5643 |
5656 lemma redlove: assumes qf: "qfree p" |
5644 lemma redlove: assumes qf: "qfree p" |
5660 |
5648 |
5661 let ?I = "\<lambda> (x::int) p. Ifm (real x#bs) p" |
5649 let ?I = "\<lambda> (x::int) p. Ifm (real x#bs) p" |
5662 let ?q = "fst (chooset p)" |
5650 let ?q = "fst (chooset p)" |
5663 let ?B = "fst (snd(chooset p))" |
5651 let ?B = "fst (snd(chooset p))" |
5664 let ?d = "snd (snd (chooset p))" |
5652 let ?d = "snd (snd (chooset p))" |
5665 let ?js = "iupt (1,?d)" |
5653 let ?js = "[1..?d]" |
5666 let ?mq = "minusinf ?q" |
5654 let ?mq = "minusinf ?q" |
5667 let ?smq = "simpfm ?mq" |
5655 let ?smq = "simpfm ?mq" |
5668 let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js" |
5656 let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js" |
5669 fix i |
5657 fix i |
5670 let ?N = "\<lambda> (t,k). (Inum (real (i::int)#bs) t,k)" |
5658 let ?N = "\<lambda> (t,k). (Inum (real (i::int)#bs) t,k)" |
5690 have "?lhs = ((\<exists> j\<in> {1.. ?d}. ?I j ?mq) \<or> (\<exists> (e,c)\<in> set ?B. \<exists> j\<in> {1 .. c*?d}. Ifm (real i#bs) (\<sigma> ?q c (Add e (C j)))))" by auto |
5678 have "?lhs = ((\<exists> j\<in> {1.. ?d}. ?I j ?mq) \<or> (\<exists> (e,c)\<in> set ?B. \<exists> j\<in> {1 .. c*?d}. Ifm (real i#bs) (\<sigma> ?q c (Add e (C j)))))" by auto |
5691 also have "\<dots> = ((\<exists> j\<in> {1.. ?d}. ?I j ?smq) \<or> (\<exists> (e,c)\<in> set ?B. ?I i (stage ?q ?d (e,c) )))" |
5679 also have "\<dots> = ((\<exists> j\<in> {1.. ?d}. ?I j ?smq) \<or> (\<exists> (e,c)\<in> set ?B. ?I i (stage ?q ?d (e,c) )))" |
5692 by (simp add: simpfm stage split_def) |
5680 by (simp add: simpfm stage split_def) |
5693 also have "\<dots> = ((\<exists> j\<in> {1 .. ?d}. ?I i (subst0 (C j) ?smq)) \<or> ?I i ?qd)" |
5681 also have "\<dots> = ((\<exists> j\<in> {1 .. ?d}. ?I i (subst0 (C j) ?smq)) \<or> ?I i ?qd)" |
5694 by (simp add: evaldjf_ex subst0_I[OF qfmq]) |
5682 by (simp add: evaldjf_ex subst0_I[OF qfmq]) |
5695 finally have mdqd:"?lhs = (?I i ?md \<or> ?I i ?qd)" by (simp only: evaldjf_ex iupt_set simpfm) |
5683 finally have mdqd:"?lhs = (?I i ?md \<or> ?I i ?qd)" by (simp only: evaldjf_ex set_upto simpfm) |
5696 also have "\<dots> = (?I i (disj ?md ?qd))" by (simp add: disj) |
5684 also have "\<dots> = (?I i (disj ?md ?qd))" by (simp add: disj) |
5697 also have "\<dots> = (Ifm bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb]) |
5685 also have "\<dots> = (Ifm bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb]) |
5698 finally have mdqd2: "?lhs = (Ifm bs (decr (disj ?md ?qd)))" . |
5686 finally have mdqd2: "?lhs = (Ifm bs (decr (disj ?md ?qd)))" . |
5699 {assume mdT: "?md = T" |
5687 {assume mdT: "?md = T" |
5700 hence cT:"redlove p = T" by (simp add: redlove_def Let_def chooset_def split_def) |
5688 hence cT:"redlove p = T" by (simp add: redlove_def Let_def chooset_def split_def) |