Fixes for auto-metarulification for axioms.

ekpyron · May 9, 2024 · 4af38cd · 4af38cd
1 parent 1566b30
commit 4af38cd
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 4 deletions.
diff --git a/AOT_PLM.thy b/AOT_PLM.thy
@@ -39,6 +39,8 @@ attribute_setup act_axiom_inst =
   \<open>Scan.succeed (Thm.rule_attribute []
     (K (fn thm => thm RS @{thm "vdash-properties:1[1]"})))\<close>
   "Instantiate modally fragile axiom as modally fragile theorem."
+lemmas "act_axiom_inst" = "vdash-properties:1[1]"
+declare "act_axiom_inst"[AOT_inst AOT_model_act_axiom]
 
 AOT_theorem "vdash-properties:1[2]":
   assumes \<open>\<phi> \<in> \<Lambda>\<^sub>\<box>\<close>
@@ -51,6 +53,8 @@ attribute_setup axiom_inst =
   \<open>Scan.succeed (Thm.rule_attribute []
     (K (fn thm => thm RS @{thm "vdash-properties:1[2]"})))\<close>
   "Instantiate axiom as theorem."
+lemmas "axiom_inst" = "vdash-properties:1[2]"
+declare "axiom_inst"[AOT_inst AOT_model_axiom]
 
 text\<open>Convenience methods and theorem sets for applying "cqt:2".\<close>
 method cqt_2_lambda_inst_prover =

diff --git a/AOT_commands.ML b/AOT_commands.ML
@@ -41,6 +41,11 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *)
 
 (**** RULIFICATION START *****)
+structure AOT_RulifyInsts = Theory_Data (
+  type T = thm Symtab.table
+  val empty = Symtab.empty
+  val merge = Symtab.merge (K true)
+);
 structure AOT_RulifyElims = Theory_Data (
   type T = (thm list) Symtab.table
   val empty = Symtab.empty
@@ -86,15 +91,20 @@ fun getUnvarifyRules ctxt thm = (
                                | NONE => []
 )
 
-val unvarifyRules = getUnvarifyRules ctxt thm
-val unvarifiedThm = fold (fn rule => fn thm => thm RS rule) unvarifyRules thm
-
 fun outermost_proper_const trm = case Term.strip_comb trm of
   (Const (\<^const_name>\<open>Trueprop\<close>, _), [trm]) => outermost_proper_const trm
  | (Const (\<^const_name>\<open>AOT_model_valid_in\<close>, _), [_,trm]) => outermost_proper_const trm
  | (Const c, _) => SOME (Const c)
  | _ => NONE
 
+val (thm,inst_thms) =
+  case Option.mapPartial (fn Const (trm,_) => Symtab.lookup (AOT_RulifyInsts.get (Context.theory_of ctxt)) trm | _ => NONE)
+                         (outermost_proper_const (Thm.concl_of thm))
+        of SOME instThm => (thm RS instThm,[instThm]) | _ => (thm,[])
+
+val unvarifyRules = getUnvarifyRules ctxt thm
+val unvarifiedThm = fold (fn rule => fn thm => thm RS rule) unvarifyRules thm
+
 fun getRules term = case (Symtab.lookup (AOT_RulifyElims.get (Context.theory_of ctxt)) term) of SOME list => list | _ => []
 
 fun getSimplifications thm = 
@@ -111,7 +121,7 @@ in flat simps end)
     | NONE => []
 
 val simps = getSimplifications unvarifiedThm
-val simps = map (fn thms => unvarifyRules@thms) simps
+val simps = map (fn thms => inst_thms@unvarifyRules@thms) simps
 in
 simps
 end

diff --git a/AOT_commands.thy b/AOT_commands.thy
@@ -46,6 +46,10 @@ attribute_setup AOT_elim = \<open>
 Args.term >>
 (fn (Const (name, _)) => Thm.declaration_attribute (fn thm => Context.mapping (AOT_RulifyElims.map (Symtab.map_default (name,[]) (fn thms => thm::thms))) I))
 \<close>
+attribute_setup AOT_inst = \<open>
+Args.term >>
+(fn (Const (name, _)) => Thm.declaration_attribute (fn thm => Context.mapping (AOT_RulifyInsts.map (Symtab.update_new (name,thm))) I))
+\<close>
 attribute_setup AOT_intro = \<open>
 Scan.succeed
 (Thm.declaration_attribute (fn thm => Context.mapping (AOT_RulifyIntros.map (Net.insert (K true) (Net.key_of_term (Thm.concl_of thm), thm))) I))

diff --git a/ROOT b/ROOT
@@ -15,6 +15,7 @@ session "AOT" = "HOL-Cardinals" +
     AOT_ExtendedRelationComprehension
     AOT_PossibleWorlds
     AOT_NaturalNumbers
+	AOT_Possibilities
     AOT_misc
   theories [document = false]
     ExportInfo