reorganisation

reflection and holDerivation don't need to depend on ordinalTheory. move
lca-related stuff into a subdirectory that depends on ordinalTheory.

add some explicit removal of type abbreviations to avoid conflicts
during merge_grammars.

Author: xrchz

Holmakefile

@@ -3,7 +3,7 @@ VMLDIR = ../vml
 endif
 
 HOLHOL = $(VMLDIR)/hol-light
-INCLUDES = $(VMLDIR) $(HOLHOL)/syntax-lib $(HOLHOL)/set-theory $(HOLHOL)/standard/syntax $(HOLHOL)/standard/semantics $(HOLDIR)/examples/countable $(HOLDIR)/examples/set-theory/hol_sets
+INCLUDES = $(VMLDIR) $(HOLHOL)/syntax-lib $(HOLHOL)/set-theory $(HOLHOL)/standard/syntax $(HOLHOL)/standard/semantics $(HOLDIR)/examples/countable
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
@@ -16,7 +16,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
 all: $(TARGETS) $(HOLHEAP)
 .PHONY: all
 
-BARE_THYS = $(HOLHOL)/syntax-lib/holSyntaxLibTheory $(HOLHOL)/set-theory/setSpecTheory $(HOLHOL)/standard/syntax/holAxiomsSyntaxTheory $(HOLDIR)/examples/set-theory/hol_sets/ordinalTheory
+BARE_THYS = $(HOLHOL)/syntax-lib/holSyntaxLibTheory $(HOLHOL)/set-theory/setSpecTheory $(HOLHOL)/standard/syntax/holAxiomsSyntaxTheory
 
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 

holDerivationScript.sml

@@ -2,6 +2,8 @@ open HolKernel boolLib boolSimps bossLib lcsymtacs listTheory alistTheory pred_s
 open miscLib holSyntaxLibTheory holSyntaxTheory holSyntaxExtraTheory
 val _ = new_theory"holDerivation"
 
+val _ = temp_tight_equality()
+
 (* TODO: move? *)
 val type1_size_append = prove(
   ``∀l1 l2. type1_size (l1 ++ l2) = type1_size l1 + type1_size l2``,

lca/Holmakefile

@@ -0,0 +1,25 @@
+ifndef VMLDIR
+VMLDIR = ../vml
+endif
+
+HOLHOL = $(VMLDIR)/hol-light
+INCLUDES = .. $(HOLDIR)/examples/set-theory/hol_sets
+OPTIONS = QUIT_ON_FAILURE
+
+ifdef POLY
+HOLHEAP = heap
+PARENT_HOLHEAP = ../heap
+EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
+
+THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
+TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
+all: $(TARGETS) $(HOLHEAP)
+.PHONY: all
+
+BARE_THYS = ../reflectionTheory $(HOLDIR)/examples/set-theory/hol_sets/ordinalTheory
+
+DEPS = $(patsubst %,%.uo,$(BARE_THYS))
+
+$(HOLHEAP): $(DEPS)
+	$(protect $(HOLDIR)/bin/buildheap) -b $(PARENT_HOLHEAP) -o $(HOLHEAP) $(BARE_THYS)
+endif

lcaCtxtScript.sml renamed to lca/lcaCtxtScript.sml

@@ -4,6 +4,19 @@ open ordinalTheory wellorderTheory
 open setSpecTheory miscLib
 val _ = new_theory"lca"
 
+(* TODO: this functionality should be implemented by Parse *)
+local val ct = current_theory () in
+fun remove_tyabbrev s =
+  let
+    val _ = Parse.temp_set_grammars(type_grammar.remove_abbreviation(Parse.type_grammar())s,Parse.term_grammar())
+    val q = String.concat["val ",ct,"_grammars = (type_grammar.remove_abbreviation(#1 ",ct,"_grammars)\"",s,"\",#2 ",ct,"_grammars);"]
+    val _ = adjoin_to_theory{sig_ps=NONE, struct_ps=SOME(fn pp => PP.add_string pp q)}
+  in () end
+end
+val _ = remove_tyabbrev"reln"
+val _ = remove_tyabbrev"inf"
+(* -- *)
+
 (* TODO: move *)
 val MULT_LE_EXP = store_thm("MULT_LE_EXP",
   ``∀a:num b. a ≠ 1 ⇒ a * b ≤ a ** b``,
@@ -510,7 +523,7 @@ val implies_set_theory = store_thm("implies_set_theory",
   ``strong_limit_cardinal (UNIV:'U set) ∧
     regular_cardinal (UNIV:'U set)
     ⇒
-    ∃(mem:'U reln). is_set_theory mem ∧
+    ∃(mem:'U->'U->bool). is_set_theory mem ∧
       (∀s. s ≺ (UNIV:'U set) ⇒ ∃x. s = { a | a <: x }) ∧
       (¬countable (UNIV:'U set) ⇒ ∃inf. is_infinite mem inf)``,
   strip_tac >>
@@ -657,7 +670,7 @@ val strongly_inaccessible_def = Define`
 
 val strongly_inaccessible_imp = store_thm("strongly_inaccessible_imp",
   ``strongly_inaccessible (UNIV:'U set) ⇒
-    ∃(mem:'U reln). is_set_theory mem ∧
+    ∃(mem:'U->'U->bool). is_set_theory mem ∧
     (∀s. s ≺ (UNIV:'U set) ⇒ ∃x. s = { a | a <: x }) ∧
     (∃inf. is_infinite mem inf)``,
   rw[strongly_inaccessible_def] >> metis_tac[implies_set_theory])

lcaDemoScript.sml renamed to lca/lcaDemoScript.sml

@@ -7,6 +7,18 @@ open holConstrainedExtensionTheory
 val _ = temp_tight_equality()
 val _ = new_theory"reflection"
 
+(* TODO: this functionality should be implemented by Parse *)
+local val ct = current_theory () in
+fun remove_tyabbrev s =
+  let
+    val _ = Parse.temp_set_grammars(type_grammar.remove_abbreviation(Parse.type_grammar())s,Parse.term_grammar())
+    val q = String.concat["val ",ct,"_grammars = (type_grammar.remove_abbreviation(#1 ",ct,"_grammars)\"",s,"\",#2 ",ct,"_grammars);"]
+    val _ = adjoin_to_theory{sig_ps=NONE, struct_ps=SOME(fn pp => PP.add_string pp q)}
+  in () end
+end
+val _ = remove_tyabbrev"reln"
+(* -- *)
+
 (* TODO: move *)
 val termsem_typesem_matchable = store_thm("termsem_typesem_matchable",
 ``is_set_theory ^mem ⇒