Require Arith.
Require machine.
Require axioms.

Section induction.


(* Mutual induction on ofType, ptr, ofmem *)

Scheme ofType_etc_ind := Minimality for ofType Sort Prop
with ptr_etc_ind := Minimality for ptr Sort Prop
with ofmem_etc_ind := Minimality for ofmem Sort Prop.

Lemma ofType_ptr_ofmem_simul_ind
     : (s:state'; P:(exp->type->Prop); P0:(exp->rorw->type->Prop);
        P1:(mem->Prop))
        ((E:exp)(P E jint))
        ->((E:exp)(P E jbyte))
        ->((E:exp)(P E jchar))
        ->((E:exp)(P E jshort))
        ->((E:exp)(P E jbool))
        ->((C:exp)(P Null (jinstof C)))
        ->((T:javatype)(P Null (jarray T)))
        ->((E,C,D:exp)
            (jextends C D)
            ->(ofType s E (jinstof C))
            ->(P E (jinstof C))
            ->(P E (jinstof D)))
        ->((E:exp; T:javatype)
            (ofType s E (jarray T))
            ->(P E (jarray T))
            ->(P E (jinstof _4java4lang6Object_C)))
        ->((M:mem; ADDR:exp; T:type; RO:rorw)
            (ptr s ADDR RO T)
            ->(P0 ADDR RO T)
            ->(jsize T (4))
            ->(ofmem s M)
            ->(P1 M)
            ->(P (sel4 M ADDR) T))
        ->((M:mem; ADDR:exp; T:type; RO:rorw)
            (ptr s ADDR RO T)
            ->(P0 ADDR RO T)
            ->(jsize T (8))
            ->(ofmem s M)
            ->(P1 M)
            ->(P (sel8 M ADDR) T))
        ->((E:exp)(given_jclassdesc E)->(P E jclassdesc))
        ->((h:exp; C:exp)
            (alloc_in repval h (jinstof C) (rep_of s))
            ->(P h (jinstof C)))
        ->((h:exp; T:javatype)
            (alloc_in repval h (jarray T) (rep_of s))
            ->(P h (jarray T)))
        ->((E,C:exp)
            (ofType s E (jinstof C))
            ->(P E (jinstof C))
            ->(nonnull E)
            ->(P0 E ro (jvirtab C)))
        ->((E,C:exp)
            (ofType s E (jvirtab C))
            ->(P E (jvirtab C))
            ->(P0 E ro jclassdesc))
        ->((OFF:nat; T:javatype; C,E:exp)
            (jifield C OFF T)
            ->(ofType s E (jinstof C))
            ->(P E (jinstof C))
            ->(nonnull E)
            ->(P0 (plus E OFF) rw T))
        ->((E,C:exp; OFF:nat; SIG:exp)
            (jvmethod C OFF SIG)
            ->(ofType s E (jvirtab C))
            ->(P E (jvirtab C))
            ->(P0 (plus E OFF) ro (jimplof SIG)))
        ->((A:exp; T:javatype)
            (ofType s A (jarray T))
            ->(P A (jarray T))
            ->(nonnull A)
            ->(P0 (plus A (4)) ro jint))
        ->((A:exp; T:javatype; SZ:nat; M:mem; IDX:nat)
            (ofType s A (jarray T))
            ->(P A (jarray T))
            ->(ofmem s M)
            ->(P1 M)
            ->(nonnull A)
            ->(jsize T SZ)
            ->(lt IDX (sel4 M (plus A (4))))
            ->(P0 (plus A (plus (mult IDX SZ) (8))) rw T))
        ->((E:exp; T:javatype)
            (ofType s E (jarray T))
            ->(P E (jarray T))
            ->(nonnull E)
            ->(P0 E ro (jvirtab _4java4lang6Object_C)))
        ->((E:exp; T:javatype)(given_staticptr E T)->(P0 E rw T))
        ->((h:exp; T:javasimpletype)
            (alloc_in repptr h T (rep_of s))->(P0 h rw T))
        ->((M:mem; ADDR,E:exp; T:type)
            (ptr s ADDR rw T)
            ->(P0 ADDR rw T)
            ->(jsize T (4))
            ->(ofType s E T)
            ->(P E T)
            ->(ofmem s M)
            ->(P1 M)
            ->(P1 (upd4 M ADDR E)))
        ->((M:mem; ADDR,E:exp; T:type)
            (ptr s ADDR rw T)
            ->(P0 ADDR rw T)
            ->(jsize T (8))
            ->(ofType s E T)
            ->(P E T)
            ->(ofmem s M)
            ->(P1 M)
            ->(P1 (upd8 M ADDR E)))
        ->(P1 (last_alloc_of s))
        ->
  (((e:exp; t:type)(ofType s e t)->(P e t))
    /\ ((e:exp; r:rorw; t:type)(ptr s e r t)->(P0 e r t))
    /\ ((m:mem)(ofmem s m)->(P1 m))).
Proof.
Intros.
Repeat Split.
  Intros.
  EApply ofType_etc_ind; EAuto.

  Intros.
  EApply ptr_etc_ind; EAuto.

  Intros.
  EApply ofmem_etc_ind; EAuto.
Qed.

End induction.