Theory Subtype

(*  Title:       Jive Data and Store Model
    Author:      Norbert Schirmer <schirmer at informatik.tu-muenchen.de>, 2003
    Maintainer:  Nicole Rauch <rauch at informatik.uni-kl.de>
    License:     LGPL
*)

section ‹Widening the Direct Subtype Relation›

theory Subtype
imports "../Isa_Counter/DirectSubtypes"
begin

text ‹
In this theory, we define the widening subtype relation of types and prove 
that it is a partial order.
›

subsection ‹Auxiliary lemmas›

text ‹These general lemmas are not especially related to Jive. 
They capture
some useful properties of general relations. 
›
lemma distinct_rtrancl_into_trancl:
  assumes neq_x_y: "x≠y"
  assumes x_y_rtrancl: "(x,y) ∈ r⇧*"
  shows "(x,y) ∈ r⇧+"
  using x_y_rtrancl neq_x_y
proof (induct)
  assume "x≠x" thus "(x, x) ∈ r⇧+" by simp
next
  fix y z
  assume x_y_rtrancl: "(x, y) ∈ r⇧*" 
  assume y_z_r: "(y, z) ∈ r" 
  assume "x ≠ y ⟹ (x, y) ∈ r⇧+" 
  assume "x ≠ z"
  from x_y_rtrancl
  show "(x, z) ∈ r⇧+"
  proof (cases)
    assume "x=y"
    with y_z_r have "(x,z) ∈ r" by simp
    thus "(x,z) ∈  r⇧+"..
  next
    fix w
    assume "(x, w) ∈ r⇧*"
    moreover assume "(w, y) ∈ r"
    ultimately have "(x,y) ∈ r⇧+"
      by (rule rtrancl_into_trancl1)
    from this y_z_r
    show "(x, z) ∈ r⇧+"..
  qed
qed

lemma acyclic_imp_antisym_rtrancl: "acyclic r ⟹ antisym (r⇧*)"
proof (clarsimp simp only: acyclic_def antisym_def)
  fix x y
  assume acyclic: "∀x. (x, x) ∉ r⇧+"
  assume x_y: "(x, y) ∈ r⇧*" 
  assume y_x: "(y, x) ∈ r⇧*"
  show "x=y"
  proof (cases "x=y")
    case True thus ?thesis .
  next
    case False
    from False x_y have "(x, y) ∈ r⇧+"
      by (rule distinct_rtrancl_into_trancl)
    also
    from False y_x have "(y, x) ∈ r⇧+"
      by (fastforce intro: distinct_rtrancl_into_trancl)
    finally have "(x,x) ∈ r⇧+".
    with acyclic show ?thesis by simp
  qed
qed

lemma acyclic_trancl_rtrancl: 
  assumes acyclic: "acyclic r"
  shows "(x,y) ∈ r⇧+ = ((x,y) ∈ r⇧* ∧ x≠y)"
proof
  assume x_y_trancl: "(x,y) ∈ r⇧+"
  show "(x,y) ∈ r⇧* ∧ x≠y"
  proof
    from x_y_trancl show "(x,y) ∈ r⇧*"..
  next
    from x_y_trancl acyclic show "x≠y" by (auto simp add: acyclic_def)
  qed
next
  assume "(x,y) ∈ r⇧* ∧ x≠y"
  thus "(x,y) ∈ r⇧+"
    by (auto intro: distinct_rtrancl_into_trancl)
qed


subsection ‹The Widening (Subtype) Relation of Javatypes›


text ‹\label{widening_subtypes}
In this section we widen the direct subtype relations specified in Sec. 
\ref{direct_subtype_relations}.
It is done by a calculation of the transitive closure of the 
direct subtype relation. 
›

text ‹This is the concrete syntax that expresses the subtype relations 
between all types. 
\label{subtype_relations_concrete_syntax}›

abbreviation
  direct_subtype_syntax :: "Javatype ⇒ Javatype ⇒ bool" ("_ ≺1 _" [71,71] 70)
where ― ‹direct subtype relation›
  "A ≺1 B == (A,B) ∈ direct_subtype"

abbreviation
  widen_syntax :: "Javatype ⇒ Javatype ⇒ bool" ("_ ≼ _" [71,71] 70)
