Theory Design_generated

theory Design_generated imports "../Toy_Library"   "../Toy_Library_Static"   "../embedding/Generator_dynamic_sequential" 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ℰ𝒳𝒯⇩A⇩t⇩o⇩m = mkℰ𝒳𝒯⇩A⇩t⇩o⇩m "oid" "oid list option" "int option" "bool option" "nat option" "unit option"
datatype ty⇩A⇩t⇩o⇩m = mk⇩A⇩t⇩o⇩m "tyℰ𝒳𝒯⇩A⇩t⇩o⇩m" "int option"
datatype tyℰ𝒳𝒯⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e = mkℰ𝒳𝒯⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e_⇩A⇩t⇩o⇩m "ty⇩A⇩t⇩o⇩m"
                        | mkℰ𝒳𝒯⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "oid" "oid list option" "int option" "bool option" "nat option" "unit option"
datatype ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e = mk⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "tyℰ𝒳𝒯⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e"
datatype tyℰ𝒳𝒯⇩P⇩e⇩r⇩s⇩o⇩n = mkℰ𝒳𝒯⇩P⇩e⇩r⇩s⇩o⇩n_⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e"
                        | mkℰ𝒳𝒯⇩P⇩e⇩r⇩s⇩o⇩n_⇩A⇩t⇩o⇩m "ty⇩A⇩t⇩o⇩m"
                        | mkℰ𝒳𝒯⇩P⇩e⇩r⇩s⇩o⇩n "oid" "nat option" "unit option"
datatype ty⇩P⇩e⇩r⇩s⇩o⇩n = mk⇩P⇩e⇩r⇩s⇩o⇩n "tyℰ𝒳𝒯⇩P⇩e⇩r⇩s⇩o⇩n" "oid list option" "int option" "bool option"
datatype tyℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y = mkℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y_⇩P⇩e⇩r⇩s⇩o⇩n "ty⇩P⇩e⇩r⇩s⇩o⇩n"
                        | mkℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y_⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e"
                        | mkℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y_⇩A⇩t⇩o⇩m "ty⇩A⇩t⇩o⇩m"
                        | mkℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y "oid"
datatype ty⇩G⇩a⇩l⇩a⇩x⇩y = mk⇩G⇩a⇩l⇩a⇩x⇩y "tyℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y" "nat option" "unit option"
datatype tyℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y = mkℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y_⇩G⇩a⇩l⇩a⇩x⇩y "ty⇩G⇩a⇩l⇩a⇩x⇩y"
                        | mkℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y_⇩P⇩e⇩r⇩s⇩o⇩n "ty⇩P⇩e⇩r⇩s⇩o⇩n"
                        | mkℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y_⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e"
                        | mkℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y_⇩A⇩t⇩o⇩m "ty⇩A⇩t⇩o⇩m"
                        | mkℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y "oid"
datatype ty⇩T⇩o⇩y⇩A⇩n⇩y = mk⇩T⇩o⇩y⇩A⇩n⇩y "tyℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y"

