Code

Revamp fixpoint code#49

Code

Merged

jvanbruegge merged 37 commits intomasterjvanbruegge/binder_datatypes:masterfrom fixpoint-revampjvanbruegge/binder_datatypes:fixpoint-revampCopy head branch name to clipboardNov 26, 2024

+19,255-9,489

Commits

Commits on Oct 17, 2024

• Add operations theory for least fixpoint

  jvanbruegge

  committed
  1ac8a6f

  Copy full SHA for 1ac8a6f

• Adapt recursor operations to manual fixpoint theory

  jvanbruegge

  committed
  a80e591

  Copy full SHA for a80e591

• Add bound free position to fixpoint operation

  jvanbruegge

  committed
  94fd68c

  Copy full SHA for 94fd68c

• Adapt recursor operations theory for bound free

  jvanbruegge

  committed
  ba4173b

  Copy full SHA for ba4173b

• Allow to disable noting of mrbnf theorems

  jvanbruegge

  committed
  c10476b

  Copy full SHA for c10476b

• Reorder fixpoint operations theory to bundle definitions

  jvanbruegge

  committed
  b2a2c20

  Copy full SHA for b2a2c20

• Add @{map_filter n} antiquotation

  jvanbruegge

  committed
  bbc0f9b

  Copy full SHA for bbc0f9b

• Rename old fixpoint code

  jvanbruegge

  committed
  a129e9a

  Copy full SHA for a129e9a

• Define fixpoint constants from ML

  jvanbruegge

  committed
  d070240

  Copy full SHA for d070240

• Automate fixpoint theorems up to and including alpha_trans

  jvanbruegge

  committed
  834b39e

  Copy full SHA for 834b39e

• Fix equivp subgoals for quotient

  jvanbruegge

  committed
  2295954

  Copy full SHA for 2295954

• Add operations theory for two datatype with two binding position for one free position

  jvanbruegge

  committed
  62e2ade

  Copy full SHA for 62e2ade

• Note covar_large theorem properly in covar class

  jvanbruegge

  committed
  e3f02a7

  Copy full SHA for e3f02a7

• Add more lemmas about id_on and eq_on

  jvanbruegge

  committed
  d32750b

  Copy full SHA for d32750b

• Add operations theory for greatest fixpoint

  jvanbruegge

  committed
  71af052

  Copy full SHA for 71af052

• Use same tactic for alpha_FVars for codatatypes and datatypes

  jvanbruegge

  committed
  135e793

  Copy full SHA for 135e793

• Remove usage of subgoal_tac, hard to use from ML

  jvanbruegge

  committed
  90fdbf8

  Copy full SHA for 90fdbf8

• Use induction on free vars for alpha_FVars in lfp operations

  jvanbruegge

  committed
  6df6526

  Copy full SHA for 6df6526

Commits on Oct 29, 2024

• Automate fixpoint proofs until alpha_FVars

  jvanbruegge

  committed
  d2413b7

  Copy full SHA for d2413b7

Commits on Oct 31, 2024

• Automate alpha_sym and alpha_trans

  jvanbruegge

  committed
  268e62e

  Copy full SHA for 268e62e

• Automate until permute_simps theorem

  jvanbruegge

  committed
  a2910b8

  Copy full SHA for a2910b8

Commits on Nov 5, 2024

• Automate rest fixpoint theorems for datatypes

  jvanbruegge

  committed
  3ed209e

  Copy full SHA for 3ed209e

Commits on Nov 7, 2024

• Delete old fp code

  jvanbruegge

  committed
  7ee8f2b

  Copy full SHA for 7ee8f2b

• Adapt fp_result for new theorems and register fixpoint operation

  jvanbruegge

  committed
  38a6dd8

  Copy full SHA for 38a6dd8

Commits on Nov 9, 2024

• Adjust recursor code to deal with bound free positions

  jvanbruegge

  committed
  700cfad

  Copy full SHA for 700cfad

• Fix VVSubst and TVSubst operations theories for bound free positions

  jvanbruegge

  committed
  52da0d3

  Copy full SHA for 52da0d3

Commits on Nov 10, 2024

• Fix vvsubst automation and sugar operations for bound free positions

  jvanbruegge

  committed
  68c574c

  Copy full SHA for 68c574c

Commits on Nov 18, 2024

• Fix tvsubst for bound free positions

  jvanbruegge

  committed
  db01938

  Copy full SHA for db01938

• Add map, subst and permute simps to sugar operations

  jvanbruegge

  committed
  c78f80d

  Copy full SHA for c78f80d

• Merge branch 'master' into fixpoint-revamp

  jvanbruegge

  committed
  5b1540d

  Copy full SHA for 5b1540d

Commits on Nov 19, 2024

• Fix renamed theorems in case studies

  jvanbruegge

  committed
  0a1cea2

  Copy full SHA for 0a1cea2

• Fix theorem names in pi calculus

  jvanbruegge

  committed
  7c8ceec

  Copy full SHA for 7c8ceec

Commits on Nov 21, 2024

• Make induction theorems optional in fixpoint

  jvanbruegge

  committed
  add3337

  Copy full SHA for add3337

• Strengthen fresh_cases theorem, do not use unnecessary "avoid" constant

  jvanbruegge

  committed
  35807c7

  Copy full SHA for 35807c7

• Allow bound free positions and non-recursive types

  jvanbruegge

  committed
  2f9551b

  Copy full SHA for 2f9551b

• Fix usage of fresh_cases theorem

  jvanbruegge

  committed
  a479bcd

  Copy full SHA for a479bcd

• Replace custom ML for commitment type

  jvanbruegge

  committed
  3c5ee89

  Copy full SHA for 3c5ee89