Improve speed of PMATCH_INTRO_CONV and PMATCH_ELIM_CONV in patternMatchesLib #2052

Activity

1. mn200 commented on Sep 7, 2026

   

   mn200

   on Sep 7, 2026

   Member

   More actions

   Is this code much used? If not, I will mark this as low priority.
2. ordinarymath commented on Sep 7, 2026

   

   ordinarymath

   on Sep 7, 2026

   ContributorAuthor

   More actions

   PMATCH_ELIM_CONV is pretty much used for the pmatch theorems for CakeML definitions for the translator to use.

   
   Definition dest_Seq_def:
     (dest_Seq (Seq p1 p2) = (p1,p2:'a wordLang$prog)) /\
     (dest_Seq p = (Skip,p))
   End
   
   Theorem dest_Seq_pmatch:
     !p.
     dest_Seq p =
     pmatch p of
       Seq p1 p2 => (p1,p2:'a wordLang$prog)
      | p => (Skip,p)
   Proof
     rpt strip_tac
     >> CONV_TAC(RAND_CONV patternMatchesLib.PMATCH_ELIM_CONV)
     >> every_case_tac
     >> fs[dest_Seq_def]
   QED