Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

small steps here and there

This commit is contained in:
Burkhart Wolff 2018-08-30 12:53:02 +02:00
parent 177938de0b
commit 745b335033
4 changed files with 26 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Isa_DOF.thy
View File

@ -880,14 +880,17 @@ end (* struct *)
*}
ML{*
structure AttributeAcces =
structure AttributeAccess =
struct
fun calculate_attr_access ctxt proj_term term =
(* term assumed to be ground type, (f term) not necessarily *)
let val [subterm'] = Type_Infer_Context.infer_types ctxt [proj_term $ term]
val ty = type_of (subterm')
val _ = writeln ("calculate_attr_access raw term: " ^ Syntax.string_of_term ctxt subterm')
(* Debug :
val _ = writeln ("calculate_attr_access raw term: "
^ Syntax.string_of_term ctxt subterm')
*)
val term' = (Const(@{const_name "HOL.eq"}, ty --> ty --> HOLogic.boolT)
$ subterm'
$ Free("_XXXXXXX", ty))

10
RegExp.thy
View File

@ -77,10 +77,18 @@ fun L :: "'a rexp => 'a lang"
where L_Emp : "L Empty = {}"
|L_Atom: "L (\<lfloor>a\<rfloor>) = {[a]}"
|L_Un: "L (el || er) = (L el) \<union> (L er)"
|L_Conc: "L (el ~~ er) = {xs@ys | xs ys. xs:L el \<and> ys:L er}"
|L_Conc: "L (el ~~ er) = {xs@ys | xs ys. xs \<in> L el \<and> ys \<in> L er}"
|L_Star: "L (Star e) = star(L e)"
fun L\<^sub>s\<^sub>u\<^sub>b :: "'a::order rexp => 'a lang"
where L\<^sub>s\<^sub>u\<^sub>b_Emp : "L\<^sub>s\<^sub>u\<^sub>b Empty = {}"
|L\<^sub>s\<^sub>u\<^sub>b_Atom: "L\<^sub>s\<^sub>u\<^sub>b (\<lfloor>a\<rfloor>) = {z . \<forall>x. x \<le> a \<and> z=[x]}"
|L\<^sub>s\<^sub>u\<^sub>b_Un: "L\<^sub>s\<^sub>u\<^sub>b (el || er) = (L\<^sub>s\<^sub>u\<^sub>b el) \<union> (L\<^sub>s\<^sub>u\<^sub>b er)"
|L\<^sub>s\<^sub>u\<^sub>b_Conc: "L\<^sub>s\<^sub>u\<^sub>b (el ~~ er) = {xs@ys | xs ys. xs \<in> L\<^sub>s\<^sub>u\<^sub>b el \<and> ys \<in> L\<^sub>s\<^sub>u\<^sub>b er}"
|L\<^sub>s\<^sub>u\<^sub>b_Star: "L\<^sub>s\<^sub>u\<^sub>b (Star e) = star(L\<^sub>s\<^sub>u\<^sub>b e)"
schematic_goal WeCompute: "L(Star ((\<lfloor>CHR ''a''\<rfloor> || \<lfloor>CHR ''b''\<rfloor>) ~~ \<lfloor>CHR ''c''\<rfloor>)) = ?X"
by simp

22
examples/conceptual/Attributes.thy
View File

@ -29,7 +29,7 @@ text*[dfgdfg2::C, z = "None"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
text*[omega::E, x = "''def''"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
text\<open> @{docitem_ref \<open>dfgdfg\<close>} \<close>
text\<open> As mentioned in @{docitem_ref \<open>dfgdfg\<close>} \<close>
term "A.x (undefined\<lparr>A.x := 3\<rparr>)"
@ -51,9 +51,9 @@ DOF_core.get_attribute_info "Conceptual.C" "z" @{theory};
ML\<open>
DOF_core.get_value_local "sdf" @{context};
DOF_core.get_value_local "sdfg" @{context};
DOF_core.get_value_local "xxxy" @{context};
DOF_core.get_value_local "sdf" @{context};
DOF_core.get_value_local "sdfg" @{context};
DOF_core.get_value_local "xxxy" @{context};
DOF_core.get_value_local "dfgdfg" @{context};
DOF_core.get_value_local "omega" @{context};
\<close>
@ -63,28 +63,28 @@ text\<open>A not too trivial test: default y -> [].
The latter wins at access time.
Then @{term "t"}: creation of a multi inheritance object omega,
triple updates, the last one wins.\<close>
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg});
val t = HOLogic.dest_string (@{docitem_attr x::omega}); \<close>
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg});
val t = HOLogic.dest_string (@{docitem_attr x::omega}); \<close>
section\<open>Mutation of Attibutes in DocItems\<close>
ML\<open> val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attr a2::omega} \<close>
ML\<open> val Const("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attr a2::omega} \<close>
update_instance*[omega::E, a2+="1"]
ML\<open> val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attr a2::omega} \<close>
ML\<open> val Const("Groups.one_class.one", @{typ "int"})= @{docitem_attr a2 :: omega} \<close>
update_instance*[omega::E, a2+="6"]
ML\<open> @{docitem_attr a2::omega} \<close>
ML\<open> HOLogic.dest_number @{docitem_attr a2::omega} \<close>
ML\<open> @{docitem_attr a2::omega};
val s = HOLogic.dest_number @{docitem_attr a2::omega} \<close>
update_instance*[omega::E, x+="''inition''"]
ML\<open> val s = HOLogic.dest_string ( @{docitem_attr x::omega}) \<close>
ML\<open> val s = HOLogic.dest_string ( @{docitem_attr x::omega}) \<close>
update_instance*[omega::E, y+="[''defini'',''tion'']"]

1
ontologies/Conceptual.thy
View File

@ -14,6 +14,7 @@ doc_class C = B +
z :: "A option" <= None (* A LINK, i.e. an attribute that has a type
referring to a document class. Mathematical
relations over document items can be modeled. *)
g :: "thm"
datatype enum = X1 | X2 | X3