Merge branch 'master' of github.com:jvanbruegge/binder_datatypes

jvanbruegge · Sep 24, 2024 · 7457641 · 7457641
2 parents ef6c4a2 + 45adf12
commit 7457641
Show file tree

Hide file tree

Showing 4 changed files with 1,655 additions and 5 deletions.
diff --git a/Tools/mrbnf_sugar.ML b/Tools/mrbnf_sugar.ML
@@ -291,11 +291,17 @@ fun create_binder_datatype (spec : spec) lthy =
             REPEAT_DETERM o rtac ctxt allI,
             TRY o rtac ctxt @{thm disjointI},
             rtac ctxt IH,
-            REPEAT_DETERM o FIRST' [
-              rtac ctxt @{thm UnI1} THEN' rtac ctxt @{thm singletonI},
-              rtac ctxt @{thm UnI2}
+            K (Local_Defs.unfold0_tac ctxt @{thms Un_iff singleton_iff HOL.simp_thms(6,29,30)}),
+            REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms UNIV_I UN_I singletonI TrueI}),
+            IF_UNSOLVED o EVERY' [
+              etac ctxt @{thm contrapos_pp},
+              K (print_tac ctxt "bar"),
+              K (Local_Defs.unfold0_tac ctxt @{thms Un_iff de_Morgan_disj}),
+              REPEAT_DETERM o etac ctxt conjE,
+              assume_tac ctxt,
+              TRY o rtac ctxt @{thm UNIV_I},
+              K (print_tac ctxt "foo")
             ],
-            REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms UNIV_I UN_I singletonI}),
             IF_UNSOLVED o K no_tac
           ])) prems)
         ]) ctxt) (drop n prems))

diff --git a/Tools/parser.ML b/Tools/parser.ML
@@ -16,7 +16,7 @@ val parse_spec_arg = @{keyword "("} |-- BNF_Util.parse_binding_colon -- parse_se
   || parse_selector_typ >> pair Binding.empty
 
 val parse_binder_specs = Parse.enum1 "|" (Ctr_Sugar.parse_ctr_spec Parse.binding parse_spec_arg -- Parse.opt_mixfix
-  -- Scan.option (@{keyword binds} |-- (*Parse.enum1 ";"*) (Parse.list1 Parse.name --| @{keyword in} -- Parse.list1 Parse.name))
+  -- Scan.option (@{keyword binds} |-- (*Parse.enum1 ";"*) (Scan.repeat1 Parse.name --| @{keyword in} -- Scan.repeat1 Parse.name))
   )
 
 val parse_type_arg_constrained =