ARM_security_properties/model/armSyntax.sml

31   Term.inst [Type.alpha |->
94     Term.inst [Type.alpha |-> stringSyntax.string_ty] s)
99     [Type.alpha |-> Term.type_of v,
100      Type.beta |-> Term.type_of s] valuestate_tm, [v,s])
104   HolKernel.mk_comb(Term.inst[Type.alpha |-> Term.type_of t] constT_tm,t)
109     [Type.alpha |-> dest_monad_type (Term.type_of f),
110      Type.beta  |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) g]
116     [Type.alpha |-> dest_monad_type (Term.type_of f),
117      Type.beta  |-> dest_monad_type (Term.type_of g)] parT_tm,[f,g])
122     [Type.alpha |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) f]
128     [Type.alpha |-> snd (dom_rng (Term.type_of f))] readT_tm, f)
137     [Term.inst [Type.alpha |-> ``:iiid``] ii,
138      Term.inst [Type.alpha |-> ``:RName``] r])
143     [Term.inst [Type.alpha |-> ``:iiid``] ii,
144      Term.inst [Type.alpha |-> ``:RName``] r,
150     [Term.inst [Type.alpha |-> ``:iiid``] ii,
151      Term.inst [Type.alpha |-> ``:PSRName``] r])
156     [Term.inst [Type.alpha |-> ``:iiid``] ii,
157      Term.inst [Type.alpha |-> ``:PSRName``] r,
158      Term.inst [Type.alpha |-> ``:ARMpsr``] v])
163     [Term.inst [Type.alpha |-> ``:iiid``] ii,
169     [Term.inst [Type.alpha |-> ``:iiid``] ii,
176     [Term.inst [Type.alpha |-> ``:iiid``] ii,
183     [Term.inst [Type.alpha |-> ``:iiid``] ii,
190   HolKernel.mk_comb(read_cpsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
195     [Term.inst [Type.alpha |-> ``:iiid``] ii,
196      Term.inst [Type.alpha |-> ``:ARMpsr``] v])
200   HolKernel.mk_comb(read_spsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
205     [Term.inst [Type.alpha |-> ``:iiid``] ii,
206      Term.inst [Type.alpha |-> ``:ARMpsr``] v])
211     [Term.inst [Type.alpha |-> ``:iiid``] ii,
214         Term.inst [Type.alpha |-> ``:num``] s)])
219     [Term.inst [Type.alpha |-> ``:iiid``] ii,
222         Term.inst [Type.alpha |-> ``:num``] s),
228     Term.inst [Type.alpha |-> ``:iiid``] ii)
232   HolKernel.mk_comb(send_event_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
237     Term.inst [Type.alpha |-> ``:iiid``] ii)
242     Term.inst [Type.alpha |-> ``:iiid``] ii)
255     [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] align_tm,
261     [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] aligned_tm,
267   [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] bit_count_tm, w)
272   [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] ITAdvance_tm, w)