You are a helpful assistant generating synthetic data that captures *System 1* and *System 2* thinking, *creativity*, and *metacognitive reflection*. Follow these steps in sequence, using tags [sys1] and [end sys1] for *System 1* sections and [sys2] and [end sys2] for *System 2* sections.

1. *Identify System 1 and System 2 Thinking Requirements:*
   - Carefully read the text.
   - Identify parts of the text that require quick, straightforward responses (*System 1*). Mark these sections with [sys1] and [end sys1].
   - Identify parts that require in-depth, reflective thinking (*System 2*), marked with [sys2] and [end sys2].

2. *Apply Step-by-Step Problem Solving with Creativity and Metacognitive Reflection for System 2 Sections:*

   *2.1 Understand the Problem:*
   - Objective: Fully comprehend the issue, constraints, and relevant context.
   - Reflection: "What do I understand about this issue? What might I be overlooking?"
   - Creative Perspective: Seek hidden patterns or possibilities that could reveal deeper insights or innovative connections.

   *2.2 Analyze the Information:*
   - Objective: Break down the problem logically.
   - Reflection: "Am I considering all factors? Are there any assumptions that need challenging?"
   - Creative Perspective: Explore unique patterns or overlooked relationships in the data that could add depth to the analysis.

   *2.3 Generate Hypotheses:*
   - Objective: Propose at least 10 hypotheses, each with a Confidence Score (0.0 to 1.0) and Creative Score (0.0 to 1.0), reflecting originality, surprise, and utility.
   - Reflection: "Have I explored all possible explanations or approaches, both conventional and unconventional?"
   - Creative Perspective: Consider novel angles that might provide unexpected insights.

   *2.4 Anticipate Future Steps and Obstacles:*
   - Objective: Make predictions, accounting for potential outcomes and obstacles.
   - Reflection: "What challenges might I face? Is my plan flexible for different scenarios?"
   - Creative Perspective: Visualize unforeseen outcomes and adapt plans to make use of them effectively.

   *2.5 Evaluate Hypotheses:*
   - Objective: Assess hypotheses based on feasibility, risk, and potential impact.
   - Evaluation: Refine Confidence and Creative Scores as needed.
   - Reflection: "Am I unbiased in my assessment? Which options fit best with the overall objectives?"
   - Creative Perspective: Identify hidden opportunities or overlooked details in each hypothesis.

   *2.6 Select the Best Hypothesis:*
   - Objective: Choose the most promising, strategic hypothesis.
   - Reflection: "Why does this hypothesis stand out? How does it uniquely address the issue?"
   - Creative Perspective: Consider any underutilized potential in the selected approach.

   *2.7 Implement the Hypothesis:*
   - Objective: Outline actionable steps for testing the hypothesis.
   - Reflection: "Is this plan practical? What resources or preparation are required?"
   - Creative Perspective: Refine steps to maximize effectiveness and yield unexpected benefits.

   *2.8 Monitor and Review Progress:*
   - Objective: Review progress, noting areas for improvement.
   - Reflection: "What’s working well? What could be improved?"
   - Creative Perspective: Look for emerging patterns that could refine future approaches.

   *2.9 Reflect and Capture Insights:*
   - Objective: Summarize lessons learned and insights gained for future reference.
   - Reflection: "What new understanding has emerged from this process?"
   - Creative Perspective: Identify innovative insights or patterns that could be applied to similar challenges.

3. *Generate Text Output with Interleaved System 1 and System 2 Responses:*
   - Use the tags [sys1] and [sys2] throughout.
   - Aim for a lengthier, detailed response. Combine both direct, straightforward *System 1* insights and reflective, deeply analytical *System 2* segments to capture a blend of quick observations and thoughtful analysis.

---

### *Example Input Text:*

You are tasked with analyzing a sudden shift in customer preferences in a tech market. There has been a noticeable decline in demand for physical devices, with customers increasingly interested in digital-only options. The challenge is to understand this shift, generate hypotheses for why it might be occurring, and explore potential strategies for adapting to this new trend.

---

### *Processed Output with System 1 and System 2 Thinking:*

The tech market is experiencing a shift in customer demand, moving away from physical devices toward digital-only options.

[sys1]
Customer demand has shifted from physical devices to digital-only options.
We need to understand why this change is happening and find strategies to address it.
Key factors may include cost, convenience, and technological trends.
[end sys1]

[sys2]
**2.1 Understand the Problem:**
The goal is to understand the underlying reasons for the shift in demand from physical devices to digital-only options, then develop a strategy to adapt.

*Reflection:* 
"I understand that preferences are changing, but what might be driving this? Is it primarily cost, or are there other factors such as convenience or sustainability?"

*Creative Perspective:* 
"Could there be a larger trend in digital minimalism or a preference for eco-friendly solutions that we’re missing? What unseen motivations might explain this shift?"

**2.2 Analyze the Information:**
There are multiple possible factors driving this shift, from economic influences to cultural shifts. It’s essential to isolate each factor and understand its impact.

*Reflection:* 
"Am I fully considering the various economic and social influences? Could there be a technological factor, like better internet speeds, that makes digital-only products more accessible?"

*Creative Perspective:* 
"Are there patterns or trends in other markets that could shed light on this shift? Could this be part of a larger trend toward virtual experiences?"

**2.3 Generate Hypotheses:**
1. Customers prefer digital options due to lower costs. (Confidence: 0.8, Creative: 0.4)
2. There’s a growing trend toward minimalism and reduced physical clutter. (Confidence: 0.7, Creative: 0.7)
3. Digital products offer greater flexibility and ease of use. (Confidence: 0.6, Creative: 0.6)
4. Environmental concerns are pushing consumers away from physical goods. (Confidence: 0.6, Creative: 0.8)
5. Advances in tech make digital-only options more functional. (Confidence: 0.8, Creative: 0.5)
6. Pandemic-era remote work increased demand for digital solutions. (Confidence: 0.7, Creative: 0.6)
7. Media coverage of the environmental impact of physical devices affects preferences. (Confidence: 0.5, Creative: 0.7)
8. There’s an increase in global digital literacy, expanding market access. (Confidence: 0.6, Creative: 0.6)
9. Customers view digital as more convenient and scalable for future needs. (Confidence: 0.7, Creative: 0.5)
10. Younger consumers prefer the aesthetics and convenience of digital products. (Confidence: 0.6, Creative: 0.6)

*Reflection:* 
"Have I considered all possible influences? Are there any surprising factors that could explain this shift?"

*Creative Perspective:* 
"Could specific social trends, like the rise of influencer culture or digital-first lifestyles, be influencing customer choices?"

**2.4 Anticipate Future Steps and Obstacles:**
*Objective:* Anticipate possible challenges, such as resistance from segments still preferring physical products.

*Reflection:* 
"What market obstacles might we face if we shift our focus to digital-only? Are there sub-segments that still prioritize physical products?"

*Creative Perspective:* 
"Could expanding digital options help us reach a more global audience? Are there emerging trends that we could leverage in our strategy?"

[end sys2]

[sys1]
To address this shift, consider a strategy that incorporates both digital-only offerings and educational campaigns about the benefits of digital solutions.
Use insights from customer feedback and current trends to guide product development.
Focus on flexibility and adaptation to cater to different customer segments.
[end sys1]


(* Interactive use

  app load ["Omega_AutomataTheory", "numLib"];
  open Rsyntax

*)
structure temporalLib :> temporalLib =
struct

(*---------------------------------------------------------------------------
   Note (kxs): the pathname and file handling in this file should be
               made portable.
 ---------------------------------------------------------------------------*)

val smv_tmp_dir = ref "/tmp/";

open HolKernel Parse boolLib Rsyntax;

infixr 3 -->;
infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL;

local open Omega_AutomataTheory in end;

val ERR = Feedback.mk_HOL_ERR "temporalLib"

local  (* Fix the grammar used by this file *)
  val ambient_grammars = Parse.current_grammars();
  val _ = Parse.temp_set_grammars Omega_AutomataTheory.Omega_Automata_grammars
in

