Theory Design_generated_generated

theory Design_generated_generated imports "../Toy_Library"   "../Toy_Library_Static" begin

(* 1 ************************************ 0 + 1 *)
text ‹
  For certain concepts like classes and class-types, only a generic
  definition for its resulting semantics can be given. Generic means,
  there is a function outside HOL that ``compiles'' a concrete,
  closed-world class diagram into a ``theory'' of this data model,
  consisting of a bunch of definitions for classes, accessors, method,
  casts, and tests for actual types, as well as proofs for the
  fundamental properties of these operations in this concrete data
  model. ›

(* 2 ************************************ 1 + 1 *)
text ‹
   Our data universe  consists in the concrete class diagram just of node's,
and implicitly of the class object. Each class implies the existence of a class
type defined for the corresponding object representations as follows: ›

(* 3 ************************************ 2 + 10 *)
datatype tyℰ𝒳𝒯Atom = mkℰ𝒳𝒯Atom "oid" "oid list option" "int option" "bool option" "nat option" "unit option"
datatype tyAtom = mkAtom "tyℰ𝒳𝒯Atom" "int option"
datatype tyℰ𝒳𝒯Molecule = mkℰ𝒳𝒯Molecule_Atom "tyAtom"
                        | mkℰ𝒳𝒯Molecule "oid" "oid list option" "int option" "bool option" "nat option" "unit option"
datatype tyMolecule = mkMolecule "tyℰ𝒳𝒯Molecule"
datatype tyℰ𝒳𝒯Person = mkℰ𝒳𝒯Person_Molecule "tyMolecule"
                        | mkℰ𝒳𝒯Person_Atom "tyAtom"
                        | mkℰ𝒳𝒯Person "oid" "nat option" "unit option"
datatype tyPerson = mkPerson "tyℰ𝒳𝒯Person" "oid list option" "int option" "bool option"
datatype tyℰ𝒳𝒯Galaxy = mkℰ𝒳𝒯Galaxy_Person "tyPerson"
                        | mkℰ𝒳𝒯Galaxy_Molecule "tyMolecule"
                        | mkℰ𝒳𝒯Galaxy_Atom "tyAtom"
                        | mkℰ𝒳𝒯Galaxy "oid"
datatype tyGalaxy = mkGalaxy "tyℰ𝒳𝒯Galaxy" "nat option" "unit option"
datatype tyℰ𝒳𝒯ToyAny = mkℰ𝒳𝒯ToyAny_Galaxy "tyGalaxy"
                        | mkℰ𝒳𝒯ToyAny_Person "tyPerson"
                        | mkℰ𝒳𝒯ToyAny_Molecule "tyMolecule"
                        | mkℰ𝒳𝒯ToyAny_Atom "tyAtom"
                        | mkℰ𝒳𝒯ToyAny "oid"
datatype tyToyAny = mkToyAny "tyℰ𝒳𝒯ToyAny"

(* 4 ************************************ 12 + 1 *)
text ‹
   Now, we construct a concrete ``universe of ToyAny types'' by injection into a
sum type containing the class types. This type of ToyAny will be used as instance
for all respective type-variables. ›

(* 5 ************************************ 13 + 1 *)
datatype 𝔄 = inAtom "tyAtom"
                        | inMolecule "tyMolecule"
                        | inPerson "tyPerson"
                        | inGalaxy "tyGalaxy"
                        | inToyAny "tyToyAny"

(* 6 ************************************ 14 + 1 *)
text ‹
   Having fixed the object universe, we can introduce type synonyms that exactly correspond
to Toy types. Again, we exploit that our representation of Toy is a ``shallow embedding'' with a
one-to-one correspondance of Toy-types to types of the meta-language HOL. ›

(* 7 ************************************ 15 + 5 *)
type_synonym Atom = "tyAtom"
type_synonym Molecule = "tyMolecule"
type_synonym Person = "tyPerson"
type_synonym Galaxy = "tyGalaxy"
type_synonym ToyAny = "tyToyAny"

(* 8 ************************************ 20 + 3 *)
definition "oidAtom_0___boss = 0"
definition "oidMolecule_0___boss = 0"
definition "oidPerson_0___boss = 0"

(* 9 ************************************ 23 + 2 *)
definition "switch2_01 = (λ [x0 , x1]  (x0 , x1))"
definition "switch2_10 = (λ [x0 , x1]  (x1 , x0))"

