-- I) Base case

open INV
  red inv100(init) .
close

-- II) Inductive ceses

--
-- In each inductive case where we prove that any transition rule
-- corresponding to an action 'act' preserves a property P, namely
-- P(s) implies P(act(s)) for any s, we usually have to split the
-- state space into multiple ones to make progress on the proof.
-- For each sub-space, a proof score that looks like this is written:
--
--   open ISTEP
--   -- arbitrary objects
--     Declare constants denoting arbitrary objects.
--   -- assumption
--     Declare equations characterizing this sub-space.
--   -- successor state
--     eq s' = act(s) .
--   -- check if the predicate is true
--     red P(s) implies P(s') .
--   close
--
-- In a proof score, we use constants to denote arbitrary objects.
-- In this example, nothing is declared in this part.
--
-- How do you split the state space into multiple ones? 
-- This is a good question!
-- Splitting the state space, or case analysis is one of the most
-- intelligent and important activities in writing proof scores. 
-- Case analysis depends on systems, problems, etc. that we are
-- dealing with. 
-- We expect you to grasp how to split the state space through this
-- seminar. 
--

--> 1) inc(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq x(s) >= 0 = true .
-- successor state
  eq s' = inc(s) .
-- check if the predicate is true.
  red istep100 .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  eq x(s) >= 0 = false .
-- successor state
  eq s' = inc(s) .
-- check if the predicate is true.
  red istep100 .
close

--
-- If the (effective) condition of a transition rule is not always
-- true, what we have to do is first to split the state space into
-- two sub-spaces: one where the condition is true, and the other
-- where the condition is false. 
--
-- If the condition is false, the transition rule deos not change
-- anything. 
-- So, in theory, you don't have to take care of the case. 
-- From an engineering point of view, it is meaningful becasue you may
-- find some errors in the specification by writing the proof score
-- for this case and having the CafeOBJ system execute it. 
-- Therefore, first write the proof score for the case where the
-- condition is false. 
--

--> 2) dec(s)
-- 2.1) c-dec(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-dec(s) = treue .
  eq flag(s) = true .
--
  eq x(s) >= 1 = true .
-- successor state
  eq s' = dec(s) .
-- check if the predicate is true.
  red istep100 .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-dec(s) = treue .
  eq flag(s) = true .
--
  eq x(s) >= 1 = false .
-- successor state
  eq s' = dec(s) .
-- check if the predicate is true.
  red inv110(s) implies istep100 .
close
--
-- 2.1) not c-dec(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-dec(s) = false .
-- successor state
  eq s' = dec(s) .
-- check if the predicate is true.
  red istep100 .
close

--
-- Sometimes we need other invariants as lemmas to prove an invariant.
-- Finding lemmas is another intelligent and important activity.
-- If we need invariant Q as a lemma to prove P in a case,
-- instead of P(s) implies P(s'), Q(s) implies (P(s) implies P(s')) is 
-- reduced:
--
--   red Q(s) implies (P(s) implies P(s'))
--
-- (Q(s) implies (P(s) implies P(s'))) 
--                              iff ((Q(s) and P(s)) implies P(s')) .
--
-- Suppose that we prove that the system has the following invariant 
--  
--   P1(s) and ... and Pi(s) and ... and Pn(s)
--
-- which is called P(s).
-- In order to show that an action 'act' preserves P(s), we check if
-- P(s) implies P(act(s)) is true. 
-- This check can be done compositionally, namely that
--   
--   P(s) implies P1(act(s))
--   ...
--   P(s) implies Pi(act(s))
--   ...
--   P(s) implies Pn(act(s))
--
-- Moreover, these cheks can be replaced by the following:
--
--   P1(s) implies P1(act(s))
--   ...
--   Pi(s) implies Pi(act(s))
--   ...
--   Pn(s) implies Pn(act(s))
--
-- But sometimes Pi(s) implies Pi(act(s)) may not be true because
-- the induction hypothesis Pi(s) used is too weak. 
-- Therefroe, instead of Pi(s) implies Pi(act(s)), we can check the
-- following: 
--
--   (Pj(s) and Pi(s)) implies Pi(s)
-- or
--   Pj(s) implies (Pi(s)) implies Pi(s))
--
-- Pj(s) can be considered as a lemma to prove that Pi(s) is
-- invariant. 
--

--> Q.E.D.