where ― ‹reflexive transitive closure of direct subtype relation›
  "A ≼ B == (A,B) ∈ direct_subtype⇧*"

abbreviation
  widen_strict_syntax :: "Javatype ⇒ Javatype ⇒ bool" ("_ ≺ _" [71,71] 70)
where ― ‹transitive closure of direct subtype relation›
  "A ≺ B == (A,B) ∈ direct_subtype⇧+"


subsection ‹The Subtype Relation as Partial Order›

text ‹We prove the axioms required for partial orders, i.e.\ 
reflexivity, transitivity and antisymmetry, for the widened subtype
relation. The direct subtype relation has been
defined in Sec. \ref{direct_subtype_relations}.
The reflexivity lemma is
added to the Simplifier and to the Classical reasoner (via the
attribute iff), and the transitivity and antisymmetry lemmas
are made known as transitivity rules (via the attribute trans).
This way, these lemmas will be automatically used in subsequent proofs.
›

lemma acyclic_direct_subtype: "acyclic direct_subtype"
proof (clarsimp simp add: acyclic_def)
  fix x show "x ≺ x ⟹ False"
  by (cases x) (fastforce elim: tranclE simp add: direct_subtype_def)+
     (* takes a very long time to calculate *)
qed

lemma antisym_rtrancl_direct_subtype: "antisym (direct_subtype⇧*)"
using acyclic_direct_subtype by (rule acyclic_imp_antisym_rtrancl)

lemma widen_strict_to_widen: "C ≺ D = (C ≼ D ∧ C≠D)"
using acyclic_direct_subtype by (rule acyclic_trancl_rtrancl)

text ‹The widening relation on Javatype is reflexive.›

lemma widen_refl [iff]: "X ≼ X" ..

text ‹The widening relation on Javatype is transitive.›

lemma widen_trans [trans] : 
  assumes a_b: "a ≼ b"
  shows "⋀ c. b ≼ c ⟹ a ≼ c"
  by (insert a_b, rule rtrancl_trans)

text ‹The widening relation on Javatype is antisymmetric.›

lemma widen_antisym [trans]: 
  assumes a_b: "a ≼ b" 
  assumes b_c: "b ≼ a"  
  shows "a = b"
  using a_b b_c antisym_rtrancl_direct_subtype
  by (unfold antisym_def) blast


subsection ‹Javatype Ordering Properties›

text ‹The type class @{term ord} allows us to overwrite the two comparison 
operators $<$ and $\leq$.
  These are  the two comparison operators on @{typ Javatype} that we want
to use subsequently.›

text ‹We can also prove that @{typ Javatype} is in the type class @{term order}. 
For this we
  have to prove reflexivity, transitivity, antisymmetry and that $<$ and $\leq$ are 
defined in such
  a way that @{thm Orderings.order_less_le [no_vars]} holds. This proof can easily 
be achieved by using the
  lemmas proved above and the definition of @{term less_Javatype_def}.
›

instantiation Javatype:: order
begin

definition
  le_Javatype_def:   "A ≤ B ≡ A ≼ B"

definition
  less_Javatype_def: "A < B ≡ A ≤ B ∧ ¬ B ≤ (A::Javatype)"
  
instance proof
  fix x y z:: "Javatype"
  {
    show "x ≤ x"
      by (simp add: le_Javatype_def )
  next
    assume "x ≤ y" "y ≤ z"
    then show "x ≤ z"
      by (unfold le_Javatype_def) (rule rtrancl_trans) 
  next
    assume "x ≤ y" "y ≤ x" 
    then show "x = y"
      apply (unfold le_Javatype_def) 
      apply (rule widen_antisym) 
      apply assumption +
      done
  next
    show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
      by (simp add: less_Javatype_def)
  }
qed

end


subsection ‹Enhancing the Simplifier›

lemmas subtype_defs = le_Javatype_def less_Javatype_def
                      direct_subtype_def 
(*
                      direct_subtype
                      direct_subtype[THEN r_into_rtrancl]
*)
lemmas subtype_ok_simps = subtype_defs 
lemmas subtype_wrong_elims = rtranclE

text ‹During verification we will often have to solve the goal that one type
widens to the other. So we equip the simplifier with a special solver-tactic.
›

lemma widen_asm: "(a::Javatype) ≤ b ⟹ a ≤ b"
  by simp

