You need to define a helper function that has as its state not only the llist that is being consumed but also a Boolean indicating whether or not to stop (because a P-satisfying element has been seen).
- - val until0_def = new_specification ("until0_def", ["until0"], ISPEC ``λbll. if FST bll then NONE else if SND bll = [||] then NONE else if P (THE (LHD (SND bll))) then SOME ((T, THE (LTL (SND bll))), THE (LHD (SND bll))) else SOME ((F, THE (LTL (SND bll))), THE (LHD (SND bll)))`` llist_Axiom_1 |> Q.GEN ‘P’ |> CONV_RULE (HO_REWR_CONV SKOLEM_THM)); val until0_T = until0_def |> Q.SPEC `P` |> Q.SPEC ‘(T, ll)’ |> SIMP_RULE (srw_ss()) [] val until0_FCONS = until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, h:::t)’ |> SIMP_RULE (srw_ss()) [] |> SIMP_RULE bool_ss [COND_RAND, Once COND_RATOR] |> SIMP_RULE bool_ss [Once COND_RATOR] |> SIMP_RULE (srw_ss()) [until0_T] val until0_FNIL = until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, [||])’ |> SIMP_RULE (srw_ss()) [] val until_def = Define‘until P ll = until0 P (F, ll)’ val until_thm = LIST_CONJ (map (SIMP_RULE bool_ss [GSYM until_def]) [until0_FNIL, until0_FCONS]) - - Michael From: Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net> Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk> Date: Tuesday, 7 August 2018 at 03:26 To: hol-info <hol-info@lists.sourceforge.net> Subject: [Hol-info] Partial Function on lazy list Hi all, Is there any easy way to define the following partial function on lazy list val recur_llist_fn_def = Define `recur_llist_fn P w = if P (THE (LHD w)) then [|THE (LHD w)|] else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`; Otherwise, I can also include the LNIL case as val recur_llist_fn_def = Define `recur_llist_fn P w = if (w = [||]) then [||] else if P (THE (LHD w)) then [|THE (LHD w)|] else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`; but I'm having issue to write its corresponding axiomatic form for llist_Axiom_1: !f. ?g. !x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a Particularly for P (THE (LHD w)) what will be SOME (?).... Any suggestion or thoughts? -- Waqar Ahmad, Ph.D. Post Doc at Hardware Verification Group (HVG) Department of Electrical and Computer Engineering Concordia University, QC, Canada Web: http://save.seecs.nust.edu.pk/waqar-ahmad/ ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info