1(* Title: HOL/HOLCF/IOA/Asig.thy 2 Author: Olaf M��ller, Tobias Nipkow & Konrad Slind 3*) 4 5section \<open>Action signatures\<close> 6 7theory Asig 8imports Main 9begin 10 11type_synonym 'a signature = "'a set \<times> 'a set \<times> 'a set" 12 13definition inputs :: "'action signature \<Rightarrow> 'action set" 14 where asig_inputs_def: "inputs = fst" 15 16definition outputs :: "'action signature \<Rightarrow> 'action set" 17 where asig_outputs_def: "outputs = fst \<circ> snd" 18 19definition internals :: "'action signature \<Rightarrow> 'action set" 20 where asig_internals_def: "internals = snd \<circ> snd" 21 22definition actions :: "'action signature \<Rightarrow> 'action set" 23 where "actions asig = inputs asig \<union> outputs asig \<union> internals asig" 24 25definition externals :: "'action signature \<Rightarrow> 'action set" 26 where "externals asig = inputs asig \<union> outputs asig" 27 28definition locals :: "'action signature \<Rightarrow> 'action set" 29 where "locals asig = internals asig \<union> outputs asig" 30 31definition is_asig :: "'action signature \<Rightarrow> bool" 32 where "is_asig triple \<longleftrightarrow> 33 inputs triple \<inter> outputs triple = {} \<and> 34 outputs triple \<inter> internals triple = {} \<and> 35 inputs triple \<inter> internals triple = {}" 36 37definition mk_ext_asig :: "'action signature \<Rightarrow> 'action signature" 38 where "mk_ext_asig triple = (inputs triple, outputs triple, {})" 39 40 41lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def 42 43lemma asig_triple_proj: 44 "outputs (a, b, c) = b \<and> 45 inputs (a, b, c) = a \<and> 46 internals (a, b, c) = c" 47 by (simp add: asig_projections) 48 49lemma int_and_ext_is_act: "a \<notin> internals S \<Longrightarrow> a \<notin> externals S \<Longrightarrow> a \<notin> actions S" 50 by (simp add: externals_def actions_def) 51 52lemma ext_is_act: "a \<in> externals S \<Longrightarrow> a \<in> actions S" 53 by (simp add: externals_def actions_def) 54 55lemma int_is_act: "a \<in> internals S \<Longrightarrow> a \<in> actions S" 56 by (simp add: asig_internals_def actions_def) 57 58lemma inp_is_act: "a \<in> inputs S \<Longrightarrow> a \<in> actions S" 59 by (simp add: asig_inputs_def actions_def) 60 61lemma out_is_act: "a \<in> outputs S \<Longrightarrow> a \<in> actions S" 62 by (simp add: asig_outputs_def actions_def) 63 64lemma ext_and_act: "x \<in> actions S \<and> x \<in> externals S \<longleftrightarrow> x \<in> externals S" 65 by (fast intro!: ext_is_act) 66 67lemma not_ext_is_int: "is_asig S \<Longrightarrow> x \<in> actions S \<Longrightarrow> x \<notin> externals S \<longleftrightarrow> x \<in> internals S" 68 by (auto simp add: actions_def is_asig_def externals_def) 69 70lemma not_ext_is_int_or_not_act: "is_asig S \<Longrightarrow> x \<notin> externals S \<longleftrightarrow> x \<in> internals S \<or> x \<notin> actions S" 71 by (auto simp add: actions_def is_asig_def externals_def) 72 73lemma int_is_not_ext:"is_asig S \<Longrightarrow> x \<in> internals S \<Longrightarrow> x \<notin> externals S" 74 by (auto simp add: externals_def actions_def is_asig_def) 75 76end 77