src/HOL/MicroJava/DFA/Semilat.thy
changeset 62145 5b946c81dfbf
parent 61994 133a8a888ae8
child 63258 576fb8068ba6
     1.1 --- a/src/HOL/MicroJava/DFA/Semilat.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Semilat.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -15,23 +15,26 @@
     1.4  type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     1.5  type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
     1.6  
     1.7 -consts
     1.8 -  "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
     1.9 -  "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
    1.10 -  "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" 
    1.11 -(*<*)
    1.12 +definition lesub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
    1.13 +  where "lesub x r y \<longleftrightarrow> r x y"
    1.14 +
    1.15 +definition lesssub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
    1.16 +  where "lesssub x r y \<longleftrightarrow> lesub x r y \<and> x \<noteq> y"
    1.17 +
    1.18 +definition plussub :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c"
    1.19 +  where "plussub x f y = f x y"
    1.20 +
    1.21  notation (ASCII)
    1.22    "lesub"  ("(_ /<='__ _)" [50, 1000, 51] 50) and
    1.23    "lesssub"  ("(_ /<'__ _)" [50, 1000, 51] 50) and
    1.24    "plussub"  ("(_ /+'__ _)" [65, 1000, 66] 65)
    1.25 -(*>*)
    1.26 +
    1.27  notation
    1.28    "lesub"  ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
    1.29    "lesssub"  ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
    1.30    "plussub"  ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
    1.31 -(*<*)
    1.32 +
    1.33  (* allow \<sub> instead of \<bsub>..\<esub> *)
    1.34 -
    1.35  abbreviation (input)
    1.36    lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
    1.37    where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
    1.38 @@ -43,12 +46,6 @@
    1.39  abbreviation (input)
    1.40    plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
    1.41    where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
    1.42 -(*>*)
    1.43 -
    1.44 -defs
    1.45 -  lesub_def:   "x \<sqsubseteq>\<^sub>r y \<equiv> r x y"
    1.46 -  lesssub_def: "x \<sqsubset>\<^sub>r y \<equiv> x \<sqsubseteq>\<^sub>r y \<and> x \<noteq> y"
    1.47 -  plussub_def: "x \<squnion>\<^sub>f y \<equiv> f x y"
    1.48  
    1.49  definition ord :: "('a \<times> 'a) set \<Rightarrow> 'a ord" where
    1.50    "ord r \<equiv> \<lambda>x y. (x,y) \<in> r"