[go: up one dir, main page]
Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Open
10 of 15 tasks
yutakang opened this issue Jul 24, 2020 · 2 comments
Open
10 of 15 tasks

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

yutakang opened this issue Jul 24, 2020 · 2 comments
Assignees
@yutakang
Labels
enhancement

Comments

@yutakang
Copy link
Collaborator
yutakang commented Jul 24, 2020 •
edited
Loading
  • 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.
  • rtranclp_induct -> 1 use case in Probabilistic_Timed_Automata/library/Graphs.thy and 2 use cases in Safe_OCL/Finite_Map_Ext.thy
  • tranclp_induct -> 1 use case in Probabilistic_Timed_Automata/library/Graphs.thy and 2 use cases in Safe_OCL/Finite_Map_Ext.thy
  • 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.
  • converse_trancl_induct -> 1 use case in Automatic_Refinement/Lib/Misc.thy`
  • converse_rtranclp_induct -> Simpl/SmallStep.thy(about 90 proofs by induction)
  • converse_rtranclp_induct2
  • 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.
  • 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
  • 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 yutakang self-assigned this Jul 24, 2020
@yutakang
Copy link
Collaborator Author
yutakang commented Oct 3, 2020 •
edited
Loading

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

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

@yutakang
Copy link
Collaborator Author
yutakang commented Oct 6, 2020 •
edited
Loading
  • 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.

@yutakang yutakang closed this as completed Oct 6, 2020
@yutakang yutakang reopened this Oct 6, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@yutakang yutakang

Labels
enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@yutakang