*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Hardware modelling: Temporal Abstraction*From*: Martin Ellis <m.a.ellis at ncl.ac.uk>*Date*: Tue, 9 Aug 2005 15:59:40 +0100*Cc*:*User-agent*: KMail/1.8.1

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. (Actually, I read the "Advanced Induction Techniques" section in the tutorial, 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))))" by(auto simp add:wo1) (* 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)))" by(simp add:wo2) (* *********************************************************************** *) lemma inf_ex:"Inf P \<longrightarrow> Ex P" by(auto simp add: Inf_def) (* *********************************************************************** *) (* 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

- Previous by Date: [isabelle] CFP: TCS special issue on Automated Reasoning for Security Protocol Analysis
- Next by Date: [isabelle] Simplifier problem
- Previous by Thread: [isabelle] CFP: TCS special issue on Automated Reasoning for Security Protocol Analysis
- Next by Thread: [isabelle] Simplifier problem
- Cl-isabelle-users August 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list