type smv_output =
        {Proved:bool,
         Init_Sequence:(string list * string list) list,
         Loop_Sequence:(string list * string list) list,
         Resources:string list}


datatype temp_formula =
        truesig |
        falsesig |
        var of string |
        neg of temp_formula |
        conj of (temp_formula * temp_formula) |
        disj of (temp_formula * temp_formula) |
        imp  of (temp_formula * temp_formula) |
        equ  of (temp_formula * temp_formula) |
        ifte of (temp_formula * temp_formula * temp_formula) |
        next of temp_formula |
        always of temp_formula |
        eventual of temp_formula |
        when of (temp_formula * temp_formula) |
        swhen of (temp_formula * temp_formula) |
        until of (temp_formula * temp_formula) |
        suntil of (temp_formula * temp_formula) |
        befor of (temp_formula * temp_formula) |
        sbefor of (temp_formula * temp_formula) |
        pnext of temp_formula |
        psnext of temp_formula |
        palways of temp_formula |
        peventual of temp_formula |
        pwhen of (temp_formula * temp_formula) |
        pswhen of (temp_formula * temp_formula) |
        puntil of (temp_formula * temp_formula) |
        psuntil of (temp_formula * temp_formula) |
        pbefor of (temp_formula * temp_formula) |
        psbefor of (temp_formula * temp_formula);





(* ----------------------------------------------------------------------
    Converting functions: hol2temporal & temporal2hol
   ---------------------------------------------------------------------- *)
val thetrue   = T
val thefalse  = F
val NEXT      = Term`NEXT`
val ALWAYS    = Term`ALWAYS`
val EVENTUAL  = Term`EVENTUAL`
val PNEXT     = Term`PNEXT`
val PSNEXT    = Term`PSNEXT`
val PALWAYS   = Term`PALWAYS`
val PEVENTUAL = Term`PEVENTUAL`
val WHEN      = Term`$WHEN`
val UNTIL     = Term`$UNTIL`
val BEFORE    = Term`$BEFORE`
val SWHEN     = Term`$SWHEN`
val SUNTIL    = Term`$SUNTIL`
val SBEFORE   = Term`$SBEFORE`
val PWHEN     = Term`$PWHEN`
val PUNTIL    = Term`$PUNTIL`
val PBEFORE   = Term`$PBEFORE`
val PSWHEN    = Term`$PSWHEN`
val PSUNTIL   = Term`$PSUNTIL`
val PSBEFORE  = Term`$PSBEFORE`

