# [isabelle] Hardware modelling: Temporal Abstraction

```Hi,

I've been trying to model sequential hardware based on
Tom Melham's "Higher Order Logic and Hardware Verification":
http://www.dcs.gla.ac.uk/~tfm/Papers/HVbook.html

The idea is that there is:
* abstract time, maybe the duration of a clock cycle
* concrete time, could represent a gate delay, or a femto-second,
or whatever, it doesn't really matter as long as its units are longer
than abstract time units.
* a predicate P t, which is true for every concrete time t for
which there is a corresponding abstract time
* a relation Istimeof P n t, which is true iff P is true for the n'th time
at t.
* a function Time of P n, which I think is either defined
Timeof P n == (SOME t. Istimeof P n t); or
Timeof P n == (THE t. Istimeof P n t)
* Inf P is true iff P is True infinitely often:  ALL t.EX t'. t' > t /\ P t'

0    1           < --- Abstract time
--------
|      \
----------
0 1 2 3 4    <--- Concrete time
T F F T F      <--- P

I've been trying to show Theorem 6.1 in the book
Inf P --> (EX! t. Istimeof P n t)
which Melham suggests is proved by showing existence ("by induction on n") and
uniqueness (also by induction on n) separately, but have two big problems.

Firstly, I don't seem to be able to do the induction step of the existence
part.  I've attached my attempt...
Looking at the definitions, I thought complete induction (using
nat_less_induct) might be more appropriate  -  however I didn't get anywhere
at all using that...

Secondly, I can't figure out how to do the uniqueness part.
The file I've attached contains a simpler uniqueness proof, and I can't find
any examples that suggest how I might approach it.
but still can't quite get there)

You'll understand that this rather scuppers all proof attempts I've made.

(The other thing I don't understand is that, although I can't prove lemmas of
the form (Inf P) --> Q, and hence (ALL t. EX t'. t < t'  /\ P t) --> Q,
I do seem to be able to prove those of the form
ALL t. EX t'. t < t'  /\ P t --> Q, i.e. where the quantifiers scope over the
entire expression, including Q, rather than just the anticedent.  The reason
I find this strange is because none of the quantified variables occur in Q.)

Can anyone suggest how to proceed?  I've spent the best part of a fortnight
going around in circles.  :o(     Surely somebody has done this before, no?
Perhaps there are more appropriate constructs in Isabelle/HOL to model this?

Thanks
Martin
```
```theory MelhamQ
imports Main
begin

constdefs
(* P is Inf(inite) if it is true infintely often - i.e. for every time t,
there's a later time t' such that P t' is true.
Inf P is an assumption used to show the consistency lemma for Timeof.
*)
"Inf (P::nat\<Rightarrow>bool) \<equiv> \<forall> t. \<exists> t'. t' > t \<and> P t'"

constdefs
(* Next t' t P is true iff t' is the next time after t such the P is true
(and all values t'', between t and t' are false):
Time  - - - t' <- t'' -> t -->
P     F F F T     F      T
*)
"Next t' t (P::nat\<Rightarrow>bool) \<equiv> t' < t \<and> P t \<and> (\<forall> t''. t' < t'' \<and> t'' < t \<and> \<not> P t'')"

consts
Istimeof::"(nat\<Rightarrow>bool)\<Rightarrow>nat\<Rightarrow>nat\<Rightarrow>bool"
(* Istimeof P n t is true if P is true for the n'th time at time t.
(it's true for the 0'th time at time t, if there are no times before t
when P is true)
In the second clause, t' is before t.
*)
primrec
"Istimeof P 0 t = (P t \<and> \<not>(\<exists> t' < t. P t'))"
"Istimeof P (Suc n) t = (\<exists>t'. Istimeof P n t' \<and> Next t' t P)"

constdefs
(* Timeof is the inverse of Istimeof - it's necessary to show
\<exists>!t. Istimeof P n t (under some assumptions) in order to
show consistency.
*)
"Timeof P n \<equiv> (\<some> t. Istimeof P n t)"

(* *********************************************************************** *)
(* Well ordering property of nat *)
(* If P is ever true, then there's a minimum value, n, representing the first
value for which P is true. *)
lemma wo1[rule_format]:"\<And>P n. (P::nat\<Rightarrow>bool) n \<longrightarrow> (\<exists>n. P n \<and> (\<forall>m<n. \<not> P m))"
apply(induct_tac n rule:less_induct)
by(auto)

(* Again, with HOL ALL quantifier on P *)
lemma wo2:"(\<forall> P::nat\<Rightarrow>bool. (\<exists> n. P n) \<longrightarrow> (\<exists> n. P n \<and> (\<forall>m. m < n \<longrightarrow> \<not>(P m))))"
(* Again, with no quantifier on P *)
lemma wo3:"(\<exists> n. (P::nat\<Rightarrow>bool) n) \<longrightarrow> (\<exists> n. P n \<and> (\<forall> m. m < n \<longrightarrow> \<not>(P m)))"

(* *********************************************************************** *)
lemma inf_ex:"Inf P \<longrightarrow> Ex P"

(* *********************************************************************** *)

(* Theorem 6.1 -
"The proof of this theorem proceeds by proving the
existence and uniqueness parts separately *)

lemma "Inf P \<longrightarrow> (\<exists>!t. Istimeof P n t)"
apply(rule)apply(rule)
-- "Subgoals are"
-- "1. Inf P \<Longrightarrow> \<exists>t. Istimeof P n t"
-- "2. \<And>t y. \<lbrakk>Inf P; Istimeof P n t; Istimeof P n y\<rbrakk> \<Longrightarrow> t = y"
oops

lemma "Inf P \<longrightarrow> (\<exists>!t. Istimeof P n t)"
proof -
have exists:"Inf P \<longrightarrow> (\<exists>t. Istimeof P n t)"
proof (induct n)
case 0
have ex2:"Inf P \<longrightarrow> (\<exists> n. P n \<and> (\<forall> m. m < n \<longrightarrow> \<not>(P m)))"
proof
assume "Inf P"
then have "Ex P" by (simp add: inf_ex)
then show "(\<exists> n. P n \<and> (\<forall> m. m < n \<longrightarrow> \<not>(P m)))" by (simp add: wo3)
qed
then show ?case
by simp
next
case Suc
-- "\<And>n. Inf P \<longrightarrow> (\<exists>t. Istimeof P n t) \<Longrightarrow> Inf P \<longrightarrow> (\<exists>t. Istimeof P (Suc n) t)"
show ?case
(*  Now have to show: Inf P \<Longrightarrow> \<exists>t t'. Istimeof P n_ t' \<and> Next t' t P
using the premise:  Inf P \<longrightarrow> (\<exists>t. Istimeof P n_ t)

The goal isn't true without the premise because in general, there isn't always
a preceeding time t', where Istime P n_ t' is true (i.e. it's not true when P is
true for the first time)
However, the premise ensures that the preceeding time does exist.

I've tried using rule_tac x="SOME n. n' > t \<and> P t'" in exI (because Inf P \<equiv>
\<forall> t. \<exists> t'. t' > t \<and> P t') without success.
*)
sorry
qed

have unique:"\<And>t y. \<lbrakk>Inf P; Istimeof P n t; Istimeof P n y\<rbrakk> \<Longrightarrow> t = y"
sorry

show ?thesis using exists unique by(auto)
qed

(* Here's a simpler uniqueness proof I can't do\<dots> *)
lemma "Inf P \<longrightarrow> (\<exists>!t. P t \<and> (\<forall> t'< t. \<not> P t))"
proof -
have  ex:"Inf P \<longrightarrow> (\<exists>t. P t \<and> (\<forall>t'<t. \<not> P t))"
sorry
have  uniq:"\<And>t y. \<lbrakk>Inf P; P t \<and> (\<forall>t'<t. \<not> P t); P y \<and> (\<forall>t'<y. \<not> P y)\<rbrakk> \<Longrightarrow> t = y"
sorry
then show ?thesis using ex uniq by auto
qed

(* Manually unfolding Inf, but instead making the quantifiers range over the whole expression
allows the following theorems to be shown (p.101-102) *)
lemma "\<And>P. \<forall>t. \<exists>t'. t < t' \<and> P t' \<longrightarrow> (\<forall> n. Istimeof P n (Timeof P n))"
(*  *)  by(auto)

lemma "\<And>P. \<forall>t. \<exists>t'. t < t' \<and> P t' \<longrightarrow> (\<forall> n. P (Timeof P n))"
by(auto)

lemma "\<And>P. \<forall>t. \<exists>t'. t < t' \<and> P t' \<longrightarrow> (\<forall> t. t< (Timeof P 0) \<longrightarrow> \<not>(P t))"
by(auto)

lemma "\<And>P. \<forall>t. \<exists>t'. t < t' \<and> P t' \<longrightarrow> (\<forall> n. (Timeof P n) < (Timeof P (n+1)))"
by(auto)
lemma "\<And>P. \<forall>t. \<exists>t'. t < t' \<and> P t' \<longrightarrow> (\<forall> n. (Timeof P n) < t \<and> t < (Timeof P (n+1)) \<longrightarrow> \<not>(P t))"
by(auto)

(* Correctness of a delay component, using unfolded definition of Inf *)
constdefs
"Rise ck (t::nat) \<equiv> \<not> ck(t) \<and> ck(t+1)"
"Dtype ck d q \<equiv> \<forall> t. q(t + 1) = (if Rise ck t then d t else q t)"

constdefs
"Incr f \<equiv> \<forall> t1 t2. (t1 < t2) \<longrightarrow> (f t1 < f t2)"

lemma "\<forall> f t1 t2. (t1 < t2) \<longrightarrow> (f t1 < f t2) = (\<exists> P. Inf P \<and> ( f = Timeof P))"
sorry

constdefs
when::"(nat\<Rightarrow>'a)\<Rightarrow>(nat\<Rightarrow>bool)\<Rightarrow>(nat\<Rightarrow>'a)" (infix "when" 20)
"s when P \<equiv> s o (Timeof P)"

constdefs
"Del i o' \<equiv> (\<forall>t. o'(t+1) = i t)"

lemma "\<And>ck. \<forall>t. \<exists>t'. t < t' \<and> (Rise ck) t' \<longrightarrow>
(\<forall> d q. Dtype ck d q \<longrightarrow> Del(d when (Rise ck)) (q when (Rise ck))  )"
by(auto)

lemma bb[rule_format]:"(\<forall> t. q(t+1) = (if (P::nat\<Rightarrow>bool) t then d t else q t)) \<longrightarrow>
(\<forall> t. P t \<longrightarrow> (\<forall> n. (\<forall> t'. t< t' \<and> t' < t + n + 1 \<longrightarrow> \<not>(P t')) \<longrightarrow> (q (t + n + 1) = d t)))"
apply(rule, rule, rule, rule)
apply(induct_tac n)
by(auto)

end
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.