(* 10 ************************************ 25 + 3 *)
definition "oid1 = 1"
definition "oid2 = 2"
definition "inst_assoc1 = (λoid_class to_from oid. ((case (deref_assocs_list ((to_from::oid list list  oid list × oid list)) ((oid::oid)) ((drop ((((map_of_list ([(oidPerson_0___boss , (List.map ((λ(x , y). [x , y]) o switch2_01) ([[[oid1] , [oid2]]])))]))) ((oid_class::oid))))))) of Nil  None
    | l  (Some (l)))::oid list option))"

(* 11 ************************************ 28 + 0 *)

(* 12 ************************************ 28 + 2 *)
definition "oid3 = 3"
definition "inst_assoc3 = (λoid_class to_from oid. ((case (deref_assocs_list ((to_from::oid list list  oid list × oid list)) ((oid::oid)) ((drop ((((map_of_list ([]))) ((oid_class::oid))))))) of Nil  None
    | l  (Some (l)))::oid list option))"

(* 13 ************************************ 30 + 0 *)

(* 14 ************************************ 30 + 5 *)
definition "oid4 = 4"
definition "oid5 = 5"
definition "oid6 = 6"
definition "oid7 = 7"
definition "inst_assoc4 = (λoid_class to_from oid. ((case (deref_assocs_list ((to_from::oid list list  oid list × oid list)) ((oid::oid)) ((drop ((((map_of_list ([(oidPerson_0___boss , (List.map ((λ(x , y). [x , y]) o switch2_01) ([[[oid7] , [oid6]] , [[oid6] , [oid1]] , [[oid4] , [oid5]]])))]))) ((oid_class::oid))))))) of Nil  None
    | l  (Some (l)))::oid list option))"

(* 15 ************************************ 35 + 0 *)

(* 16 ************************************ 35 + 1 *)
locale state_σ1 =
fixes "oid4" :: "nat"
fixes "oid5" :: "nat"
fixes "oid6" :: "nat"
fixes "oid1" :: "nat"
fixes "oid7" :: "nat"
fixes "oid2" :: "nat"
assumes distinct_oid: "(distinct ([oid4 , oid5 , oid6 , oid1 , oid7 , oid2]))"
fixes "σ1_object0Person" :: "tyPerson"
fixes "σ1_object0" :: "Person"
assumes σ1_object0_def: "σ1_object0 = (λ_. σ1_object0Person)"
fixes "σ1_object1Person" :: "tyPerson"
fixes "σ1_object1" :: "Person"
assumes σ1_object1_def: "σ1_object1 = (λ_. σ1_object1Person)"
fixes "σ1_object2Person" :: "tyPerson"
fixes "σ1_object2" :: "Person"
assumes σ1_object2_def: "σ1_object2 = (λ_. σ1_object2Person)"
fixes "XPerson1Person" :: "tyPerson"
fixes "XPerson1" :: "Person"
assumes XPerson1_def: "XPerson1 = (λ_. XPerson1Person)"
fixes "σ1_object4Person" :: "tyPerson"
fixes "σ1_object4" :: "Person"
assumes σ1_object4_def: "σ1_object4 = (λ_. σ1_object4Person)"
fixes "XPerson2Person" :: "tyPerson"
fixes "XPerson2" :: "Person"
assumes XPerson2_def: "XPerson2 = (λ_. XPerson2Person)"
begin
definition "σ1 = (state.make ((Map.empty (oid4  (inPerson (σ1_object0Person)), oid5  (inPerson (σ1_object1Person)), oid6  (inPerson (σ1_object2Person)), oid1  (inPerson (XPerson1Person)), oid7  (inPerson (σ1_object4Person)), oid2  (inPerson (XPerson2Person))))) ((map_of_list ([(oidPerson_0___boss , (List.map ((λ(x , y). [x , y]) o switch2_01) ([[[oid4] , [oid2]] , [[oid6] , [oid4]] , [[oid1] , [oid6]] , [[oid7] , [oid3]]])))]))))"

lemma perm_σ1 : "σ1 = (state.make ((Map.empty (oid2  (inPerson (XPerson2Person)), oid7  (inPerson (σ1_object4Person)), oid1  (inPerson (XPerson1Person)), oid6  (inPerson (σ1_object2Person)), oid5  (inPerson (σ1_object1Person)), oid4  (inPerson (σ1_object0Person))))) ((assocs (σ1))))"
  apply(simp add: σ1_def)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (2) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (3) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (2) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (4) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (3) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (2) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (5) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (4) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (3) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (2) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
by(simp)
end

