fix: resolve merge conflicts and fix syntax errors in extraction scripts

Author: hyperpolymath

scripts/extract_isabelle_tropical.jl

@@ -33,7 +33,7 @@ const START_ID        = 200000
 
 # Path to the tropical-resource-typing repo (sibling of neural-foundations).
 # Adjust if your checkout differs.
-const TROPICAL_REPO   = abspath(joinpath(REPO_ROOT, "..", "..", "..", "..", "tropical-resource-typing"))
+const TROPICAL_REPO   = abspath(joinpath(REPO_ROOT, "..", "tropical-resource-typing"))
 
 const THY_FILES = [
     ("Tropical_v2.thy",            "tropical_v2"),
@@ -527,7 +527,7 @@ function synthetic_isabelle_algebra()::Vector{IsabelleEntry}
          "\"dim_row A = n \\<Longrightarrow> dim_col A = m \\<Longrightarrow>\n  c \\<cdot>\\<^sub>m (d \\<cdot>\\<^sub>m A) = (c * d) \\<cdot>\\<^sub>m (A :: 'a :: semiring_0 mat)\"",
          "by (rule smult_smult_assoc)"),
         ("matrix_row_col",
-         "\"i < dim_row A \\<Longrightarrow> j < dim_col A \\<Longrightarrow>\n  (A :: 'a mat) $$ (i, j) = row A i $ j\"",
+         "\"i < dim_row A \\<Longrightarrow> j < dim_col A \\<Longrightarrow>\n  (A :: 'a mat) \$\$ (i, j) = row A i \$ j\"",
          "by (simp add: row_def)"),
         ("matrix_dim_mult",
          "\"dim_row (A * B) = dim_row A\"",

scripts/extract_mizar.jl

@@ -388,26 +388,26 @@ function generate_synthetic_mizar()::Vector{Dict{String,Any}}
     ]
 
     lattices = [
-        ("lattice_join_comm", "for L being Lattice, a, b being Element of L holds a \"\\\/\" b = b \"\\\/\" a",
-         "let L be Lattice; let a, b be Element of L; thus a \"\\\/\" b = b \"\\\/\" a by LATTICES:def 1;"),
+        ("lattice_join_comm", "for L being Lattice, a, b being Element of L holds a \"\\/\" b = b \"\\/\" a",
+         "let L be Lattice; let a, b be Element of L; thus a \"\\/\" b = b \"\\/\" a by LATTICES:def 1;"),
         ("lattice_meet_comm", "for L being Lattice, a, b being Element of L holds a \"/\\\" b = b \"/\\\" a",
          "let L be Lattice; let a, b be Element of L; thus a \"/\\\" b = b \"/\\\" a by LATTICES:def 2;"),
-        ("lattice_join_assoc", "for L being Lattice, a, b, c being Element of L holds a \"\\\/\" (b \"\\\/\" c) = (a \"\\\/\" b) \"\\\/\" c",
-         "let L be Lattice; let a, b, c be Element of L; thus a \"\\\/\" (b \"\\\/\" c) = (a \"\\\/\" b) \"\\\/\" c by LATTICES:def 5;"),
+        ("lattice_join_assoc", "for L being Lattice, a, b, c being Element of L holds a \"\\/\" (b \"\\/\" c) = (a \"\\/\" b) \"\\/\" c",
+         "let L be Lattice; let a, b, c be Element of L; thus a \"\\/\" (b \"\\/\" c) = (a \"\\/\" b) \"\\/\" c by LATTICES:def 5;"),
         ("lattice_meet_assoc", "for L being Lattice, a, b, c being Element of L holds a \"/\\\" (b \"/\\\" c) = (a \"/\\\" b) \"/\\\" c",
          "let L be Lattice; let a, b, c be Element of L; thus a \"/\\\" (b \"/\\\" c) = (a \"/\\\" b) \"/\\\" c by LATTICES:def 7;"),
-        ("lattice_absorption_join", "for L being Lattice, a, b being Element of L holds a \"\\\/\" (a \"/\\\" b) = a",
-         "let L be Lattice; let a, b be Element of L; thus a \"\\\/\" (a \"/\\\" b) = a by LATTICES:def 8;"),
-        ("lattice_absorption_meet", "for L being Lattice, a, b being Element of L holds a \"/\\\" (a \"\\\/\" b) = a",
-         "let L be Lattice; let a, b be Element of L; thus a \"/\\\" (a \"\\\/\" b) = a by LATTICES:def 9;"),
-        ("lattice_distributive", "for L being distributive Lattice, a, b, c being Element of L holds a \"/\\\" (b \"\\\/\" c) = (a \"/\\\" b) \"\\\/\" (a \"/\\\" c)",
-         "let L be distributive Lattice; let a, b, c be Element of L; thus a \"/\\\" (b \"\\\/\" c) = (a \"/\\\" b) \"\\\/\" (a \"/\\\" c) by LATTICES:def 11;"),
-        ("lattice_complemented", "for L being complemented bounded Lattice, a being Element of L ex b being Element of L st a \"\\\/\" b = Top L & a \"/\\\" b = Bottom L",
-         "let L be complemented bounded Lattice; let a be Element of L; thus ex b being Element of L st a \"\\\/\" b = Top L & a \"/\\\" b = Bottom L by LATTICES:def 19;"),
-        ("lattice_bounded", "for L being bounded Lattice, a being Element of L holds a \"\\\/\" (Bottom L) = a & a \"/\\\" (Top L) = a",
-         "let L be bounded Lattice; let a be Element of L; thus a \"\\\/\" (Bottom L) = a by LATTICES:39; thus a \"/\\\" (Top L) = a by LATTICES:41;"),
-        ("lattice_modular", "for L being modular Lattice, a, b, c being Element of L st a [= c holds a \"\\\/\" (b \"/\\\" c) = (a \"\\\/\" b) \"/\\\" c",
-         "let L be modular Lattice; let a, b, c be Element of L; assume a [= c; hence a \"\\\/\" (b \"/\\\" c) = (a \"\\\/\" b) \"/\\\" c by LATTICES:def 12;"),
+        ("lattice_absorption_join", "for L being Lattice, a, b being Element of L holds a \"\\/\" (a \"/\\\" b) = a",
+         "let L be Lattice; let a, b be Element of L; thus a \"\\/\" (a \"/\\\" b) = a by LATTICES:def 8;"),
+        ("lattice_absorption_meet", "for L being Lattice, a, b being Element of L holds a \"/\\\" (a \"\\/\" b) = a",
+         "let L be Lattice; let a, b be Element of L; thus a \"/\\\" (a \"\\/\" b) = a by LATTICES:def 9;"),
+        ("lattice_distributive", "for L being distributive Lattice, a, b, c being Element of L holds a \"/\\\" (b \"\\/\" c) = (a \"/\\\" b) \"\\/\" (a \"/\\\" c)",
+         "let L be distributive Lattice; let a, b, c be Element of L; thus a \"/\\\" (b \"\\/\" c) = (a \"/\\\" b) \"\\/\" (a \"/\\\" c) by LATTICES:def 11;"),
+        ("lattice_complemented", "for L being complemented bounded Lattice, a being Element of L ex b being Element of L st a \"\\/\" b = Top L & a \"/\\\" b = Bottom L",
+         "let L be complemented bounded Lattice; let a be Element of L; thus ex b being Element of L st a \"\\/\" b = Top L & a \"/\\\" b = Bottom L by LATTICES:def 19;"),
+        ("lattice_bounded", "for L being bounded Lattice, a being Element of L holds a \"\\/\" (Bottom L) = a & a \"/\\\" (Top L) = a",
+         "let L be bounded Lattice; let a be Element of L; thus a \"\\/\" (Bottom L) = a by LATTICES:39; thus a \"/\\\" (Top L) = a by LATTICES:41;"),
+        ("lattice_modular", "for L being modular Lattice, a, b, c being Element of L st a [= c holds a \"\\/\" (b \"/\\\" c) = (a \"\\/\" b) \"/\\\" c",
+         "let L be modular Lattice; let a, b, c be Element of L; assume a [= c; hence a \"\\/\" (b \"/\\\" c) = (a \"\\/\" b) \"/\\\" c by LATTICES:def 12;"),
     ]
 
     metric_spaces = [