SeLFiE: even more evaluation targets

[yutakang]

• [ ] Cantor_NF.thy in Zermelo Fraenkel Set Theory in Higher-Order Logic by Lawrence Paulson in 2019 has about 25 proofs by induction.
• [ ] Authenticated Data Structures As Functors by Andreas Lochbihler et al. in 2020 has about 28 proofs by induction
• [ ] Finger Trees by Benedikt Nordhoff in 2010 has about 65 proofs by induction
• [ ] Normalization by Evaluation by Klaus Aehlig et al. in 2008 has about 25 proofs by induction.
• [ ] Data_List.thy in HOLCF-Prelude by Joachim Breitner in 2017 has about 90 proofs by induction.
• [ ] OpSem.thy in PCF by Peter Gammie in 2012 has about 48 proofs by induction

In the alphabetical ordering,

• [ ] ADS_Functor -> ?
• [ ] Automatic_Refinement/Lib/Misc.thy
• [x] Binomial-Heaps/BinomialHeap.thy -> depends on SkewBinomialHeap.thy
• [x] Binomial-Heaps/SkewBinomialHeap.thy
• [x] Boolean
• [x] CoreC++/TypeSafe.thy
• [x] Depth-First-Search/DFS.thy
• [X] Finger-Trees/FingerTree.thy
• [x] Goodstein_Lambda/Goodstein_Lambda.thy
• [ ] HOLCF-Prelude/Data_List.thy -> depends on many files
• [x] Hybrid_Logic/Hybrid_Logic.thy
• [X] KBPs/Kripke.thy
• [x] KD_Tree/KD_Tree.thy
• [x] KD_Tree/Build.thy
• [x] KD_Tree/Nearest_Neighbors.thy -> depends on KD_Tree.thy
• [x] LTL/Disjunctive_Normal_Form.thy -> depends on LTL.thy and Equivalence_Relations.thy
• [x] NormByEval/NBE.thy
  • semantic_induct failed to apply Timeout for pure_foldl_At in Line 2214.
• [x] PCF/OpSem.thy -> depends on Basis.thy, Logical_Relations.thy, and PCF.thy.
• [x] Priority_Search_Trees/PST_RBT.thy -> depends on Prio_Map_Specs.thy and PST_General.thy.
• [x] Probabilistic_Timed_Automata/library/Graphs.thy -> depends on Instantiate_Existentials.thy, More_List.thy, Basic, Sequence, Sequence_LTL, Instantiate_Existentials, and Stream_More.
• [x] Rep_Fin_Groups/Rep_Fin_Groups.thy
• [x] Safe_OCL/OCL_Basic_Types.thy
• [x] Safe_OCL/OCL_Types.thy -> depends on OCL_Basic_Types.thy, Errorable.thy, Finite_Map_Ext, Transitive_Closure_Ext, and Tuple.
• [x] Simpl/SmallStep.thy -> depends on Language.thy, Semantic.thy, and Termination.thy.
• [x] VerifyThis2019/Challenge1A.thy
• [x] VerifyThis2019/Challenge1B.thy -> depends on Challenge1A.thy
• [ ] ZFC_in_HOL/Cantor_NF.thy -> depends on ZFC_in_HOL.thy, ZFC_Cardinals.thy, Kirby.thy, and Ordinal_Exp.thy.
  • semantic_induct failed at ω_sum_append in Line 494

[yutakang]

• [ ] Rep_Fin_Groups.thy has about 137 proofs by induction

[yutakang]

We already have more than 1k inductive problems in our dataset. And IJCAI has accepted our paper.