(* 17 ************************************ 36 + 1 *)
locale state_σ1' =
fixes "oid1" :: "nat"
fixes "oid2" :: "nat"
fixes "oid3" :: "nat"
assumes distinct_oid: "(distinct ([oid1 , oid2 , oid3]))"
fixes "XPerson1Person" :: "tyPerson"
fixes "XPerson1" :: "Person"
assumes XPerson1_def: "XPerson1 = (λ_. XPerson1Person)"
fixes "XPerson2Person" :: "tyPerson"
fixes "XPerson2" :: "Person"
assumes XPerson2_def: "XPerson2 = (λ_. XPerson2Person)"
fixes "XPerson3Person" :: "tyPerson"
fixes "XPerson3" :: "Person"
assumes XPerson3_def: "XPerson3 = (λ_. XPerson3Person)"
begin
definition "σ1' = (state.make ((Map.empty (oid1  (inPerson (XPerson1Person)), oid2  (inPerson (XPerson2Person)), oid3  (inPerson (XPerson3Person))))) ((map_of_list ([(oidPerson_0___boss , (List.map ((λ(x , y). [x , y]) o switch2_01) ([[[oid1] , [oid2]]])))]))))"

lemma perm_σ1' : "σ1' = (state.make ((Map.empty (oid3  (inPerson (XPerson3Person)), oid2  (inPerson (XPerson2Person)), oid1  (inPerson (XPerson1Person))))) ((assocs (σ1'))))"
  apply(simp add: σ1'_def)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (2) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
by(simp)
end

(* 18 ************************************ 37 + 1 *)
locale pre_post_σ11' =
fixes "oid1" :: "nat"
fixes "oid2" :: "nat"
fixes "oid3" :: "nat"
fixes "oid4" :: "nat"
fixes "oid5" :: "nat"
fixes "oid6" :: "nat"
fixes "oid7" :: "nat"
assumes distinct_oid: "(distinct ([oid1 , oid2 , oid3 , oid4 , oid5 , oid6 , oid7]))"
fixes "XPerson1Person" :: "tyPerson"
fixes "XPerson1" :: "Person"
assumes XPerson1_def: "XPerson1 = (λ_. XPerson1Person)"
fixes "XPerson2Person" :: "tyPerson"
fixes "XPerson2" :: "Person"
assumes XPerson2_def: "XPerson2 = (λ_. XPerson2Person)"
fixes "XPerson3Person" :: "tyPerson"
fixes "XPerson3" :: "Person"
assumes XPerson3_def: "XPerson3 = (λ_. XPerson3Person)"
fixes "σ1_object0Person" :: "tyPerson"
fixes "σ1_object0" :: "Person"
assumes σ1_object0_def: "σ1_object0 = (λ_. σ1_object0Person)"
fixes "σ1_object1Person" :: "tyPerson"
fixes "σ1_object1" :: "Person"
assumes σ1_object1_def: "σ1_object1 = (λ_. σ1_object1Person)"
fixes "σ1_object2Person" :: "tyPerson"
fixes "σ1_object2" :: "Person"
assumes σ1_object2_def: "σ1_object2 = (λ_. σ1_object2Person)"
fixes "σ1_object4Person" :: "tyPerson"
fixes "σ1_object4" :: "Person"
assumes σ1_object4_def: "σ1_object4 = (λ_. σ1_object4Person)"

assumes σ1: "(state_σ1 (oid4) (oid5) (oid6) (oid1) (oid7) (oid2) (σ1_object0Person) (σ1_object0) (σ1_object1Person) (σ1_object1) (σ1_object2Person) (σ1_object2) (XPerson1Person) (XPerson1) (σ1_object4Person) (σ1_object4) (XPerson2Person) (XPerson2))"

assumes σ1': "(state_σ1' (oid1) (oid2) (oid3) (XPerson1Person) (XPerson1) (XPerson2Person) (XPerson2) (XPerson3Person) (XPerson3))"
begin
interpretation state_σ1: state_σ1 "oid4" "oid5" "oid6" "oid1" "oid7" "oid2" "σ1_object0Person" "σ1_object0" "σ1_object1Person" "σ1_object1" "σ1_object2Person" "σ1_object2" "XPerson1Person" "XPerson1" "σ1_object4Person" "σ1_object4" "XPerson2Person" "XPerson2"
by(rule σ1)

interpretation state_σ1': state_σ1' "oid1" "oid2" "oid3" "XPerson1Person" "XPerson1" "XPerson2Person" "XPerson2" "XPerson3Person" "XPerson3"
by(rule σ1')

definition "heap_σ1 = (heap (state_σ11))"

definition "heap_σ1' = (heap (state_σ1'.σ1'))"
end

end