(* 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 𝔄 = in⇩A⇩t⇩o⇩m "ty⇩A⇩t⇩o⇩m"
                        | in⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e"
                        | in⇩P⇩e⇩r⇩s⇩o⇩n "ty⇩P⇩e⇩r⇩s⇩o⇩n"
                        | in⇩G⇩a⇩l⇩a⇩x⇩y "ty⇩G⇩a⇩l⇩a⇩x⇩y"
                        | in⇩T⇩o⇩y⇩A⇩n⇩y "ty⇩T⇩o⇩y⇩A⇩n⇩y"

(* 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 = "⟨⟨ty⇩A⇩t⇩o⇩m⟩⇩⊥⟩⇩⊥"
type_synonym Molecule = "⟨⟨ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e⟩⇩⊥⟩⇩⊥"
type_synonym Person = "⟨⟨ty⇩P⇩e⇩r⇩s⇩o⇩n⟩⇩⊥⟩⇩⊥"
type_synonym Galaxy = "⟨⟨ty⇩G⇩a⇩l⇩a⇩x⇩y⟩⇩⊥⟩⇩⊥"
type_synonym ToyAny = "⟨⟨ty⇩T⇩o⇩y⇩A⇩n⇩y⟩⇩⊥⟩⇩⊥"

(* 8 ************************************ 20 + 3 *)
definition "oid⇩A⇩t⇩o⇩m_0___boss = 0"
definition "oid⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e_0___boss = 0"
definition "oid⇩P⇩e⇩r⇩s⇩o⇩n_0___boss = 0"

(* 9 ************************************ 23 + 2 *)
definition "switch⇩2_01 = (λ [x0 , x1] ⇒ (x0 , x1))"
definition "switch⇩2_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 ([(oid⇩P⇩e⇩r⇩s⇩o⇩n_0___boss , (List.map ((λ(x , y). [x , y]) o switch⇩2_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 + 4 *)
generation_syntax [ shallow (generation_semantics [ design ]) ]
setup ‹(Generation_mode.update_compiler_config ((K (let open META in Compiler_env_config_ext (true, NONE, Oids ((Code_Numeral.natural_of_integer 0), (Code_Numeral.natural_of_integer 1), (Code_Numeral.natural_of_integer 4)), I ((Code_Numeral.natural_of_integer 0), (Code_Numeral.natural_of_integer 0)), Gen_only_design, SOME (ToyClass ((META.SS_base (META.ST "ToyAny")), nil, uncurry cons (ToyClass ((META.SS_base (META.ST "Galaxy")), uncurry cons (I ((META.SS_base (META.ST "wormhole")), ToyTy_base_unlimitednatural), uncurry cons (I ((META.SS_base (META.ST "is_sound")), ToyTy_base_void), nil)), uncurry cons (ToyClass ((META.SS_base (META.ST "Person")), uncurry cons (I ((META.SS_base (META.ST "boss")), ToyTy_object (ToyTyObj (ToyTyCore (Toy_ty_class_ext ((META.SS_base (META.ST "oid")), (Code_Numeral.natural_of_integer 0), (Code_Numeral.natural_of_integer 2), Toy_ty_class_node_ext ((Code_Numeral.natural_of_integer 0), Toy_multiplicity_ext (uncurry cons (I (Mult_star, NONE), nil), NONE, uncurry cons (Set, nil), ()), (META.SS_base (META.ST "Person")), ()), Toy_ty_class_node_ext ((Code_Numeral.natural_of_integer 1), Toy_multiplicity_ext (uncurry cons (I (Mult_nat ((Code_Numeral.natural_of_integer 0)), SOME (Mult_nat ((Code_Numeral.natural_of_integer 1)))), nil), SOME ((META.SS_base (META.ST "boss"))), uncurry cons (Set, nil), ()), (META.SS_base (META.ST "Person")), ()), ())), nil))), uncurry cons (I ((META.SS_base (META.ST "salary")), ToyTy_base_integer), uncurry cons (I ((META.SS_base (META.ST "is_meta_thinking")), ToyTy_base_boolean), nil))), uncurry cons (ToyClass ((META.SS_base (META.ST "Molecule")), nil, uncurry cons (ToyClass ((META.SS_base (META.ST "Atom")), uncurry cons (I ((META.SS_base (META.ST "size")), ToyTy_base_integer), nil), nil), nil)), nil)), nil)), nil))), uncurry cons (META_instance (ToyInstance (uncurry cons (Toy_instance_single_ext (SOME ((META.SS_base (META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n3"))), SOME ((META.SS_base (META.ST "Person"))), ToyAttrNoCast (uncurry cons (I (NONE, I ((META.SS_base (META.ST "salary")), ShallB_term (ToyDefInteger ((META.SS_base (META.ST "1")))))), nil)), ()), nil))), uncurry cons (META_instance (ToyInstance (uncurry cons (Toy_instance_single_ext (SOME ((META.SS_base (META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n1"))), SOME ((META.SS_base (META.ST "Person"))), ToyAttrNoCast (uncurry cons (I (NONE, I ((META.SS_base (META.ST "salary")), ShallB_term (ToyDefInteger ((META.SS_base (META.ST "1300")))))), uncurry cons (I (NONE, I ((META.SS_base (META.ST "boss")), ShallB_str ((META.SS_base (META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n2"))))), nil))), ()), uncurry cons (Toy_instance_single_ext (SOME ((META.SS_base (META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n2"))), SOME ((META.SS_base (META.ST "Person"))), ToyAttrNoCast (uncurry cons (I (NONE, I ((META.SS_base (META.ST "salary")), ShallB_term (ToyDefInteger ((META.SS_base (META.ST "1800")))))), nil)), ()), nil)))), uncurry cons (META_class_raw (Floor1, Toy_class_raw_ext (ToyTyObj (ToyTyCore_pre ((META.SS_base (META.ST "Person"))), uncurry cons (uncurry cons (ToyTyCore_pre ((META.SS_base (META.ST "Galaxy"))), nil), nil)), uncurry cons (I ((META.SS_base (META.ST "salary")), ToyTy_base_integer), uncurry cons (I ((META.SS_base (META.ST "boss")), ToyTy_object (ToyTyObj (ToyTyCore_pre ((META.SS_base (META.ST "Person"))), nil))), uncurry cons (I ((META.SS_base (META.ST "is_meta_thinking")), ToyTy_base_boolean), nil))), nil, false, ())), uncurry cons (META_class_raw (Floor1, Toy_class_raw_ext (ToyTyObj (ToyTyCore_pre ((META.SS_base (META.ST "Galaxy"))), nil), uncurry cons (I ((META.SS_base (META.ST "wormhole")), ToyTy_base_unlimitednatural), uncurry cons (I ((META.SS_base (META.ST "is_sound")), ToyTy_base_void), nil)), nil, false, ())), uncurry cons (META_class_raw (Floor1, Toy_class_raw_ext (ToyTyObj (ToyTyCore_pre ((META.SS_base (META.ST "Molecule"))), uncurry cons (uncurry cons (ToyTyCore_pre ((META.SS_base (META.ST "Person"))), nil), nil)), nil, nil, false, ())), uncurry cons (META_class_raw (Floor1, Toy_class_raw_ext (ToyTyObj (ToyTyCore_pre ((META.SS_base (META.ST "Atom"))), uncurry cons (uncurry cons (ToyTyCore_pre ((META.SS_base (META.ST "Molecule"))), nil), nil)), uncurry cons (I ((META.SS_base (META.ST "size")), ToyTy_base_integer), nil), nil, false, ())), nil)))))), uncurry cons (I ((META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n3"), I (Toy_instance_single_ext (SOME ((META.SS_base (META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n3"))), SOME ((META.SS_base (META.ST "Person"))), ToyAttrNoCast (uncurry cons (I (NONE, I ((META.SS_base (META.ST "salary")), ShallB_term (ToyDefInteger ((META.SS_base (META.ST "1")))))), nil)), ()), Oids ((Code_Numeral.natural_of_integer 0), (Code_Numeral.natural_of_integer 1), (Code_Numeral.natural_of_integer 3)))), uncurry cons (I ((META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n2"), I (Toy_instance_single_ext (SOME ((META.SS_base (META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n2"))), SOME ((META.SS_base (META.ST "Person"))), ToyAttrNoCast (uncurry cons (I (NONE, I ((META.SS_base (META.ST "salary")), ShallB_term (ToyDefInteger ((META.SS_base (META.ST "1800")))))), nil)), ()), Oids ((Code_Numeral.natural_of_integer 0), (Code_Numeral.natural_of_integer 1), (Code_Numeral.natural_of_integer 2)))), uncurry cons (I ((META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n1"), I (Toy_instance_single_ext (SOME ((META.SS_base (META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n1"))), SOME ((META.SS_base (META.ST "Person"))), ToyAttrNoCast (uncurry cons (I (NONE, I ((META.SS_base (META.ST "salary")), ShallB_term (ToyDefInteger ((META.SS_base (META.ST "1300")))))), uncurry cons (I (NONE, I ((META.SS_base (META.ST "boss")), ShallB_str ((META.SS_base (META.ST "X⇩P⇩e⇩r⇩s⇩o⇩n2"))))), nil))), ()), Oids ((Code_Numeral.natural_of_integer 0), (Code_Numeral.natural_of_integer 1), (Code_Numeral.natural_of_integer 1)))), nil))), nil, false, false, I (nil, nil), nil, I (NONE, false), ()) end))))›
Instance σ⇩1_object0 :: Person = [ "salary" = 1000, "boss" = self 1 ]
     and σ⇩1_object1 :: Person = [ "salary" = 1200 ]
     and σ⇩1_object2 :: Person = [ "salary" = 2600, "boss" = X⇩P⇩e⇩r⇩s⇩o⇩n1 ]
     and σ⇩1_object4 :: Person = [ "salary" = 2300, "boss" = self 2 ]
(* Fails because of modified map update syntax priorities
State[shallow] σ⇩1 = [ σ⇩1_object0, σ⇩1_object1, σ⇩1_object2, X⇩P⇩e⇩r⇩s⇩o⇩n1, σ⇩1_object4, X⇩P⇩e⇩r⇩s⇩o⇩n2 ]

(* 15 ************************************ 34 + 1 *)
State[shallow] σ⇩1' = [ X⇩P⇩e⇩r⇩s⇩o⇩n1, X⇩P⇩e⇩r⇩s⇩o⇩n2, X⇩P⇩e⇩r⇩s⇩o⇩n3 ]

(* 16 ************************************ 35 + 1 *)
PrePost[shallow] σ⇩1 σ⇩1'
*)
end