Tweak some fragile code in src/rat, removing jbUtils along the way

HOL-Theorem-Prover · Jan 23, 2024 · ee5139a · ee5139a
1 parent 51194e7
commit ee5139a
Show file tree

Hide file tree

Showing 9 changed files with 104 additions and 216 deletions.
diff --git a/src/rational/fracLib.sml b/src/rational/fracLib.sml
@@ -15,7 +15,7 @@ open
         pairTheory pairLib integerTheory intLib intSyntax
         EVAL_ringLib integerRingTheory integerRingLib
         intExtensionTheory intExtensionLib
-        jbUtils fracTheory fracUtils fracSyntax;
+        fracTheory fracUtils fracSyntax;
 
 val ERR = mk_HOL_ERR "fracLib"
 

diff --git a/src/rational/fracScript.sml b/src/rational/fracScript.sml
@@ -16,9 +16,9 @@ app load [
 *)
 
 open
-        pairTheory jbUtils schneiderUtils
+        pairTheory schneiderUtils
         arithmeticTheory integerTheory intLib integerRingLib intSyntax
-        intExtensionTheory intExtensionLib fracUtils;
+        intExtensionTheory intExtensionLib
 
 val _ = new_theory "frac";
 val _ = ParseExtras.temp_loose_equality()
@@ -347,6 +347,38 @@ fun frac_dnm_tac (asm_list:term list) (nmr,dnm) =
  *  simplify resp. nmr(abs_frac(a1,b1)) to a1 and frac_dnm(abs_frac(a1,b1)) to b1
  *--------------------------------------------------------------------------*)
 
+fun ttrip_eq (t1,t2,t3) (ta,tb,tc) =
+  pair_eq (pair_eq aconv aconv) aconv ((t1,t2),t3) ((ta,tb),tc)
+
+fun extract_frac_fun (l2:term list) (t1:term) =
+  if is_comb t1 then
+    let
+      val (top_rator, top_rand) = dest_comb t1;
+    in
+      if tmem top_rator l2 andalso is_comb top_rand then
+        let
+          val (second_rator, second_rand) = dest_comb top_rand;
+        in
+          if second_rator ~~ ``abs_frac`` then
+            let
+              val (this_nmr, this_dnm) = dest_pair (second_rand)
+              val sub_fracs =
+                  op_union ttrip_eq
+                           (extract_frac_fun l2 this_nmr)
+                           (extract_frac_fun l2 this_dnm)
+            in
+                [(top_rator,this_nmr,this_dnm)] @ sub_fracs
+            end
+          else (* not second_rator = ``abs_frac`` *)
+            extract_frac_fun l2 top_rand
+        end
+      else (* not (top_rator = l2 andalso is_comb top_rand) *)
+        op_union ttrip_eq (extract_frac_fun l2 top_rator)
+                 (extract_frac_fun l2 top_rand)
+    end
+  else (* not is_comb t1 *)
+    [];
+
 fun FRAC_NMRDNM_TAC (asm_list, goal) =
 let
   val term_list = extract_frac_fun [``frac_nmr``,``frac_dnm``] goal

diff --git a/src/rational/fracUtils.sig b/src/rational/fracUtils.sig
@@ -11,5 +11,4 @@ sig
         val extract_abs_frac : term -> term list
         val extract_frac_fun : term list -> term -> (term * term * term) list
 
-        val INT_GT0_CONV : term -> thm
 end
diff --git a/src/rational/fracUtils.sml b/src/rational/fracUtils.sml
@@ -1,22 +1,29 @@
 structure fracUtils :> fracUtils =
 struct
 
-open HolKernel boolLib Parse bossLib;
+open HolKernel boolLib bossLib;
 
-(* interactive mode
-app load ["pairTheory", "pairLib",
-        "integerTheory", "intLib",
-        "jbUtils"];
-*)
+structure Parse =
+struct
+open Parse
+val (Type,Term) = parse_from_grammars fracTheory.frac_grammars
+end
 
-open
-        pairTheory pairLib
-        integerTheory intLib
-        jbUtils;
+open Parse pairTheory pairLib integerTheory intLib
 
 (*--------------------------------------------------------------------------
  *  dest_frac : term -> term * term list
  *--------------------------------------------------------------------------*)
