2018-06-11 16:48:49 +00:00
|
|
|
theory Conceptual
|
2018-05-24 09:30:01 +00:00
|
|
|
imports "../Isa_DOF"
|
2018-04-28 13:15:25 +00:00
|
|
|
begin
|
2018-05-24 09:30:01 +00:00
|
|
|
|
2018-04-28 13:15:25 +00:00
|
|
|
doc_class A =
|
|
|
|
|
x :: "string"
|
|
|
|
|
|
|
|
|
|
doc_class B =
|
|
|
|
|
y :: "string list" <= "[]"
|
|
|
|
|
|
|
|
|
|
doc_class C = B +
|
|
|
|
|
z :: "A option" <= None
|
|
|
|
|
|
|
|
|
|
datatype enum = X1 | X2 | X3
|
|
|
|
|
|
|
|
|
|
doc_class D = B +
|
|
|
|
|
a1 :: enum <= "X2"
|
|
|
|
|
a2 :: int <= 0
|
|
|
|
|
|
|
|
|
|
doc_class F =
|
|
|
|
|
r :: "thm list"
|
2018-05-15 07:11:17 +00:00
|
|
|
b :: "(A \<times> C) set" <= "{}"
|
2018-04-28 13:15:25 +00:00
|
|
|
|
|
|
|
|
doc_class M =
|
|
|
|
|
trace :: "(A + C + D + F) list"
|
2018-05-15 07:11:17 +00:00
|
|
|
where "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
|
2018-04-28 13:15:25 +00:00
|
|
|
|
|
|
|
|
end
|
