Require Arith.
Require axioms.

Section jsize_lemmas.

Hint jsize : temp := Constructors jsize.

Definition jsize_of [T:type] : nat :=
  Cases T of 
    (fromjavatype (fromsimple jlong)) => (8)
  | (fromjavatype (fromsimple jdouble)) => (8)
  | _ => (4)
  end.

Lemma jsize_lemma : (T:type)(jsize T (jsize_of T)).
Proof.
Destruct T; Try (Compute; Constructor).
Destruct j; Try (Compute; Constructor).
Destruct j0; Try (Compute; Constructor).
Qed.

Lemma jsize_unique : (T:type)(SZ1,SZ2:nat)
  (jsize T SZ1) ->
  (jsize T SZ2) ->
  (SZ1 = SZ2).
Proof.
Intros until 1.
Inversion_clear H; Intro; Inversion_clear H; Reflexivity.
Qed.

Lemma jsize4or8 : (T:type)
  (jsize T (4)) \/ (jsize T (8)).
Proof.
Destruct T; Auto with temp.
Destruct j; Auto with temp.
Destruct j0; Auto with temp.
Qed.

Lemma jsize_of4or8 : (P:nat->Prop)(T:type)
  (P (4)) ->
  (P (8)) ->
  (P (jsize_of T)).
Proof.
Intros.
NewDestruct (jsize4or8 T).
  Rewrite (jsize_unique ? ? ? (jsize_lemma T) H1).
  Assumption.

  Rewrite (jsize_unique ? ? ? (jsize_lemma T) H1).
  Assumption.
Qed.

End jsize_lemmas.


Tactic Definition Rewrite_4or8 SZ :=
  Match Context With [ JSZ : (jsize ?1 SZ) |- ? ]
    -> Elim (jsize4or8 ?1); Intro JSZ_spec;
       Rewrite (jsize_unique ? ? ? JSZ JSZ_spec).