+fun dest_comb2 t = let val (fx,y) = dest_comb t
+                       val (f,x) = dest_comb fx
+                   in
+                     (f, [x,y])
+                   end
+fun is_rep_rat t = let val {Thy,Name,...} = dest_thy_const t
+                   in
+                     Thy = "rat" andalso Name = "rep_rat"
+                   end handle HOL_ERR _ => false
+
 
 fun dest_frac (t1:term) =
   if is_comb t1 then
@@ -31,14 +38,14 @@ fun dest_frac (t1:term) =
         end
       else
         if top_rator ~~ ``frac_ainv`` orelse top_rator ~~ ``frac_minv`` orelse
-           top_rator ~~ ``rep_rat``
+           is_rep_rat top_rator
         then
           (top_rator, [top_rand])
         else
           let
-            val (this_op, this_first, this_second) = dest_binop_triple t1
+            val (f, args) = dest_comb2 t1
           in
-            (this_op, [this_first, this_second])
+            (f, args)
           end
     end
   else (* t1 must be a variable *)
@@ -56,7 +63,12 @@ fun dest_frac (t1:term) =
  *  extract_frac : term -> term list
  *--------------------------------------------------------------------------*)
 
-fun extract_frac (t1:term) = extract_terms_of_type ``:frac`` t1;
+val frac_ty = mk_thy_type {Thy = "frac", Tyop = "frac", Args = []}
+fun extract_frac t =
+    if type_of t = frac_ty then [t]
+    else case dest_term t of
+             COMB (t1,t2) => op_U aconv [extract_frac t1, extract_frac t2]
+           | _ => []
 
 (* ---------- test cases ---------- *
         extract_frac ``4i + (frac_nmr(abs_frac(3i,4i))) = 3``;
@@ -132,17 +144,6 @@ fun extract_frac_fun (l2:term list) (t1:term) =
         extract_frac_fun [``frac_nmr``,``frac_dnm``] ``nmr(abs_frac(3,4)) + dnm(abs_frac(4,5))``;
  * ---------- test cases ---------- *)
 
-(*--------------------------------------------------------------------------
- *  INT_GT0_CONV : conv
- *
- *    t1          (with t1 greater than zero)
- *   -----------
- *    |- 0 < t1
- *--------------------------------------------------------------------------*)
-
-fun INT_GT0_CONV (t1:term) =
-        EQT_ELIM (intLib.ARITH_CONV ``0 < ^t1``);
-
 (*==========================================================================
  * end of structure
  *==========================================================================*)

diff --git a/src/rational/jbUtils.sig b/src/rational/jbUtils.sig
diff --git a/src/rational/jbUtils.sml b/src/rational/jbUtils.sml
diff --git a/src/rational/ratLib.sml b/src/rational/ratLib.sml
@@ -3,12 +3,14 @@ struct
 
 open HolKernel boolLib Parse bossLib;
 
-open simpLib pairLib integerTheory intLib intExtensionTheory jbUtils
+open simpLib pairLib integerTheory intLib intExtensionTheory
      schneiderUtils fracTheory fracLib fracUtils ratTheory ratUtils
      integerRingLib ratSyntax;
 
 val ERR = mk_HOL_ERR "ratLib";
 
+val IMP_AND_RULE = REWRITE_RULE[GSYM AND_IMP_INTRO];
+
 (*--------------------------------------------------------------------------
  *  imported from fracLib
  *--------------------------------------------------------------------------*)

diff --git a/src/rational/ratScript.sml b/src/rational/ratScript.sml
@@ -13,7 +13,7 @@ open
         integerTheory intLib
         intExtensionTheory intExtensionLib
         EVAL_ringLib integerRingLib
-        fracTheory fracLib ratUtils jbUtils
+        fracTheory fracLib ratUtils
         quotient schneiderUtils;
 
 val arith_ss = old_arith_ss
@@ -850,17 +850,21 @@ val RAT_EQ0_NMR = store_thm("RAT_EQ0_NMR", ``!r1. (r1 = 0q) = (rat_nmr r1 = 0)``
    |- !r1. (r1 < 0q) = (rat_nmr r1 < 0i)
  *--------------------------------------------------------------------------*)
 
