SeLFiE: commonly used manually developed induction principles in the standard library

[yutakang]

• [x] trancl_induct -> 2 use cases in Automatic_Refinement/Lib/Misc.thy out of about 200 proofs by induction. 7 use cases in KBPs/Kripke.thy out of 18 proofs by induction.
• [x] rtranclp_induct -> 1 use case in Probabilistic_Timed_Automata/library/Graphs.thy and 2 use cases in Safe_OCL/Finite_Map_Ext.thy
• [x] tranclp_induct -> 1 use case in Probabilistic_Timed_Automata/library/Graphs.thy and 2 use cases in Safe_OCL/Finite_Map_Ext.thy
• [x] converse_tranclp_induct in 9 use cases in Safe_OCL/OCL_Types.thy out of about 40 proofs by induction and 9 use cases in Safe_OCL/OCL_Basic_Types.thy out of 20 proofs by induction.
• [x] converse_trancl_induct -> 1 use case in Automatic_Refinement/Lib/Misc.thy`
• [x] converse_rtranclp_induct -> Simpl/SmallStep.thy(about 90 proofs by induction)
• [x] converse_rtranclp_induct2
• [x] converse_rtrancl_induct2 -> about 6 use cases inCoreC++/TypeSafe.thy (about 35 proofs by induction)
• [ ] less_induct-> used in Aggregation_Algebras/Hoare_Logic.thy but not a good example or difficult to encode a heuristic for this.
• [x] finite_induct -> about 7-9 use cases in Disjunctive_Normal_Form.thy in LTL (about 58 proofs by induction) (I guess this induction rule is obsolete due to the use of set field.)
• [ ] less_Suc_induct in Nat.thy-> used in Goodstein_Lambda.thy
• [ ] inc_induct in Nat.thy-> used in Goodstein_Lambda.thy
• [x] list_nonempty_induct -> as ≠ [] ⟹ ... and list consisting of one element (List.list.Cons, function application that returns an element from a list.) about 4 use cases in Probabilistic_Timed_Automata/library/Graphs.thy which has in total about 60 proofs by induction.
• rev_induct -> difficult to encode heuristics. See OpSets/. The choice of this inductive rule is mostly based on the existence of a simplification rule that has the form of ... (xs @ [x]).... Therefore, we have to resort to a proof search to pick up this induction rule if such simplification rule does not appear as assumptions or chained facts. The presence of length and a variable of type list might work as an indicator, but not very reliable one.
• [ ] nat_less_induct -> difficult to encode heuristics using SeLFiE. used often in HOL-CSP/Sync.thy Induction terms are usually not just sub-terms appearing in proof goals. The use case in Automatic_Refinement/Lib/Misc.thy seems straightforward.
• [ ] length_induct -> 4 use cases in Automatic_Refinement/Lib/Misc.thy out of . Check for length xs <= length ys.
  • All length ? can be good candidates as well: see KD_Tree.Build.thy, Closest_Pair_Points/Closest_Pair_Alternative.thy, and KD_Tree/Build.thy.

[yutakang]

The file Rep_Fin_Groups.thy has nice examples of how these are used. (about 130 proofs by induction)

• [x] list_all2_induct
• [x] rev_nonempty_induct -> as ≠ [ ] ⟹...
• [x] list_induct2
• [ ] list_induct3

[yutakang]

• [ ] dec_induct in Nat.thy -> Not used often. 6 cases are found in Architectural_Design_Patterns.RF_LTL.thy. xs ≥ ys -> induct xs. xs ≤ ys -> induct ys but only if they are in a premise or chained fact.
• [ ] zero_induct in Nat.thy -> Not used often.
• [ ] strict_inc_induct in Nat.thy -> Not used often.