lemmas direct_subtype_widened = direct_subtype[THEN r_into_rtrancl]

ML ‹
local val ss = simpset_of @{context} in

fun widen_tac ctxt =
  resolve_tac ctxt @{thms widen_asm} THEN'
  simp_tac (put_simpset ss ctxt addsimps @{thms le_Javatype_def}) THEN'
  Method.insert_tac ctxt @{thms direct_subtype_widened} THEN'
  simp_tac (put_simpset (simpset_of @{theory_context Transitive_Closure}) ctxt)

end
›

declaration ‹fn _ =>
  Simplifier.map_ss (fn ss => ss addSolver (mk_solver "widen" widen_tac))
›


text ‹In this solver-tactic, we first try the trivial resolution with ‹widen_asm› to
check if the actual subgaol really is a request to solve a subtyping problem.
If so, we unfold the comparison operator, insert the direct subtype
relations and call the simplifier.
›


subsection ‹Properties of the Subtype Relation›


text ‹The class ‹Object› has to be the root of the class hierarchy, 
i.e.~it is supertype of each concrete class, abstract class, interface
and array type.
  The proof scripts should run on every correctly generated type hierarchy.
›


lemma Object_root: "CClassT C ≤ CClassT Object"
  by (cases C, simp_all)

lemma Object_root_abs: "AClassT C ≤ CClassT Object"
  by (cases C, simp_all)

lemma Object_root_int: "InterfaceT C ≤ CClassT Object"
  by (cases C, simp_all)

lemma Object_root_array: "ArrT C ≤ CClassT Object"
  proof (cases C)
    fix x
    assume c: "C = CClassAT x"
    show "ArrT C ≤ CClassT Object"
      using c by (cases x, simp_all)
  next
    fix x
    assume c: "C = AClassAT x"
    show "ArrT C ≤ CClassT Object"
      using c by (cases x, simp_all)
  next
    fix x
    assume c: "C = InterfaceAT x"
    show "ArrT C ≤ CClassT Object"
      using c by (cases x, simp_all)
  next
    assume c: "C = BoolAT"
    show "ArrT C ≤ CClassT Object"
      using c by simp
  next
    assume c: "C = IntgAT"
    show "ArrT C ≤ CClassT Object"
      using c by simp
  next
    assume c: "C = ShortAT"
    show "ArrT C ≤ CClassT Object"
      using c by simp
  next
    assume c: "C = ByteAT"
    show "ArrT C ≤ CClassT Object"
      using c by simp
qed

text ‹If another type is (non-strict) supertype of Object, 
then it must be the type Object itself.›

lemma Object_rootD: 
  assumes p: "CClassT Object ≤ c"
  shows "CClassT Object = c"
  using p
  apply (cases c)
  apply (fastforce elim: subtype_wrong_elims simp add: subtype_defs) +
  ― ‹In this lemma, we only get contradictory cases except for Object itself.›
done

text ‹The type NullT has to be the leaf of each branch of the class
hierarchy, i.e.~it is subtype of each type.›

lemma NullT_leaf [simp]: "NullT ≤ CClassT C"
  by (cases C, simp_all)

lemma NullT_leaf_abs [simp]: "NullT ≤ AClassT C"
  by (cases C, simp_all)

lemma NullT_leaf_int [simp]: "NullT ≤ InterfaceT C"
  by (cases C, simp_all)

lemma NullT_leaf_array: "NullT ≤ ArrT C"
  proof (cases C)
    fix x
    assume c: "C = CClassAT x"
    show "NullT ≤ ArrT C"
      using c by (cases x, simp_all)
  next
    fix x
    assume c: "C = AClassAT x"
    show "NullT ≤ ArrT C"
      using c by (cases x, simp_all)
  next
    fix x
    assume c: "C = InterfaceAT x"
    show "NullT ≤ ArrT C"
      using c by (cases x, simp_all)
  next
    assume c: "C = BoolAT"
    show "NullT ≤ ArrT C"
      using c by simp
  next
    assume c: "C = IntgAT"
    show "NullT ≤ ArrT C"
      using c by simp
  next
    assume c: "C = ShortAT"
    show "NullT ≤ ArrT C"
      using c by simp
  next
    assume c: "C = ByteAT"
    show "NullT ≤ ArrT C"
      using c by simp
qed

end