1.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-present.sml Sat Apr 17 20:44:57 2021 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-present.sml Sat Apr 17 21:10:27 2021 +0200
1.3 @@ -151,7 +151,7 @@
1.4 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
1.5 let
1.6 val thm_deriv = Thm.get_name_hint thm
1.7 - val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
1.8 + val thminst = TermC.inst_bdv subst (Eval.norm (Thm.prop_of thm))
1.9 in
1.10 ContThmInst
1.11 {thyID = thy',
1.12 @@ -168,7 +168,7 @@
1.13 val pp = Ctree.par_pblobj pt p
1.14 val thy' = Ctree.get_obj Ctree.g_domID pt pp
1.15 val subst = Subst.T_from_input (ThyC.get_theory thy') subs
1.16 - val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
1.17 + val thminst = TermC.inst_bdv subst (Eval.norm (Thm.prop_of thm))
1.18 val f = case p_ of
1.19 Pos.Frm => Ctree.get_obj Ctree.g_form pt p
1.20 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
2.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Sat Apr 17 20:44:57 2021 +0200
2.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Sat Apr 17 21:10:27 2021 +0200
2.3 @@ -58,7 +58,7 @@
2.4 fun rewrite__ thy i bdv tless rls put_asm thm ct =
2.5 let
2.6 val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
2.7 - (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm) ct
2.8 + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
2.9 in if rew then SOME (t', distinct op = asms) else NONE end
2.10 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
2.11 and rew_sub thy i bdv tless rls put_asm lrd r t =
3.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Sat Apr 17 20:44:57 2021 +0200
3.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Sat Apr 17 21:10:27 2021 +0200
3.3 @@ -160,7 +160,7 @@
3.4 s3 :: s2 :: ss => op #>@ (SEq $ s2 $ s3) ss
3.5 | ts => raise ERROR ("fun #> not applicable to \"" ^ UnparseC.terms ts ^ "\"")
3.6
3.7 -val contains_bdv = (not o null o (filter TermC.is_bdv) o TermC.ids2str o #prop o Thm.rep_thm);
3.8 +val contains_bdv = not o null o filter TermC.is_bdv o TermC.ids2str o Thm.prop_of;
3.9
3.10 (* does a rule contain a 'bdv'; descend recursively into Rls_ *)
3.11 fun contain_bdv [] = false
4.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Sat Apr 17 20:44:57 2021 +0200
4.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Sat Apr 17 21:10:27 2021 +0200
4.3 @@ -188,7 +188,7 @@
4.4 then ()
4.5 else error "termC.sml d1_isolate_add2";
4.6 val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
4.7 - val t = (norm o #prop o Thm.rep_thm) (ThmC.numerals_to_Free @{thm d1_isolate_add2});
4.8 + val t = (norm o Thm.prop_of) (ThmC.numerals_to_Free @{thm d1_isolate_add2});
4.9 val t' = inst_bdv subst t;
4.10 if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = -1 * ?a)"
4.11 then ()
4.12 @@ -204,7 +204,7 @@
4.13 (str2term "bdv_2", str2term "c_2"),
4.14 (str2term "bdv_3", str2term "c_3"),
4.15 (str2term "bdv_4", str2term "c_4")];
4.16 -val t = (norm o #prop o Thm.rep_thm) (ThmC.numerals_to_Free @{thm separate_bdvs_add});
4.17 +val t = (norm o Thm.prop_of) (ThmC.numerals_to_Free @{thm separate_bdvs_add});
4.18 val t' = inst_bdv subst t;
4.19
4.20 if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n"
4.21 @@ -648,7 +648,7 @@
4.22 "----------- fun strip_imp_prems', fun ins_concl -----------------------------------------------";
4.23 "----------- fun strip_imp_prems', fun ins_concl -----------------------------------------------";
4.24 "----------- fun strip_imp_prems', fun ins_concl -----------------------------------------------";
4.25 -val prop = (#prop o Thm.rep_thm) @{thm real_mult_div_cancel2};
4.26 +val prop = Thm.prop_of @{thm real_mult_div_cancel2};
4.27 UnparseC.term prop = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
4.28 val t as Const ("Pure.imp", _) $
4.29 (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $ (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Const ("Groups.zero_class.zero", _)))) $
4.30 @@ -661,7 +661,7 @@
4.31 if UnparseC.term t' = "(\<Longrightarrow>) (?k \<noteq> 0)" then () else error "strip_imp_prems' changed";
4.32
4.33 val thm = ThmC.numerals_to_Free @{thm frac_sym_conv};
4.34 -val prop = (#prop o Thm.rep_thm) thm;
4.35 +val prop = Thm.prop_of thm;
4.36 val concl = Logic.strip_imp_concl prop;
4.37 val SOME prems = strip_imp_prems' prop;
4.38 val prop' = ins_concl prems concl;
5.1 --- a/test/Tools/isac/Knowledge/poly.sml Sat Apr 17 20:44:57 2021 +0200
5.2 +++ b/test/Tools/isac/Knowledge/poly.sml Sat Apr 17 21:10:27 2021 +0200
5.3 @@ -232,7 +232,7 @@
5.4 "-------- investigate (new 2002) uniary minus -----------";
5.5 "-------- investigate (new 2002) uniary minus -----------";
5.6 (*---------------------------------------------- vvvvvvvvvvvvvv -----------------------*)
5.7 -val t = (#prop o Thm.rep_thm) @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
5.8 +val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
5.9 atomty t;
5.10 (*
5.11 *** Const (HOL.Trueprop, bool => prop)
6.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Sat Apr 17 20:44:57 2021 +0200
6.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Sat Apr 17 21:10:27 2021 +0200
6.3 @@ -37,7 +37,7 @@
6.4 val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
6.5 "----- from old: fun rewrite__";
6.6 val bdv = [];
6.7 -val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm);
6.8 +val r = inst_bdv bdv (norm (Thm.prop_of thm));
6.9 "----- from old: and rew_sub";
6.10 val (LHS,RHS) = (dest_equals o strip_trueprop
6.11 o Logic.strip_imp_concl) r;
6.12 @@ -591,10 +591,10 @@
6.13
6.14 val (t', asms, _ (*lrd*), rew) =
6.15 rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
6.16 - (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm) ct;
6.17 + (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct;
6.18 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
6.19 = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
6.20 - (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm), ct);
6.21 + (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);
6.22 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
6.23 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
6.24 ;
6.25 @@ -688,7 +688,7 @@
6.26 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
6.27 (thy, 1, [], rew_ord, erls, bool, thm, term);
6.28 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
6.29 - (thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)
6.30 + (thy, i, bdv, tless, rls, put_asm, [], inst_bdv bdv (norm (Thm.prop_of thm)), ct)
6.31 val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
6.32 val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
6.33 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
7.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Sat Apr 17 20:44:57 2021 +0200
7.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Sat Apr 17 21:10:27 2021 +0200
7.3 @@ -200,7 +200,7 @@
7.4 " _________________ rewrite x=4_________________ ";
7.5 (*
7.6 rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;
7.7 -atomty ((#prop o Thm.rep_thm) (!tthm));
7.8 +atomty (Thm.prop_of (!tthm));
7.9 atomty (Thm.term_of (!tct));
7.10 *)
7.11 val thy' = "Test";
8.1 --- a/test/Tools/isac/ProgLang/listC.sml Sat Apr 17 20:44:57 2021 +0200
8.2 +++ b/test/Tools/isac/ProgLang/listC.sml Sat Apr 17 21:10:27 2021 +0200
8.3 @@ -43,7 +43,7 @@
8.4
8.5 val t = str2term "NTH 1 [a,b,c,d,e]";
8.6 atomty t;
8.7 -val thm = (#prop o Thm.rep_thm o ThmC.numerals_to_Free) @{thm NTH_NIL};
8.8 +val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_NIL};
8.9 atomty thm;
8.10 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_NIL}) t;
8.11 if UnparseC.term t' = "a" then ()
8.12 @@ -54,7 +54,7 @@
8.13 (Const ("List.list.Cons", _) $ Free ("b", _) $
8.14 (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
8.15 atomty t;
8.16 -val thm = (#prop o Thm.rep_thm o ThmC.numerals_to_Free) @{thm NTH_CONS};
8.17 +val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
8.18 atomty thm;
8.19 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
8.20 if UnparseC.term t' = "NTH (3 + -1) [b, c, d, e]" then ()