Commit 2ea84390 by nipkow

### tuned set comprehensions

parent 814978743f4e
 ... ... @@ -1113,8 +1113,8 @@ subsection "The Transformation" let ?fin="(Inv ys' xs'') \ (Inv ys' xs')" have ttt: "{(x,y)|x y. (x,y)\(Inv ys' xs'') \ (Inv ys' xs') \ y = (q)} \ {(x,y)|x y. (x,y)\(Inv ys' xs'') \ (Inv ys' xs') have ttt: "{(x,y). (x,y)\(Inv ys' xs'') \ (Inv ys' xs') \ y = (q)} \ {(x,y). (x,y)\(Inv ys' xs'') \ (Inv ys' xs') \ y \ (q)} = (Inv ys' xs'') \ (Inv ys' xs')" (is "?split1 \ ?split2 = ?easy") by auto have interem: "?split1 \ ?split2 = {}" by auto have split1subs: "?split1 \ ?fin" by auto ... ... @@ -1178,7 +1178,8 @@ subsection "The Transformation" thm setsum_my2[OF split1easy] thm setsum_my2[OF split2easy] also have E4: "\ = (\(x,y)\?split1. (-1::real) ) + (\(x,y)\?split2. 0)" by(simp only: split_def setsum_my2[OF split1easy] setsum_my2[OF split2easy]) + (\(x,y)\?split2. 0)" using setsum_my2[OF split1easy]setsum_my2[OF split2easy] by(simp only: split_def) also have "\ = (\(x,y)\?split1. (-1::real) )" by auto also have E5: "\ = - card ?split1 " by auto also have E6: "\ = - I " using cardsp1isI by auto ... ... @@ -1230,8 +1231,8 @@ subsection "The Transformation" let ?fin="(Inv ys' xs'') \ (Inv ys xs')" have ttt: "{(x,y)|x y. (x,y)\(Inv ys' xs'') \ (Inv ys xs') \ y = (q)} \ {(x,y)|x y. (x,y)\(Inv ys' xs'') \ (Inv ys xs') have ttt: "{(x,y). (x,y)\(Inv ys' xs'') \ (Inv ys xs') \ y = (q)} \ {(x,y). (x,y)\(Inv ys' xs'') \ (Inv ys xs') \ y \ (q)} = (Inv ys' xs'') \ (Inv ys xs')" (is "?split1 \ ?split2 = ?easy") by auto have interem: "?split1 \ ?split2 = {}" by auto have split1subs: "?split1 \ ?fin" by auto ... ... @@ -1271,7 +1272,7 @@ subsection "The Transformation" apply(simp only: interem) by auto thm setsum_my2[OF split2easy] also have "\ = (\(x,y)\?split1. (1::real) ) + (\(x,y)\?split2. 0)" by (simp only: split_def setsum_my2[OF split1easy] setsum_my2[OF split2easy]) + (\(x,y)\?split2. 0)" using setsum_my2[OF split1easy] setsum_my2[OF split2easy] by (simp only: split_def) also have "\ = (\(x,y)\?split1. (1::real) )" by auto also have "\ = card ?split1" by auto also have "\ = (0::real)" apply(simp only: split1empty) by auto ... ... @@ -1279,8 +1280,8 @@ subsection "The Transformation" (* abschätzung für B *) have ttt2: "{(x,y)|x y. (x,y)\(Inv ys xs') - (Inv ys' xs'') \ y = (q)} \ {(x,y)|x y. (x,y)\(Inv ys xs') - (Inv ys' xs'') have ttt2: "{(x,y). (x,y)\(Inv ys xs') - (Inv ys' xs'') \ y = (q)} \ {(x,y). (x,y)\(Inv ys xs') - (Inv ys' xs'') \ y \ (q)} = (Inv ys xs') - (Inv ys' xs'')" (is "?split1 \ ?split2 = ?easy2") by auto have interem: "?split1 \ ?split2 = {}" by auto have split1subs: "?split1 \ ?easy2" by auto ... ... @@ -1313,7 +1314,8 @@ subsection "The Transformation" apply(simp only: interem) by auto thm setsum_my2[OF split1easy2] also have "\ = (\(x,y)\?split1. 1) + (\(x,y)\?split2. (if b!(index init y) then 2::real else 1))" by (simp only: setsum_my2[OF split1easy2] split_def) + (\(x,y)\?split2. (if b!(index init y) then 2::real else 1))" using setsum_my2[OF split1easy2] by (simp only: split_def) also have "\ = card ?split1 + (\(x,y)\?split2. (if b!(index init y) then 2::real else 1))" by auto also have "\ = I ... ...
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!