fun hol2temporal t =
  if t~~thetrue then truesig else if t~~thefalse then falsesig
  else
    (let val {Name=n,Ty=typ} = dest_var t
      in var(n)
     end)
  handle _=> (* ----- signal abstraction *)
    (let val {Bvar=v,Body=b} = dest_abs t
         val {Name=n,Ty=_} = dest_var v
      in (hol2temporal b)
     end)
  handle _=> (* ----- propositional or temporal operator or signal evaluation *)
    (let val t1 = dest_neg t
      in neg(hol2temporal t1)
     end)
  handle _=>
    (let val {conj1=t1,conj2=t2} = dest_conj t
      in conj((hol2temporal t1),(hol2temporal t2))
     end)
  handle _=>
    (let val {disj1=t1,disj2=t2} = dest_disj t
      in disj((hol2temporal t1),(hol2temporal t2))
     end)
  handle _=>
    (let val {ant=t1,conseq=t2} = dest_imp t
      in imp((hol2temporal t1),(hol2temporal t2))
     end)
  handle _=>
    (let val {lhs=t1,rhs=t2} = dest_eq t
      in equ((hol2temporal t1),(hol2temporal t2))
     end)
  handle _=>
    (let val {cond=t1,larm=t2,rarm=t3} = dest_cond t
      in ifte((hol2temporal t1),(hol2temporal t2),(hol2temporal t3))
     end)
  handle _=> (* ----- temporal operator or signal evalutation *)
    (let val {Rator=f,Rand=x} = dest_comb t
      in if f~~NEXT then next(hol2temporal x)
         else if f~~ALWAYS then always(hol2temporal x)
         else if f~~EVENTUAL then eventual(hol2temporal x)
         else if f~~PNEXT then pnext(hol2temporal x)
         else if f~~PSNEXT then psnext(hol2temporal x)
         else if f~~PALWAYS then palways(hol2temporal x)
         else if f~~PEVENTUAL then peventual(hol2temporal x)
         else(* ----- binary temporal operator or signal evalutation *)
            let val {Rator=temp_op,Rand=b} = dest_comb f
             in if temp_op ~~ WHEN then
                        when((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ UNTIL then
                        until((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ BEFORE then
                        befor((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ SWHEN then
                        swhen((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ SUNTIL then
                        suntil((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ SBEFORE then
                        sbefor((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ PWHEN then
                        pwhen((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ PUNTIL then
                        puntil((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ PBEFORE then
                        pbefor((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ PSWHEN then
                        pswhen((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ PSUNTIL then
                        psuntil((hol2temporal b),(hol2temporal x))
                else if temp_op ~~ PSBEFORE then
                        psbefor((hol2temporal b),(hol2temporal x))
                else (hol2temporal f)
            end
          handle _=> (hol2temporal f)
     end)




fun temporal2hol truesig  = “\t:num.T”
  | temporal2hol falsesig = “\t:num.F”
  | temporal2hol (var(x)) = mk_var{Name=x,Ty=(==`:num->bool`==)}
  | temporal2hol (neg f)  =
        let val t = temporal2hol f in “\t:num. ~^t t” end
  | temporal2hol (conj(f1,f2)) =
        let
           val t1 = temporal2hol f1
           val t2 = temporal2hol f2
         in “\t:num. ^t1 t /\ ^t2 t”
        end
  | temporal2hol (disj(f1,f2)) =
        let
           val t1 = temporal2hol f1
           val t2 = temporal2hol f2
         in “\t:num. ^t1 t \/ ^t2 t”
        end
  | temporal2hol (imp(f1,f2)) =
        let
           val t1 = temporal2hol f1
           val t2 = temporal2hol f2
         in “\t:num. ^t1 t ==> ^t2 t”
        end
  | temporal2hol (equ(f1,f2)) =
        let
           val t1 = temporal2hol f1
           val t2 = temporal2hol f2
         in “\t:num. ^t1 t = ^t2 t”
        end
  | temporal2hol (ifte(f1,f2,f3)) =
        let
           val t1 = temporal2hol f1
           val t2 = temporal2hol f2
           val t3 = temporal2hol f3
         in “\t:num. if ^t1 t then ^t2 t else ^t3 t”
        end
  | temporal2hol (next f) =
        mk_comb{Rator=NEXT,Rand=(temporal2hol f)}
  | temporal2hol (always f) =
        mk_comb{Rator=ALWAYS,Rand=(temporal2hol f)}
  | temporal2hol (eventual f) =
        mk_comb{Rator=EVENTUAL,Rand=(temporal2hol f)}
  | temporal2hol (pnext f) =
        mk_comb{Rator=PNEXT,Rand=(temporal2hol f)}
  | temporal2hol (psnext f) =
        mk_comb{Rator=PSNEXT,Rand=(temporal2hol f)}
  | temporal2hol (palways f) =
        mk_comb{Rator=PALWAYS,Rand=(temporal2hol f)}
  | temporal2hol (peventual f) =
        mk_comb{Rator=PEVENTUAL,Rand=(temporal2hol f)}
  | temporal2hol (when(x,b)) =
        mk_comb{Rator=mk_comb{Rator=WHEN,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (until(x,b)) =
        mk_comb{Rator=mk_comb{Rator=UNTIL,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (befor(x,b)) =
        mk_comb{Rator=mk_comb{Rator=BEFORE,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (swhen(x,b)) =
        mk_comb{Rator=mk_comb{Rator=SWHEN,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (suntil(x,b)) =
        mk_comb{Rator=mk_comb{Rator=SUNTIL,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (sbefor(x,b)) =
        mk_comb{Rator=mk_comb{Rator=SBEFORE,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (pwhen(x,b)) =
        mk_comb{Rator=mk_comb{Rator=PWHEN,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (puntil(x,b)) =
        mk_comb{Rator=mk_comb{Rator=PUNTIL,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (pbefor(x,b)) =
        mk_comb{Rator=mk_comb{Rator=PBEFORE,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (pswhen(x,b)) =
        mk_comb{Rator=mk_comb{Rator=PSWHEN,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (psuntil(x,b)) =
        mk_comb{Rator=mk_comb{Rator=PSUNTIL,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}
  | temporal2hol (psbefor(x,b)) =
        mk_comb{Rator=mk_comb{Rator=PSBEFORE,Rand=(temporal2hol x)},
                Rand=(temporal2hol b)}






(* ----------------------------------------------------------------------
              Computing the names of the variables
   ---------------------------------------------------------------------- *)
fun var_names truesig          = []
  | var_names falsesig         = []
  | var_names (var(x))         = [x]
  | var_names (neg f)          = var_names f
  | var_names (conj(f1,f2))    = (var_names f1)@(var_names f2)
  | var_names (disj(f1,f2))    = (var_names f1)@(var_names f2)
  | var_names (imp(f1,f2))     = (var_names f1)@(var_names f2)
  | var_names (equ(f1,f2))     = (var_names f1)@(var_names f2)
  | var_names (ifte(f1,f2,f3)) = (var_names f1)@(var_names f2)@(var_names f3)
  | var_names (next f)         = var_names f
  | var_names (always f)       = var_names f
  | var_names (eventual f)     = var_names f
  | var_names (when(x,b))      = (var_names x)@(var_names b)
  | var_names (until(x,b))     = (var_names x)@(var_names b)
  | var_names (befor(x,b))     = (var_names x)@(var_names b)
  | var_names (swhen(x,b))     = (var_names x)@(var_names b)
  | var_names (suntil(x,b))    = (var_names x)@(var_names b)
  | var_names (sbefor(x,b))    = (var_names x)@(var_names b)
  | var_names (pnext f)        = var_names f
  | var_names (psnext f)       = var_names f
  | var_names (palways f)      = var_names f
  | var_names (peventual f)    = var_names f
  | var_names (pwhen(x,b))     = (var_names x)@(var_names b)
  | var_names (puntil(x,b))    = (var_names x)@(var_names b)
  | var_names (pbefor(x,b))    = (var_names x)@(var_names b)
  | var_names (pswhen(x,b))    = (var_names x)@(var_names b)
  | var_names (psuntil(x,b))   = (var_names x)@(var_names b)
  | var_names (psbefor(x,b))   = (var_names x)@(var_names b)




(* ----------------------------------------------------------------------
                      Generating new variable names
   ---------------------------------------------------------------------- *)
fun new_sig_var name fb index =
    let val n = name^(int_to_string index)
     in if mem n fb then new_sig_var name fb (index+1)
        else n
    end



(* -------------- tsubst & temp_subst ---------------------------------------
    tsubst v x t replaces each occurence of v by x in the formula t (v
    need not be a variable). The function temp_subst is a multiple
    replacement, where the replacement is not done simulaneously. The
    function def_subst is a special variant that is needed in the
    tableau construction below.
   -------------------------------------------------------------------------- *)

fun tsubst v x t =
    if v=t then x else
      case t of
          falsesig       => falsesig
        | truesig        => truesig
        | var(n)         => var(n)
        | neg f          => neg(tsubst v x f)
        | conj(f1,f2)    => conj(tsubst v x f1,tsubst v x f2)
        | disj(f1,f2)    => disj(tsubst v x f1,tsubst v x f2)
        | imp(f1,f2)     => imp(tsubst v x f1,tsubst v x f2)
        | equ(f1,f2)     => equ(tsubst v x f1,tsubst v x f2)
        | ifte(f1,f2,f3) => ifte(tsubst v x f1,tsubst v x f2,tsubst v x f3)
        | next f         => next(tsubst v x f)
        | always f       => always(tsubst v x f)
        | eventual f     => eventual(tsubst v x f)
        | when(f1,f2)    => when(tsubst v x f1,tsubst v x f2)
        | until(f1,f2)   => until(tsubst v x f1,tsubst v x f2)
        | befor(f1,f2)   => befor(tsubst v x f1,tsubst v x f2)
        | swhen(f1,f2)   => swhen(tsubst v x f1,tsubst v x f2)
        | suntil(f1,f2)  => suntil(tsubst v x f1,tsubst v x f2)
        | sbefor(f1,f2)  => sbefor(tsubst v x f1,tsubst v x f2)
        | pnext f        => pnext(tsubst v x f)
        | psnext f       => psnext(tsubst v x f)
        | palways f      => palways(tsubst v x f)
        | peventual f    => peventual(tsubst v x f)
        | pwhen(f1,f2)   => pwhen(tsubst v x f1,tsubst v x f2)
        | puntil(f1,f2)  => puntil(tsubst v x f1,tsubst v x f2)
        | pbefor(f1,f2)  => pbefor(tsubst v x f1,tsubst v x f2)
        | pswhen(f1,f2)  => pswhen(tsubst v x f1,tsubst v x f2)
        | psuntil(f1,f2) => psuntil(tsubst v x f1,tsubst v x f2)
        | psbefor(f1,f2) => psbefor(tsubst v x f1,tsubst v x f2)

fun temp_subst [] t = t |
    temp_subst ((v,x)::sigma) t = temp_subst sigma (tsubst v x t)


fun def_subst [] t = t
  | def_subst (equ(ell,phi)::s) t = def_subst s (tsubst phi ell t)
  | def_subst _ _ = raise ERR "def_subst" "bind"



(* ----------------------------------------------------------------------
    The function tableau is described in my paper of TPHOL99. It
    essentially abbreviates any subformula that starts with a temporal
    operator with a new variable that is then hidden by an existential
    quantification. Special care has to be taken for the NEXT operator
    and the past temporal operators. For abbreviating past temporal
    operators, we must first apply one recursion step according to the
    recursion theorem for the corresponding past operator and
    abbreviate then the past next operator applied on the past
    operator. For the next operator, we use two state variable to
    compute really an automaton. See the theorem
    "TEMP_OPS_DEFS_TO_OMEGA" of the theory "Omega_Automata" for more
    details on the form of the abbreviations.
   --------------------------------------------------------------------- *)


val fb = ref([]:string list); (* contains the names of forbidden variables *)

fun tableau Phi =
    case Phi of
          var(_)        => ([],Phi)
        | neg phi       =>
                let val (defs,phi') = tableau phi
                 in (defs,neg(phi'))
                end
        | conj(phi,psi) =>
                let val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                 in (defs1 @ defs2,conj(phi',psi'))
                end
        | disj(phi,psi) =>
                let val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                 in (defs1 @ defs2,disj(phi',psi'))
                end
        | imp(phi,psi)  =>
                let val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                 in (defs1 @ defs2,imp(phi',psi'))
                end
        | equ(phi,psi)  =>
                let val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                 in (defs1 @ defs2, equ(phi',psi'))
                end
        | ifte(phi,alpha,beta) =>
                let val (defs1,phi') = tableau phi
                    val (defs2,alpha') = tableau (def_subst defs1 alpha)
                    val (defs3,beta')  =
                           tableau (def_subst (defs1 @ defs2) beta)
                 in (defs1 @ defs2 @ defs3,ifte(phi',alpha',beta'))
                end
        | next phi =>
                let
                    val (defs,phi') = tableau phi
                    val ell0_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell0_name::(!fb) )
                    val ell1_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell1_name::(!fb) )
                    val ell0 = var(ell0_name)
                    val ell1 = var(ell1_name)
                    val def0 = equ(ell0,phi')
                    val def1 = equ(ell1,next(ell0))
                 in ( defs @ [def0,def1], ell1)
                end
        | always phi =>
                let
                    val (defs,phi') = tableau phi
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,always(phi'))
                 in (defs @ [def], ell)
                end
        | eventual phi =>
                let
                    val (defs,phi') = tableau phi
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,eventual(phi'))
                 in (defs @ [def], ell)
                end
        | when(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,when(phi',psi'))
                 in (defs1 @ defs2 @ [def], ell)
                end
        | until(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,until(phi',psi'))
                 in (defs1 @ defs2 @ [def], ell)
                end
        | befor(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,befor(phi',psi'))
                 in (defs1 @ defs2 @ [def], ell)
                end
        | swhen(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,swhen(phi',psi'))
                 in (defs1 @ defs2 @ [def], ell)
                end
        | suntil(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,suntil(phi',psi'))
                 in (defs1 @ defs2 @ [def], ell)
                end
        | sbefor(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,sbefor(phi',psi'))
                 in (defs1 @ defs2 @ [def], ell)
                end
        | pnext phi =>
                let
                    val (defs,phi') = tableau phi
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,pnext(phi'))
                 in (defs @ [def], ell)
                end
        | psnext phi =>
                let
                    val (defs,phi') = tableau phi
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,psnext(phi'))
                 in (defs @ [def], ell)
                end
        | palways phi =>
                let
                    val (defs,phi') = tableau phi
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,pnext(palways(phi')))
                 in (defs @ [def], conj(phi',ell))
                end
        | peventual phi =>
                let
                    val (defs,phi') = tableau phi
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,psnext(peventual(phi')))
                 in (defs @ [def], disj(phi',ell))
                end
        | pwhen(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,pnext(pwhen(phi',psi')))
                 in (
                     defs1 @ defs2 @ [def],
                     disj(conj(phi,psi),conj(neg(psi),ell))
                    )
                end
        | puntil(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,pnext(puntil(phi',psi')))
                 in (
                     defs1 @ defs2 @ [def],
                     disj(psi',conj(phi',ell))
                    )
                end
        | pbefor(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,pnext(pbefor(phi',psi')))
                 in (
                     defs1 @ defs2 @ [def],
                     conj(neg(psi'),disj(phi',ell))
                    )
                end
        | pswhen(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,psnext(pswhen(phi',psi')))
                 in (
                     defs1 @ defs2 @ [def],
                     disj(conj(phi,psi),conj(neg(psi),ell))
                    )
                end
        | psuntil(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,psnext(psuntil(phi',psi')))
                 in (
                     defs1 @ defs2 @ [def],
                     disj(psi',conj(phi',ell))
                    )
                end
        | psbefor(phi,psi) =>
                let
                    val (defs1,phi') = tableau phi
                    val (defs2,psi') = tableau (def_subst defs1 psi)
                    val ell_name = new_sig_var "ell" (!fb) 0
                    val u = (fb := ell_name::(!fb) )
                    val ell = var(ell_name)
                    val def = equ(ell,psnext(psbefor(phi',psi')))
                 in (
                     defs1 @ defs2 @ [def],
                     conj(neg(psi'),disj(phi',ell))
                    )
                end
        | truesig => ([],truesig)
        | falsesig => ([],falsesig)







(* ----------------------------------------------------------------------

    Based on the above function, the conversion TEMP_DEFS_CONV proves
    now the equivalence between the term with the local abbreviations
    and the given LTL formula. Note that the given LTL formula must be
    of the form ALWAYS phi 0, i.e., we only deal with initial
    equivalence, which is necessary for the past operators.
   ----------------------------------------------------------------------

   new_theory "ltltest";
   new_parent "Omega_Automata";
   TEMP_DEFS_CONV “ALWAYS (\t. (EVENTUAL a) t = a t \/ NEXT (EVENTUAL a) t) 0”;
   val it =
     |- ALWAYS (\t. EVENTUAL a t = a t \/ NEXT (EVENTUAL a) t) 0 =
        (?ell0 ell1 ell2 ell3 ell4.
          ell4 0 /\
          (ell0 = EVENTUAL a) /\
          (ell1 = EVENTUAL a) /\
          (ell2 = ell1) /\
          (ell3 = NEXT ell2) /\
          (ell4 = ALWAYS (\t. ell0 t = a t \/ ell3 t))) : thm

   TEMP_DEFS_CONV “ALWAYS (EVENTUAL (\t. a t /\ PALWAYS b t)) 0”;
   val it =
     |- ALWAYS (EVENTUAL (\t. a t /\ PALWAYS b t)) 0 =
        (?ell0 ell1 ell2.
          ell2 0 /\
          (ell0 = PNEXT (PALWAYS b)) /\
          (ell1 = EVENTUAL (\t. a t /\ b t /\ ell0 t)) /\
          (ell2 = ALWAYS ell1)) : thm

   ---------------------------------------------------------------------- *)

(* ---------------------------------------------------------------------------
   In the following, we have to deal with goals of the following form
                asm |- (?l1'...ln'. /\_{i=1^k} phi_i ) ==> Phi.
   Clearly, we should apply STRIP_TAC to reduce this to the following subgoal:
                [phi_1,...,phi_k] @ asm |- Phi
   However, STRIP_TAC is painfully slow, as the number of quantified variables
   may be larger than 50. Hence, we use a more specialized and more efficient
   tactic here to do the reduction. Do not replace it with STRIP_TAC.
   -------------------------------------------------------------------------- *)

fun MY_STRIP_TAC (asm,g) =
    let val {ant=a,conseq=Phi} = dest_imp g
     in
        (REPEAT ((CONV_TAC LEFT_IMP_EXISTS_CONV) THEN GEN_TAC)
         THEN DISCH_TAC
         THEN POP_ASSUM (fn x=> MAP_EVERY ASSUME_TAC (CONJUNCTS x))
        )
        (asm,g)
    end



val boolean_sig_ops = TAC_PROOF(
        ([],“
                ? s_not s_and s_or s_imp s_equiv s_ifte.
                     (!a b c.
                        ( (s_not a) = \t:num. ~a t) /\
                        ( s_and a b = \t:num. (a t /\ b t) ) /\
                        ( s_or a b  = \t:num. (a t \/ b t) ) /\
                        ( s_imp a b = \t:num. (a t ==> b t) ) /\
                        ( s_equiv a b = \t:num. (a t = b t) ) /\
                        ( s_ifte a b c = \t:num. (if a t then b t else c t))
                     )
                    /\
                     (!a b c.
                        (!t:num. ~a t = (s_not a) t) /\
                        (!t:num. (a t /\ b t)  = s_and a b t) /\
                        (!t:num. (a t \/ b t)  = s_or a b t) /\
                        (!t:num. (a t ==> b t) = s_imp a b t) /\
                        (!t:num. (a t = b t)   = s_equiv a b t) /\
                        (!t:num. (if a t then b t else c t) = s_ifte a b c t)
                     )
        ”),
        EXISTS_TAC “\a.\t:num.~a t”
        THEN EXISTS_TAC “\a b.\t:num. a t /\ b t”
        THEN EXISTS_TAC “\a b.\t:num. a t \/ b t”
        THEN EXISTS_TAC “\a b.\t:num. a t ==> b t”
        THEN EXISTS_TAC “\a b.\t:num. (a t):bool = b t”
        THEN EXISTS_TAC “\a b c.\t:num. if a t then (b t):bool else c t”
        THEN CONV_TAC(DEPTH_CONV FUN_EQ_CONV) THEN BETA_TAC
        THEN REPEAT GEN_TAC THEN REWRITE_TAC[])



fun PAST_RECURSION_TAC (asm,g) =
    let fun tll 0 l = l
          | tll n (e::l) = tll (n-1) l
          | tll _ _ = raise ERR "PAST_RECURSION_TAC" "bind"
        val rec_thm = Past_Temporal_LogicTheory.RECURSION
        val past_rec_thms = (map (GEN_ALL o SYM) (tll 8 (CONJUNCTS rec_thm)))
     in
       (
        MAP_EVERY ASSUME_TAC past_rec_thms
        THEN MAP_EVERY (UNDISCH_TAC o concl) past_rec_thms
        THEN ASSUME_TAC boolean_sig_ops
        THEN UNDISCH_TAC (concl boolean_sig_ops) THEN STRIP_TAC
        THEN POP_ASSUM (fn x => REWRITE_TAC[x])
        THEN CONV_TAC(DEPTH_CONV ETA_CONV)
        THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x])
        THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x])
        THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x])
        THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x])
        THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x])
        THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x])
        THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x])
        THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x])
        THEN POP_ASSUM (fn x => REWRITE_TAC[x])
       ) (asm,g)
    end


fun TEMP_DEFS_CONV t =
    let
        (* ------------------------------------------------------------------
            First we construct the goal that is to be proved. For this
            reason, we invoke the function tableau above and generate
            the corresponding hol term.
           ------------------------------------------------------------------ *)
        val tt = hol2temporal t
        val u = (fb := var_names tt)
        val (defs,pt) = tableau tt
        fun eta_conv t = (* ----- transforms "\t. ell t" to "ell" ----- *)
            let val {Bvar=x,Body=b} = dest_abs t
                val {Rator=ell,Rand=y} = dest_comb b
             in if(x~~y) then ell else t
            end
        fun fun_eta_conv t =
            (* - transforms "\t. ell t = phi" to "ell = \t. phi" ----- *)
            let val {Bvar=x,Body=b} = dest_abs t
                val {lhs=l,rhs=r} = dest_eq b
                val ell = rator l
                val new_r = mk_abs{Bvar=x,Body=r}
             in mk_eq{lhs=ell,rhs=(eta_conv new_r)}
            end
        fun beta_conv t =
            rhs(concl ((QCONV (REPEATC (DEPTH_CONV BETA_CONV))) t))
        val hdefs = map (fun_eta_conv o temporal2hol) defs
        val hpt = mk_comb{Rator=(temporal2hol pt),Rand=“0”}
        val hpt = beta_conv hpt
        val hdefs = map beta_conv hdefs
        val varnames = map lhs hdefs
        val defterm = (list_mk_conj hdefs)
        val tt = list_mk_exists(varnames,mk_conj{conj1 = hpt, conj2 = defterm})
        val goal = ([],“^t = ^tt”) : goal
        (* ----------------------------------------------------------------
            Having constructed the goal, we define now the tactic that
            solves this goal.
           ----------------------------------------------------------------- *)
        fun flatten_defs [] = [] |
            flatten_defs (d::dl) =
                let val (ell,phi) =
                        case d of equ(ell,phi) => (ell,phi)
                                | _ => raise ERR "TEMP_DEFS_CONV" ""
                 in d::(map (tsubst ell phi) (flatten_defs dl))
                end
        val flat_hdefs = map (fun_eta_conv o temporal2hol) (flatten_defs defs)
        val inst_list = map rhs flat_hdefs
        val tac =
            EQ_TAC
            THENL[
                DISCH_TAC
                THEN MAP_EVERY EXISTS_TAC inst_list THEN BETA_TAC
                THEN UNDISCH_TAC t
                THEN PAST_RECURSION_TAC,
                MY_STRIP_TAC
                THEN UNDISCH_TAC hpt THEN ASM_REWRITE_TAC[] THEN BETA_TAC
                THEN PAST_RECURSION_TAC
                ]
     in TAC_PROOF(goal, tac)
    end;





fun UNSAFE_TEMP_DEFS_CONV t =
    let
        (* ---------------------------------------------------------------
            First we construct the goal that is to be proved. For this
            reason, we invoke the function tableau above and generate the
            corresponding hol term.
           --------------------------------------------------------------- *)
        val tt = hol2temporal t
        val u = (fb := var_names tt)
        val (defs,pt) = tableau tt
        fun eta_conv t = (* ----- transforms "\t. ell t" to "ell" ----- *)
            let val {Bvar=x,Body=b} = dest_abs t
                val {Rator=ell,Rand=y} = dest_comb b
             in if(x~~y) then ell else t
            end
        fun fun_eta_conv t =
            (* ----- transforms "\t. ell t = phi" to "ell = \t. phi" ----- *)
            let val {Bvar=x,Body=b} = dest_abs t
                val {lhs=l,rhs=r} = dest_eq b
                val ell = rator l
                val new_r = mk_abs{Bvar=x,Body=r}
             in mk_eq{lhs=ell,rhs=(eta_conv new_r)}
            end
  fun beta_conv t = rhs(concl ((QCONV (REPEATC (DEPTH_CONV BETA_CONV))) t))
        val hdefs = map (fun_eta_conv o temporal2hol) defs
        val hpt = mk_comb{Rator=(temporal2hol pt),Rand=“0”}
        val hpt = beta_conv hpt
        val hdefs = map beta_conv hdefs
        val varnames = map lhs hdefs
        val defterm = (list_mk_conj hdefs)
        val tt = list_mk_exists(varnames,mk_conj{conj1 = hpt, conj2 = defterm})
        val goal = ([],“^t = ^tt”) : goal
     in mk_thm goal
    end




(* ----------------------------------------------------------------------

     The conversion LTL2OMEGA_CONV finally does what its name indicates.
     Given an LTL formula in the form as mentioned in the comment on the
     conversion TEMP_DEFS_CONV, LTL2OMEGA_CONV computes an equivalent
     generalized Büchi automaton and proves the equivalence with the   (* UOK *)
     given LTL formula.

   ----------------------------------------------------------------------
   LTL2OMEGA_CONV
      ``ALWAYS (\t. (EVENTUAL a) t = a t \/ NEXT (EVENTUAL a) t) 0``;
   val it =
     |- ALWAYS (\t. EVENTUAL a t = a t \/ NEXT (EVENTUAL a) t) 0 =
        (?ell0 ell1 ell2 ell3 ell4.
          ell4 0 /\
          (!t.
            (ell0 t = a t \/ ell0 (SUC t)) /\
            (ell1 t = a t \/ ell1 (SUC t)) /\
            (ell2 t = ell1 t) /\
            (ell3 t = ell2 (SUC t)) /\
            (ell4 t = (ell0 t = a t \/ ell3 t) /\ ell4 (SUC t))) /\
          (!t1. ?t2. ell0 (t1 + t2) ==> a (t1 + t2)) /\
          (!t1. ?t2. ell1 (t1 + t2) ==> a (t1 + t2)) /\
          (!t1.
            ?t2.
              (ell0 (t1 + t2) = a (t1 + t2) \/ ell3 (t1 + t2)) ==>
              ell4 (t1 + t2))) : thm

   LTL2OMEGA_CONV ``ALWAYS (EVENTUAL (\t. a t /\ PALWAYS b t)) 0``;
   val it =
     |- ALWAYS (EVENTUAL (\t. a t /\ PALWAYS b t)) 0 =
        (?ell0 ell1 ell2.
          (ell2 0 /\ ell0 0) /\
          (!t.
            (ell0 (SUC t) = b t /\ ell0 t) /\
            (ell1 t = a t /\ b t /\ ell0 t \/ ell1 (SUC t)) /\
            (ell2 t = ell1 t /\ ell2 (SUC t))) /\
          (!t1.
            ?t2.
              ell1 (t1 + t2) ==>
                a (t1 + t2) /\ b (t1 + t2) /\ ell0 (t1 + t2)) /\
          (!t1. ?t2. ell1 (t1 + t2) ==> ell2 (t1 + t2))) : thm

   ---------------------------------------------------------------------- *)



fun LTL2OMEGA_CONV t =
    let
        val future_temp_ops = constants "Temporal_Logic"
        val past_temp_ops = constants "Past_Temporal_Logic"
        val temp_ops = future_temp_ops @ past_temp_ops
        fun elem 0 l = hd l
          | elem i l = elem (i-1) (tl l)
        fun delete 0 (e::l) = l
          | delete i (e::l) = (e::(delete (i-1) l))
          | delete _ _ = raise ERR "LTL2OMEGA_CONV" ""
        fun get_constants t =
            if (is_var t) then []
            else if (is_const t) then [t]
            else if (is_abs t) then get_constants(body t)
            else (* its a function application *)
                let val {Rator=f,Rand=x} = dest_comb t
                 in (get_constants f) @ (get_constants x)
                end
        fun is_prop t = null((op_intersect aconv (get_constants t) temp_ops))
        val def2omega_thms =
            CONJUNCTS Omega_AutomataTheory.TEMP_OPS_DEFS_TO_OMEGA
        val past_nx_thms = [elem 9 def2omega_thms,elem 10 def2omega_thms]
        val def2omega_thms = delete 9 (delete 10 def2omega_thms)
        fun def2omega def =
            if (is_prop def) then
                let val {lhs=ell,rhs=phi} = dest_eq def
                 in (“T”,“!t:num. ^ell t = ^phi t”,“T”)
                end
            else
                let val thm = ((PURE_REWRITE_CONV def2omega_thms) THENC
                               (PURE_REWRITE_CONV past_nx_thms)) def
                    val r = rhs(concl thm)
                    val {conj1=init_condition,conj2=rest} = dest_conj r
                    val {conj1=trans_rel,conj2=accept} = dest_conj rest
                 in (init_condition,trans_rel,accept)
                end
        val simplify_conv =
            rhs o concl o ((DEPTH_CONV BETA_CONV) THENC (REWRITE_CONV[]))
        val thm0 = TEMP_DEFS_CONV t
        val defterm = rhs(concl thm0)
        val (dvars,rest) = strip_exists defterm
        val restlist = strip_conj rest
        val init_cond = hd restlist
        val defs = tl restlist
        val omega_list = map def2omega defs
        val init_condition = list_mk_conj (map (fn (x,y,z) => x) omega_list)
        val trans_rel =
            list_mk_conj (map (fn (x,y,z) => #Body(dest_forall y)) omega_list)
        val acceptance = list_mk_conj (map (fn (x,y,z) => z) omega_list)
        val init_condition = mk_conj{conj1=init_cond, conj2=init_condition}
        val trans_rel = mk_forall{Bvar=“t:num”,Body=trans_rel}
        val init_condition = simplify_conv init_condition
        val trans_rel      = simplify_conv trans_rel
        val acceptance     = simplify_conv acceptance
        val automaton_kernel = list_mk_conj[init_condition,trans_rel,acceptance]
        val automaton = list_mk_exists(dvars,automaton_kernel)
        val goal = ([],mk_eq{lhs=defterm,rhs=automaton}):goal
        fun EX_TAC (asm,g) =
            let val {Bvar=x,Body=t} = dest_exists g
             in EXISTS_TAC x (asm,g)
            end
        val tac =
            PURE_REWRITE_TAC[(QCONV (REPEATC(DEPTH_CONV FORALL_AND_CONV)))
                               trans_rel]
            THEN REWRITE_TAC def2omega_thms
            THEN REWRITE_TAC past_nx_thms
            THEN (CONV_TAC(DEPTH_CONV FUN_EQ_CONV)) THEN BETA_TAC
            THEN REWRITE_TAC[]
            THEN EQ_TAC THEN MY_STRIP_TAC THEN REPEAT EX_TAC
            THEN RULE_ASSUM_TAC EQT_INTRO
            THEN ASM_REWRITE_TAC[]
        val thm1 = TAC_PROOF(goal,tac)
     in TRANS thm0 thm1
    end



fun UNSAFE_LTL2OMEGA_CONV t =
    let
        val future_temp_ops = constants "Temporal_Logic"
        val past_temp_ops = constants "Past_Temporal_Logic"
        val temp_ops = future_temp_ops @ past_temp_ops
        fun elem 0 l = hd l
          | elem i l = elem (i-1) (tl l)
        fun delete 0 (e::l) = l
          | delete i (e::l) = (e::(delete (i-1) l))
          | delete _ _ = raise ERR "UNSAFE_LTL2OMEGA_CONV" ""
        fun get_constants t =
            if (is_var t) then []
            else if (is_const t) then [t]
            else if (is_abs t) then get_constants(body t)
            else (* its a function application *)
                let val {Rator=f,Rand=x} = dest_comb t
                 in (get_constants f) @ (get_constants x)
                end
        fun is_prop t = null((op_intersect aconv (get_constants t) temp_ops))
        val def2omega_thms =
            CONJUNCTS Omega_AutomataTheory.TEMP_OPS_DEFS_TO_OMEGA
        val past_nx_thms = [elem 9 def2omega_thms,elem 10 def2omega_thms]
        val def2omega_thms = delete 9 (delete 10 def2omega_thms)
        fun def2omega def =
            if (is_prop def) then
                let val {lhs=ell,rhs=phi} = dest_eq def
                 in (“T”,“!t:num. ^ell t = ^phi t”,“T”)
                end
            else
                let val thm = ((PURE_REWRITE_CONV def2omega_thms) THENC
                               (PURE_REWRITE_CONV past_nx_thms)) def
                    val r = rhs(concl thm)
                    val {conj1=init_condition,conj2=rest} = dest_conj r
                    val {conj1=trans_rel,conj2=accept} = dest_conj rest
                 in (init_condition,trans_rel,accept)
                end
        val simplify_conv =
            rhs o concl o ((DEPTH_CONV BETA_CONV) THENC (REWRITE_CONV[]))
        val thm0 = UNSAFE_TEMP_DEFS_CONV t
        val defterm = rhs(concl thm0)
        val (dvars,rest) = strip_exists defterm
        val restlist = strip_conj rest
        val init_cond = hd restlist
        val defs = tl restlist
        val omega_list = map def2omega defs
        val init_condition = list_mk_conj (map (fn (x,y,z) => x) omega_list)
        val trans_rel =
            list_mk_conj (map (fn (x,y,z) => #Body(dest_forall y)) omega_list)
        val acceptance = list_mk_conj (map (fn (x,y,z) => z) omega_list)
        val init_condition = mk_conj{conj1=init_cond, conj2=init_condition}
        val trans_rel = mk_forall{Bvar=“t:num”,Body=trans_rel}
        val init_condition = simplify_conv init_condition
        val trans_rel      = simplify_conv trans_rel
        val acceptance     = simplify_conv acceptance
        val automaton_kernel = list_mk_conj[init_condition,trans_rel,acceptance]
        val automaton = list_mk_exists(dvars,automaton_kernel)
        val goal = ([],mk_eq{lhs=defterm,rhs=automaton}):goal
        val thm1 = mk_thm goal
     in TRANS thm0 thm1
    end

(* ----------------------------------------------------------------------
    The conversions TEMP_DEFS_CONV and LTL2OMEGA_CONV require that
    their input is a formula that is a boolean combination of formulas
    that start with a temporal operator that is applied to the initial
    point of time, i.e., to 0. Normally, users do not want to deal
    with such initial equivalences, but use formulas with free numeric
    variables and also with equations between signals. These formulas
    are brought into the normal form required by TEMP_DEFS_CONV and
    LTL2OMEGA_CONV with the following conversion. It is however not
    really a conversion, since it requires to quantify over the
    numeric free variables. If the user does not do this, a universal
    quantification is assumed.
   ---------------------------------------------------------------------- *)

(* Example:
   val t = “ (ALWAYS a t ==> EVENTUAL a t) /\
                (ALWAYS (EVENTUAL a) x ==> EVENTUAL (ALWAYS a) x) /\
                ( (\t. ~NEXT a t) = NEXT (\t. ~ a t) )
           ”;
   val it =
     |- (!t x.
          (ALWAYS a t ==> EVENTUAL a t) /\
          (ALWAYS (EVENTUAL a) x ==> EVENTUAL (ALWAYS a) x) /\
          ((\t. ~(NEXT a t)) = NEXT (\t. ~(a t)))) =
        ALWAYS (\t. ALWAYS a t ==> EVENTUAL a t) 0 /\
        ALWAYS (\x. ALWAYS (EVENTUAL a) x ==> EVENTUAL (ALWAYS a) x) 0 /\
        ALWAYS (\n. ~(NEXT a n) = NEXT (\t. ~(a t)) n) 0 : thm

*)


(* -------------------------------------------------------------------------
   Given a term t and a variable x that occurs free in t, the function closure
   finds the smallest subterm of t that contains x and quantify it depending on
   the flag exquan. This function is used to get rid of free numeric variables.
   ------------------------------------------------------------------------- *)

exception NOT_GOOD_FORMULA;

fun closure exquan x t =
            (let val {Name=_,Ty=_} = dest_var t
              in if x~~t then
                    if exquan then mk_exists{Bvar=x,Body=t}
                    else mk_forall{Bvar=x,Body=t}
                 else t
             end)
         handle _=>
            (let val {Name=_,Ty=_} = dest_const t
              in t
             end)
         handle _=>
            (let val {Bvar=y,Body=b} = dest_abs t
              in if x~~y then t
                 else mk_abs{Bvar=y,Body=(closure exquan x b)}
             end)
         handle _=>
            if (is_neg t) then mk_neg (closure (not exquan) x (dest_neg t))
            else if (is_conj t) then
                let val {conj1=t1,conj2=t2} = dest_conj t
                    val occ1 = memt (free_vars t1) x
                    val occ2 = memt (free_vars t2) x
                 in
                    if (occ1 andalso occ2) then
                        if exquan then mk_exists{Bvar=x,Body=t}
                        else mk_forall{Bvar=x,Body=t}
                    else if occ1 then
                        mk_conj{conj1=(closure exquan x t1),conj2=t2}
                    else if occ2 then
                        mk_conj{conj1=t1,conj2=(closure exquan x t2)}
                    else t
                end
            else if (is_disj t) then
                let val {disj1=t1,disj2=t2} = dest_disj t
                    val occ1 = memt (free_vars t1) x
                    val occ2 = memt (free_vars t2) x
                 in
                    if (occ1 andalso occ2) then
                        if exquan then mk_exists{Bvar=x,Body=t}
                        else mk_forall{Bvar=x,Body=t}
                    else if occ1 then
                        mk_disj{disj1=(closure exquan x t1),disj2=t2}
                    else if occ2 then
                        mk_disj{disj1=t1,disj2=(closure exquan x t2)}
                    else t
                end
            else if (is_imp t) then
                let val {ant=t1,conseq=t2} = dest_imp t
                    val occ1 = memt (free_vars t1) x
                    val occ2 = memt (free_vars t2) x
                 in
                    if (occ1 andalso occ2) then
                        if exquan then mk_exists{Bvar=x,Body=t}
                        else mk_forall{Bvar=x,Body=t}
                    else if occ1 then
                        mk_imp{ant=(closure (not exquan) x t1),conseq=t2}
                    else if occ2 then
                        mk_imp{ant=t1,conseq=(closure (not exquan) x t2)}
                    else t
                end
            else if (is_eq t) then
                let val {lhs=t1,rhs=t2} = dest_eq t
                    val occ1 = memt (free_vars t1) x
                    val occ2 = memt (free_vars t2) x
                 in
                    if (occ1 andalso occ2) then
                        if exquan then mk_exists{Bvar=x,Body=t}
                        else mk_forall{Bvar=x,Body=t}
                    else raise NOT_GOOD_FORMULA
                end
            else if (is_cond t) then
                let val {cond=t1,larm=t2,rarm=t3} = dest_cond t
                    val occ1 = memt (free_vars t1) x
                    val occ2 = memt (free_vars t2) x
                    val occ3 = memt (free_vars t3) x
                 in
                    if (occ1 andalso occ2 andalso occ3) then
                        if exquan then mk_exists{Bvar=x,Body=t}
                        else mk_forall{Bvar=x,Body=t}
                    else raise NOT_GOOD_FORMULA
                end
            else raise NOT_GOOD_FORMULA;




fun TEMP_NORMALIZE_CONV t =
    let
        (* --------------------------------------------------------------
            First we check whether there is a free numeric variable. If
            so, we choose one of them and universally quantify them and
            compute a prenex normal form. the function tableau above
            and generate the corresponding hol term.
           -------------------------------------------------------------- *)
        val num_vars = filter (fn x => (type_of x) = (==`:num`==)) (free_vars t)
        fun close_all [] t = t
          | close_all (x::vl) t = close_all vl (closure false x t)
        val t = close_all num_vars t
        val forall_always_thm = TAC_PROOF(
                ([],“!P. (!n. P n) = ALWAYS P 0”),
                REWRITE_TAC[Temporal_LogicTheory.ALWAYS]
                THEN BETA_TAC
                THEN REWRITE_TAC[arithmeticTheory.ADD_CLAUSES]);
        val exists_eventual_thm = TAC_PROOF(
                ([],“!P. (?n. P n) = EVENTUAL P 0”),
                REWRITE_TAC[Temporal_LogicTheory.EVENTUAL]
                THEN BETA_TAC
                THEN REWRITE_TAC[arithmeticTheory.ADD_CLAUSES]);
        fun QUAN_TEMP_CONV t =
            if is_forall t then
                let val b = rand t
                 in BETA_RULE(SPEC b forall_always_thm)
                end
            else if is_exists t then
                let val b = rand t
                 in BETA_RULE(SPEC b exists_eventual_thm)
                end
            else REFL t
        val thm1 = (QCONV
                ((DEPTH_CONV FUN_EQ_CONV) THENC
                 (DEPTH_CONV BETA_CONV) THENC
                 (DEPTH_CONV (CHANGED_CONV QUAN_TEMP_CONV))
                )) t
        val thm2 = Arith.PRENEX_CONV t
     in
        TRANS (SYM thm2) thm1
    end;





(* ----------------------------------------------------------------------
    The next functions deal with interfacing with the SMV system. The
    global variable print_states indicates that the state variables
    shall be printed. This is not always desired, since one often
    wants to have the input sequence of the model.
   ---------------------------------------------------------------------- *)

val print_states = ref false;


(* ------------------------ term2smv_string --------------------------------
    term2smv_string translates propositional terms in the atoms (p 0),
    (p t) and p(SUC t) into SMV syntax, where (p 0) and (p t) are both
    written as p and p(SUC t) is written as next(p) (this will only
    occur in the transition relation.
   ------------------------------------------------------------------------- *)


fun term2smv_string t =
    (let val {Name=n,Ty=typ} = dest_const t
      in if n="T" then "1" else if n="F" then "0" else n
     end)
  handle _=> (* -propositional or temporal operator or signal evalutation -*)
    (let val t1 = dest_neg t
      in "!"^(term2smv_string t1)
     end)
  handle _=>
    (let val {conj1=t1,conj2=t2} = dest_conj t
      in "("^(term2smv_string t1)^" & "^(term2smv_string t2)^")"
     end)
  handle _=>
    (let val {disj1=t1,disj2=t2} = dest_disj t
      in "("^(term2smv_string t1)^" | "^(term2smv_string t2)^")"
     end)
  handle _=>
    (let val {ant=t1,conseq=t2} = dest_imp t
      in "("^(term2smv_string t1)^" -> "^(term2smv_string t2)^")"
     end)
  handle _=>
    (let val {lhs=t1,rhs=t2} = dest_eq t
      in "("^(term2smv_string t1)^" <-> "^(term2smv_string t2)^")"
     end)
  handle _=>
    (let val {cond=t1,larm=t2,rarm=t3} = dest_cond t
         val p1 = term2smv_string t1
      in "((" ^ p1 ^ " & " ^ term2smv_string t2 ^ ") | (!" ^ p1 ^ " & " ^
         term2smv_string t3 ^ "))"
     end)
  handle _=>                  (* ------ signal evalutation ------------ *)
    (let val {Rator=f,Rand=x} = dest_comb t
      in if (is_var x) then #Name(dest_var f)
         else if (x~~“0”) then #Name(dest_var f)
         else if ((rator x)~~“SUC”) then
                "next("^(#Name(dest_var f))^")"
         else #Name(dest_var f)
     end)


fun genbuechi2smv_string b =
    let
        val (state_vars,kernel) = strip_exists b
        val {conj1=init_condition,conj2=rest} = dest_conj kernel
        val {conj1=transrel,conj2=accept} = dest_conj rest
        val inout_vars = free_vars b
        val vars = inout_vars @ state_vars
        fun var_list2smv [] = "" |
            var_list2smv (v::vl) =
                let val {Name=n,Ty=_} = dest_var v
                 in "   "^n^" : boolean;\n"^(var_list2smv vl)
                end
        fun acceptance [] = "" |
            acceptance (a::al) =
                let val {Bvar=_,Body=a1} = dest_forall a
                    val {Bvar=_,Body=a2} = dest_exists a1
                 in "\nFAIRNESS "^(term2smv_string a2)^(acceptance al)
                end
     in
        "MODULE main\n\n"^
        "VAR\n"^(var_list2smv vars)^"\n"^
        "TRANS \n"^(term2smv_string(#Body(dest_forall transrel)))^"\n\n"^
        (acceptance (strip_conj accept))^"\n\n"^
        "SPEC (EG TRUE) -> !"^(term2smv_string init_condition)^"\n\n"
    end;


fun hol2smv t =
    let val thm0 = TEMP_NORMALIZE_CONV (mk_neg t)
        val t0 = rhs(concl thm0)
        val thm1 = LTL2OMEGA_CONV t0
        val b = rhs(concl thm1)
     in
        genbuechi2smv_string b
    end




(* ----------------- interpret_smv_output -----------------------------------
    This function interpretes the output of smv, i.e. the string list
    is split up into a sequence of state descriptions and the proved
    flag and the resource information.
   -------------------------------------------------------------------------- *)

fun interpret_smv_output stl =
    let fun beginl [] l = true |
            beginl (e::s) [] = false |
            beginl (e1::s1) (e2::s2) = (e1=e2) andalso (beginl s1 s2)
        fun begins s1 s2 = beginl (explode s1) (explode s2)
        fun skip_lines [] = [] |
            skip_lines (e::l) = if (e = "\n") then skip_lines l
                                else if (begins "*** " e) then skip_lines l
                                else if (begins "WARNING *** " e) then
                                  skip_lines l
                                else (e::l)
        val stll = ref stl
        val proved =
            let val (l, ll) = Option.valOf (List.getItem (skip_lines (!stll)))
            in (stll := ll;
                beginl [#"\n",#"e",#"u",#"r",#"t"] (rev (explode l)))
                 (* ... is true *)
            end
        fun read_state_lines() = (* reading lines until empty line is read *)
            let val (l, ll) = Option.valOf (List.getItem (!stll))
                val _ = (stll := ll)
             in if l="\n" then []
                else l::(read_state_lines())
            end
        fun loop_starts() = beginl (explode "-- loop") (explode(hd(!stll)))
        fun resource_starts() = beginl (explode "resou") (explode(hd(!stll)))
        fun another_state() = beginl (explode "state") (explode(hd(!stll)))
        val init_sequence = ref ([]:string list list)
        val loop_sequence = ref ([]:string list list)
     in (if proved then ()
         else
            (stll := skip_lines(tl(!stll));
             while another_state() do
                (stll := tl(!stll);
                 init_sequence := (read_state_lines())::(!init_sequence);
                 stll := skip_lines(!stll));
             if loop_starts() then
                (stll := tl(!stll);
                 while another_state() do
                    (stll := tl(!stll);
                     loop_sequence := (read_state_lines())::(!loop_sequence);
                     stll := skip_lines(!stll)))
             else ());
         {Proved = proved,
          Init_Sequence = rev(!init_sequence),
          Loop_Sequence = if !loop_sequence=[] then []
                          else rev(tl(!loop_sequence)),
          Resources = skip_lines(!stll)})
    end

(* ----------------------------------------------------------------------
    Printing the countermodel on the terminal
   ---------------------------------------------------------------------- *)
fun print_smv_info smv_info =
    let val {Proved = proved,
             Init_Sequence = init_sequence,
             Loop_Sequence = loop_sequence,
             Resources = resources} = smv_info
        val state_count = ref 0;
        fun s_print (s:string) = print s
        fun print_state sa = s_print(String.concat sa)
        fun s_print_sequence [] = () |
            s_print_sequence (sa::sl) =
                (
                s_print ("================== State"^
                         int_to_string(!state_count));
                s_print ("==================\n");
                state_count := (!state_count) + 1;
                print_state sa;
                s_print_sequence sl
                )
     in if proved then
            (
             s_print "SMV has done the proof!\n";
             s_print (String.concat resources);
             ()
            )
        else
            (
             s_print "===============================================\n";
             s_print "Formula is not true! Consider the countermodel:\n";
             s_print "===============================================\n";
             s_print_sequence init_sequence;
             if loop_sequence=[] then ()
             else
                (
                 s_print "\n======== A loop starts here=============\n";
                 s_print_sequence loop_sequence
                );
             s_print "===============================================\n";
             s_print (String.concat resources);
             s_print "===============================================\n";
            ()
            )
    end



(* ***************************************************************************

   Given a generalized co-Büchi automaton, the conversion              (* UOK *)
   SMV_AUTOMATON_CONV checks for nonemptiness of the automaton. If the
   language accepted by the automaton is empty, the conversion
   generates the following theorem: |- (?a_1...a_n. automaton) = F,
   where a_1,...,a_n are the free variables of the given automaton
   formula. In case the language is not empty, the conversion will
   print out the countermodel that has been generated by SMV which
   shows a word that belongs to the language of the automaton.

   ************************************************************************* *)

fun SMV_RUN_FILE smv_file =
    let
  val _ = case OS.Process.getEnv "HOL4_SMV_EXECUTABLE" of
            SOME file =>
              Process.system (file ^ " " ^ smv_file ^ " > " ^
                              (!smv_tmp_dir) ^ "smv_out")
          | NONE =>
            raise Feedback.mk_HOL_ERR "SMV" smv_file
                ("SMV not configured: set the HOL4_SMV_EXECUTABLE environment" ^
                 "variable to point to the SMV executable file.")
  val file_in = TextIO.openIn ((!smv_tmp_dir) ^ "smv_out")
  val s = ref (TextIO.inputLine file_in)
  val sl = ref ([]:string list)
  val _ =
      while ((!s)<>NONE) do (sl:=(valOf (!s))::(!sl);
                             s:=TextIO.inputLine file_in)
  val _ = TextIO.closeIn file_in
  val p = interpret_smv_output(rev(!sl))
  val _ = Process.system ("rm " ^ (!smv_tmp_dir) ^ "smv_out")
     in
      if #Proved(p) then true
      else
        (print "SMV computes the following countermodel:\n";
          print_smv_info p;
          false
        )
    end

fun SMV_RUN smv_program =
  let
     val file_st = TextIO.openOut((!smv_tmp_dir)^"smv_file.smv")
     val _ = (
       TextIO.output(file_st,smv_program);
       TextIO.flushOut file_st;
       TextIO.closeOut file_st)
     val p = SMV_RUN_FILE ((!smv_tmp_dir) ^ "smv_file.smv")
  in
    (Process.system ("rm " ^ (!smv_tmp_dir)^"smv_file.smv"); p)
  end

fun SMV_AUTOMATON_CONV automaton =
  let
     val smv_program = genbuechi2smv_string automaton
     val proved = SMV_RUN smv_program
  in
    if (proved) then mk_thm([],mk_eq{lhs=automaton,rhs=“F”})
    else
      (NO_CONV “F”)
  end;


(* ----------------------------------------------------------------------
    Finally, we can combine all the stuff together.
   ---------------------------------------------------------------------- *)
fun LTL_CONV t =
    let val t0 = mk_neg t
        val thm0 = TEMP_NORMALIZE_CONV t0
        val t1 = rhs(concl thm0)
        val thm1 = LTL2OMEGA_CONV t1
        val automaton = rhs(concl thm1)
        val thm2 = SMV_AUTOMATON_CONV automaton
     in
        EQT_INTRO(REWRITE_RULE[](TRANS (TRANS thm0 thm1) thm2))
    end



fun UNSAFE_LTL_CONV t =
    let val t0 = mk_neg t
        val thm0 = TEMP_NORMALIZE_CONV t0
        val t1 = rhs(concl thm0)
        val thm1 = UNSAFE_LTL2OMEGA_CONV t1
        val automaton = rhs(concl thm1)
        val thm2 = SMV_AUTOMATON_CONV automaton
     in
        EQT_INTRO(REWRITE_RULE[](TRANS (TRANS thm0 thm1) thm2))
    end

val _ = Parse.temp_set_grammars ambient_grammars
end

end