-val RAT_0LES_NMR = store_thm("RAT_0LES_NMR", ``!r1. rat_les 0q r1 = 0i < rat_nmr r1``,
-        GEN_TAC THEN
-        REWRITE_TAC[rat_0, rat_nmr_def, rat_les_def, rat_sgn_def, frac_0_def, frac_sgn_def, SGN_def] THEN
-        RAT_CALC_TAC THEN
-        FRAC_POS_TAC ``1i`` THEN
-        FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN
-        SUBST_TAC[FRAC_CALC_CONV ``frac_sub (rep_rat r1) (abs_frac (0,1))``] THEN
-        REWRITE_TAC[RAT_NMREQ0_CONG,RAT_NMRLT0_CONG,RAT_NMRGT0_CONG] THEN
-        FRAC_NMRDNM_TAC THEN
-        RW_TAC int_ss [RAT, FRAC, INT_SUB_RZERO] THEN
-        PROVE_TAC[INT_LT_ANTISYM, INT_LT_TOTAL] );
+Theorem RAT_0LES_NMR:
+  !r1. rat_les 0q r1 = 0i < rat_nmr r1
+Proof
+  GEN_TAC THEN
+  REWRITE_TAC[rat_0, rat_nmr_def, rat_les_def, rat_sgn_def, frac_0_def,
+              frac_sgn_def, SGN_def] THEN
+  RAT_CALC_TAC THEN
+  FRAC_POS_TAC ``1i`` THEN
+  FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN
+  SUBST_TAC[FRAC_CALC_CONV ``frac_sub (rep_rat r1) (abs_frac (0,1))``] THEN
+  REWRITE_TAC[RAT_NMREQ0_CONG,RAT_NMRLT0_CONG,RAT_NMRGT0_CONG] THEN
+  FRAC_NMRDNM_TAC THEN
+  RW_TAC int_ss [RAT, FRAC, INT_SUB_RZERO] THEN
+  PROVE_TAC[INT_LT_ANTISYM, INT_LT_TOTAL]
+QED
 
 val RAT_LES0_NMR = store_thm("RAT_LES0_NMR", ``!r1. rat_les r1 0q = rat_nmr r1 < 0i``,
         GEN_TAC THEN
@@ -882,17 +886,21 @@ val RAT_LES0_NMR = store_thm("RAT_LES0_NMR", ``!r1. rat_les r1 0q = rat_nmr r1 <
    |- !r1. (r1 <= 0q) = (rat_nmr r1 <= 0i)
  *--------------------------------------------------------------------------*)
 
-val RAT_0LEQ_NMR = store_thm("RAT_0LEQ_NMR", ``!r1. rat_leq 0q r1 = 0i <= rat_nmr r1``,
-        GEN_TAC THEN
-        REWRITE_TAC[rat_leq_def, INT_LE_LT] THEN
-        NEW_GOAL_TAC ``!a b c d. ((a=c) /\ (b=d)) ==> (a \/ b = c \/ d)`` THEN
-        PROVE_TAC[RAT_0LES_NMR, RAT_EQ0_NMR, rat_nmr_def] );
+Theorem RAT_0LEQ_NMR:
+  !r1. rat_leq 0q r1 = 0i <= rat_nmr r1
+Proof
+  GEN_TAC THEN
+  REWRITE_TAC[rat_leq_def, INT_LE_LT] THEN
+  PROVE_TAC[RAT_0LES_NMR, RAT_EQ0_NMR, rat_nmr_def]
+QED
 
-val RAT_LEQ0_NMR = store_thm("RAT_LEQ0_NMR", ``!r1. rat_leq r1 0q = rat_nmr r1 <= 0i``,
-        GEN_TAC THEN
-        REWRITE_TAC[rat_leq_def, INT_LE_LT] THEN
-        NEW_GOAL_TAC ``!a b c d. ((a=c) /\ (b=d)) ==> (a \/ b = c \/ d)`` THEN
-        PROVE_TAC[RAT_LES0_NMR, RAT_EQ0_NMR, rat_nmr_def] );
+Theorem RAT_LEQ0_NMR:
+  !r1. rat_leq r1 0q = rat_nmr r1 <= 0i
+Proof
+  GEN_TAC THEN
+  REWRITE_TAC[rat_leq_def, INT_LE_LT] THEN
+  PROVE_TAC[RAT_LES0_NMR, RAT_EQ0_NMR, rat_nmr_def]
+QED
 
 (*==========================================================================
  *  field properties