Re: [Rodin-b-sharp-user] prove that image is not bigger then pre-image

[Matthias S. <Mat...@in...>]

Hi Alexei,

it took me a moment to figure out the details.

I finally proved
 > ! p, f. finite(f) =>  card(f[p]) <= card(f)
in Isabelle. The details are rather unwieldy -- I had to make an 
induction over f. So if you don't mind using Isabelle, you can export 
the proof obligation and prove it there.

Maybe it is also possible to carry out the induction in Rodin. I don't 
have the time to find out.

Best,
Matthias

P.s.: My Isabelle proof (rather quick and dirty):

theory test imports EventB begin

lemma card_Image:
assumes
"finite r"
shows "card (r `` A) ≤ card r"
using assms
proof (induct r rule: finite.induct)
   case emptyI thus ?case by auto
next
   case (insertI r x) thus ?case
   proof (induct "x ∈ r")
     case True
     hence "insert x r = r" by blast
     with True show ?case by simp
   next
     case False
     from `finite r` have "finite (Range r)" by (rule finite_Range)
     moreover have "r `` A ⊆ Range r" by auto
     ultimately have "finite (r `` A)" by (rule rev_finite_subset)
     hence "card (insert x r `` A) ≤ card (r `` A) + 1"
       apply (cases x)
       apply (case_tac "a ∈ A")
       apply (case_tac "b ∈ r `` A")
       by (auto simp add: insert_absorb)
     with False show ?case by simp
   qed
qed

lemma
"T ∀^ p f. bfinite f↑ ^⟶^ bcard (brelimg f↑ p↑) .≤. bcard f↑"
proof (ebsimp, safe)
   fix p :: "'a set" and f :: "('a × 'b) set"
   assume "finite f"
   hence "finite (Range f)" by (rule finite_Range)
   moreover have "f `` p ⊆ Range f" by auto
   ultimately show "finite (f `` p)" by (rule rev_finite_subset)
next
   fix p :: "'a set" and f :: "('a × 'b) set"
   assume "finite f"
   hence "card (f `` p) ≤ card f" by (rule card_Image)
   thus "int (card (f `` p)) ≤ int (card f)" by auto
qed

end

Am 03.11.2011 12:16, schrieb Alexei Iliasov:
> Hi fellow Rodin users,
>
> I am stuck the following innocuous looking condition
>
> ! p, f. f : NAT +->  NAT&  finite(f)&  p<:NAT =>  card(f[p])<= card(f)
>
> If anybody could give hints on how this may be proven (or why it cannot
> be) I would be very grateful.
>
> Best regards,
> Alexei
>
> ------------------------------------------------------------------------------
> RSA(R) Conference 2012
> Save $700 by Nov 18
> Register now
> http://p.sf.net/sfu/rsa-sfdev2dev1
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user