From a1941b2f1526edf6a9dd6cabd130a47acec51842 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Tue, 12 Nov 2019 10:10:25 +0100
Subject: [PATCH] startpunkt

---
 src/ontologies/math_exam/Nmath_exam.thy | 152 ++++++++++++++++++++++++
 1 file changed, 152 insertions(+)
 create mode 100644 src/ontologies/math_exam/Nmath_exam.thy

diff --git a/src/ontologies/math_exam/Nmath_exam.thy b/src/ontologies/math_exam/Nmath_exam.thy
new file mode 100644
index 0000000..785da13
--- /dev/null
+++ b/src/ontologies/math_exam/Nmath_exam.thy
@@ -0,0 +1,152 @@
+(*************************************************************************
+ * Copyright (C) 
+ *               2019      The University of Exeter 
+ *               2018-2019 The University of Paris-Saclay
+ *               2018      The University of Sheffield
+ *
+ * License:
+ *   This program can be redistributed and/or modified under the terms
+ *   of the 2-clause BSD-style license.
+ *
+ *   SPDX-License-Identifier: BSD-2-Clause
+ *************************************************************************)
+
+theory Nmath_exam
+ imports "../../DOF/Isa_COL"
+begin
+  
+(*<<*)  
+text\<open>In our scenario, content has four different types of addressees: 
+\<^item> the @{emph \<open>setter\<close>}, i.e. the author of the exam, 
+\<^item> the @{emph \<open>student\<close>}, i.e. the addressee of the exam, 
+\<^item> the @{emph \<open>checker\<close>}, i.e. a person that checks the exam for
+\<^item> the @{emph \<open>external\_examiner\<close>}, i.e. a person that checks the exam for
+  feasibility and non-ambiguity.
+
+Note that the latter quality assurance mechanism is used in many universities,
+where for organizational reasons the execution of an exam takes place in facilities
+where the author of the exam is not expected to be physically present.
+\<close>  
+  
+  
+datatype ContentClass =   
+      setter            (* \<open>the 'author' of the exam\<close> *)
+    | checker           (* \<open>the 'proof-reader' of the exam\<close> *)
+    | externalExaminer  (* \<open>an external 'proof-reader' of the exam\<close> *)
+    | student           (* \<open>the victim ;-) ... \<close> *)
+
+  
+doc_class Author =
+   affiliation :: "string"
+   email :: "string"
+
+    
+   
+datatype Subject =
+  algebra | geometry | statistical | analysis
+
+datatype Level =
+  oneStar | twoStars | threeStars
+
+  
+datatype Grade =
+  A1 | A2 | A3
+
+
+doc_class Exam_item = 
+  level        :: "int option"
+  concerns     :: "ContentClass set"  
+
+doc_class Header = Exam_item +
+  examSubject  :: "(Subject) list"
+  date         :: string
+  timeAllowed  :: int (*  minutes *)
+
+
+type_synonym SubQuestion = string
+ 
+doc_class Answer_Formal_Step =  Exam_item +
+  justification :: string
+  "term"        :: "string" 
+  
+doc_class Answer_YesNo =  Exam_item +
+  step_label    :: string
+  yes_no        :: bool  (* \<open>for checkboxes\<close> *)
+
+datatype Question_Type =   
+  formal | informal | mixed 
+  
+doc_class Task = Exam_item +
+  local_grade :: Level
+  type        :: Question_Type
+  subitems    :: "(SubQuestion * (Answer_Formal_Step list + Answer_YesNo)list) list"
+  concerns    :: "ContentClass set" <= "{setter,student,checker,externalExaminer}" 
+  mark        :: int
+   
+
+doc_class Exercise = Exam_item +
+  content  :: "(Task) list"
+  concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}"
+
+
+text\<open>In many institutions, it makes sense to have a rigorous process of validation
+for exam subjects : is the initial question correct ? Is a proof in the sense of the
+question possible ? We model the possibility that the @{term setter} validates a 
+question by a sample proof validated by Isabelle. In our scenario this sample proofs
+are completely @{emph \<open>intern\<close>}, i.e. not exposed to the students but just additional
+material for the internal review process of the exam.\<close>
+  
+doc_class Validation = 
+   tests  :: "term list"  <="[]"
+   proofs :: "thm list"   <="[]"
+  
+doc_class Solution = Exam_item +
+  content  :: "Exercise list"
+  valids   :: "Validation list"
+  concerns :: "ContentClass set" <= "{setter,checker,externalExaminer}"
+  
+doc_class MathExam =
+  content :: "(Header + Author + Exercise) list"
+  global_grade :: Grade 
+  accepts "\<lbrace>Author\<rbrace>\<^sup>+  ~~  Header ~~  \<lbrace>Exercise ~~ Solution\<rbrace>\<^sup>+ "
+
+
+(*
+exercise - (header ~ context_description ~ task list)
+*)
+
+(*
+tasks & subtask
+
+answer > subanswer
+
+answer_element
+ - text
+ - checkbox
+ - radiobutton
+ - equational derivation
+ - proof derivation
+
+solution > subsolution
+ - test
+ - checkbox
+ - radiobutton
+ - equational derivation
+ - proof derivation
+
+marking > submarking
+  
+grade
+
+Invarianten:
+1 : n Relation answer_element \<longrightarrow> subsolution
+
+2 : invariants over markings and grades
+
+
+*)
+
+
+
+(*>>*)
+end