Use induction on free vars for alpha_FVars in lfp operations

jvanbruegge · Sep 11, 2024 · 32c87e6 · 32c87e6
1 parent 146926d
commit 32c87e6
Show file tree

Hide file tree

Showing 3 changed files with 1,862 additions and 595 deletions.
diff --git a/operations/BMV_Composition.thy b/operations/BMV_Composition.thy
@@ -0,0 +1,15 @@
+theory BMV_Composition
+  imports "Binders.MRBNF_Recursor"
+begin
+
+binder_datatype 'a type = Var 'a | App "'a type" "'a type list" | Forall x::'a t::"'a type" binds x in t
+
+abbreviation "bd_type \<equiv> natLeq"
+
+abbreviation "sb_type \<equiv> tvsubst_type"
+
+
+(* Comp *)
+type_synonym 'a T = "'a + 'a type"
+
+end