# HG changeset patch # User wenzelm # Date 1631471835 -7200 # Node ID 6bc96f31cafd2c442daf65d20b123bf2e37247f4 # Parent ffe269e74bdd3c17215c44d4857aa28412c901b6 more antiquotations; more formal use of consts; diff -r ffe269e74bdd -r 6bc96f31cafd src/Sequents/Modal0.thy --- a/src/Sequents/Modal0.thy Sun Sep 12 20:24:14 2021 +0200 +++ b/src/Sequents/Modal0.thy Sun Sep 12 20:37:15 2021 +0200 @@ -20,8 +20,8 @@ "_Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5) ML \ - fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2; - fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2; + fun star_tr c [s1, s2] = Syntax.const c $ seq_tr s1 $ seq_tr s2; + fun star_tr' c [s1, s2] = Syntax.const c $ seq_tr' s1 $ seq_tr' s2; \ parse_translation \ diff -r ffe269e74bdd -r 6bc96f31cafd src/Sequents/S43.thy --- a/src/Sequents/S43.thy Sun Sep 12 20:24:14 2021 +0200 +++ b/src/Sequents/S43.thy Sun Sep 12 20:37:15 2021 +0200 @@ -20,7 +20,7 @@ let val tr = seq_tr; fun s43pi_tr [s1, s2, s3, s4, s5, s6] = - Const (\<^const_syntax>\S43pi\, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6; + Syntax.const \<^const_syntax>\S43pi\ $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6; in [(\<^syntax_const>\_S43pi\, K s43pi_tr)] end \ @@ -28,7 +28,7 @@ let val tr' = seq_tr'; fun s43pi_tr' [s1, s2, s3, s4, s5, s6] = - Const(\<^syntax_const>\_S43pi\, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6; + Syntax.const \<^syntax_const>\_S43pi\ $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6; in [(\<^const_syntax>\S43pi\, K s43pi_tr')] end \ diff -r ffe269e74bdd -r 6bc96f31cafd src/Sequents/Sequents.thy --- a/src/Sequents/Sequents.thy Sun Sep 12 20:24:14 2021 +0200 +++ b/src/Sequents/Sequents.thy Sun Sep 12 20:37:15 2021 +0200 @@ -58,10 +58,9 @@ (* parse translation for sequences *) -fun abs_seq' t = Abs ("s", Type (\<^type_name>\seq'\, []), t); +fun abs_seq' t = Abs ("s", \<^Type>\seq'\, t); -fun seqobj_tr (Const (\<^syntax_const>\_SeqO\, _) $ f) = - Const (\<^const_syntax>\SeqO'\, dummyT) $ f +fun seqobj_tr (Const (\<^syntax_const>\_SeqO\, _) $ f) = Syntax.const \<^const_syntax>\SeqO'\ $ f | seqobj_tr (_ $ i) = i; fun seqcont_tr (Const (\<^syntax_const>\_SeqContEmp\, _)) = Bound 0 @@ -73,29 +72,28 @@ abs_seq'(seqobj_tr so $ seqcont_tr sc); fun singlobj_tr (Const (\<^syntax_const>\_SeqO\,_) $ f) = - abs_seq' ((Const (\<^const_syntax>\SeqO'\, dummyT) $ f) $ Bound 0); + abs_seq' ((Syntax.const \<^const_syntax>\SeqO'\ $ f) $ Bound 0); (* print translation for sequences *) -fun seqcont_tr' (Bound 0) = - Const (\<^syntax_const>\_SeqContEmp\, dummyT) +fun seqcont_tr' (Bound 0) = Syntax.const \<^syntax_const>\_SeqContEmp\ | seqcont_tr' (Const (\<^const_syntax>\SeqO'\, _) $ f $ s) = - Const (\<^syntax_const>\_SeqContApp\, dummyT) $ - (Const (\<^syntax_const>\_SeqO\, dummyT) $ f) $ seqcont_tr' s + Syntax.const \<^syntax_const>\_SeqContApp\ $ + (Syntax.const \<^syntax_const>\_SeqO\ $ f) $ seqcont_tr' s | seqcont_tr' (i $ s) = - Const (\<^syntax_const>\_SeqContApp\, dummyT) $ - (Const (\<^syntax_const>\_SeqId\, dummyT) $ i) $ seqcont_tr' s; + Syntax.const \<^syntax_const>\_SeqContApp\ $ + (Syntax.const \<^syntax_const>\_SeqId\ $ i) $ seqcont_tr' s; fun seq_tr' s = let - fun seq_itr' (Bound 0) = Const (\<^syntax_const>\_SeqEmp\, dummyT) + fun seq_itr' (Bound 0) = Syntax.const \<^syntax_const>\_SeqEmp\ | seq_itr' (Const (\<^const_syntax>\SeqO'\, _) $ f $ s) = - Const (\<^syntax_const>\_SeqApp\, dummyT) $ - (Const (\<^syntax_const>\_SeqO\, dummyT) $ f) $ seqcont_tr' s + Syntax.const \<^syntax_const>\_SeqApp\ $ + (Syntax.const \<^syntax_const>\_SeqO\ $ f) $ seqcont_tr' s | seq_itr' (i $ s) = - Const (\<^syntax_const>\_SeqApp\, dummyT) $ - (Const (\<^syntax_const>\_SeqId\, dummyT) $ i) $ seqcont_tr' s + Syntax.const \<^syntax_const>\_SeqApp\ $ + (Syntax.const \<^syntax_const>\_SeqId\ $ i) $ seqcont_tr' s in case s of Abs (_, _, t) => seq_itr' t @@ -104,33 +102,33 @@ fun single_tr c [s1, s2] = - Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2; + Syntax.const c $ seq_tr s1 $ singlobj_tr s2; fun two_seq_tr c [s1, s2] = - Const (c, dummyT) $ seq_tr s1 $ seq_tr s2; + Syntax.const c $ seq_tr s1 $ seq_tr s2; fun three_seq_tr c [s1, s2, s3] = - Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3; + Syntax.const c $ seq_tr s1 $ seq_tr s2 $ seq_tr s3; fun four_seq_tr c [s1, s2, s3, s4] = - Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4; + Syntax.const c $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4; fun singlobj_tr' (Const (\<^const_syntax>\SeqO'\,_) $ fm) = fm - | singlobj_tr' id = Const (\<^syntax_const>\_SeqId\, dummyT) $ id; + | singlobj_tr' id = Syntax.const \<^syntax_const>\_SeqId\ $ id; fun single_tr' c [s1, s2] = - Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; + Syntax.const c $ seq_tr' s1 $ seq_tr' s2; fun two_seq_tr' c [s1, s2] = - Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; + Syntax.const c $ seq_tr' s1 $ seq_tr' s2; fun three_seq_tr' c [s1, s2, s3] = - Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; + Syntax.const c $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; fun four_seq_tr' c [s1, s2, s3, s4] = - Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; + Syntax.const c $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; diff -r ffe269e74bdd -r 6bc96f31cafd src/Sequents/modal.ML --- a/src/Sequents/modal.ML Sun Sep 12 20:24:14 2021 +0200 +++ b/src/Sequents/modal.ML Sun Sep 12 20:37:15 2021 +0200 @@ -26,7 +26,7 @@ struct (*Returns the list of all formulas in the sequent*) -fun forms_of_seq (Const(\<^const_name>\SeqO'\,_) $ P $ u) = P :: forms_of_seq u +fun forms_of_seq \<^Const_>\SeqO' for P u\ = P :: forms_of_seq u | forms_of_seq (H $ u) = forms_of_seq u | forms_of_seq _ = []; diff -r ffe269e74bdd -r 6bc96f31cafd src/Sequents/prover.ML --- a/src/Sequents/prover.ML Sun Sep 12 20:24:14 2021 +0200 +++ b/src/Sequents/prover.ML Sun Sep 12 20:37:15 2021 +0200 @@ -117,7 +117,7 @@ (*Returns the list of all formulas in the sequent*) -fun forms_of_seq (Const(\<^const_name>\SeqO'\,_) $ P $ u) = P :: forms_of_seq u +fun forms_of_seq \<^Const_>\SeqO' for P u\ = P :: forms_of_seq u | forms_of_seq (H $ u) = forms_of_seq u | forms_of_seq _ = []; diff -r ffe269e74bdd -r 6bc96f31cafd src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Sun Sep 12 20:24:14 2021 +0200 +++ b/src/Sequents/simpdata.ML Sun Sep 12 20:37:15 2021 +0200 @@ -13,30 +13,30 @@ (*Make atomic rewrite rules*) fun atomize r = case Thm.concl_of r of - Const(\<^const_name>\Trueprop\,_) $ Abs(_,_,a) $ Abs(_,_,c) => + \<^Const_>\Trueprop for \Abs(_,_,a)\ \Abs(_,_,c)\\ => (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of ([], [p]) => (case p of - Const(\<^const_name>\imp\,_)$_$_ => atomize(r RS @{thm mp_R}) - | Const(\<^const_name>\conj\,_)$_$_ => atomize(r RS @{thm conjunct1}) @ + \<^Const_>\imp for _ _\ => atomize(r RS @{thm mp_R}) + | \<^Const_>\conj for _ _\ => atomize(r RS @{thm conjunct1}) @ atomize(r RS @{thm conjunct2}) - | Const(\<^const_name>\All\,_)$_ => atomize(r RS @{thm spec}) - | Const(\<^const_name>\True\,_) => [] (*True is DELETED*) - | Const(\<^const_name>\False\,_) => [] (*should False do something?*) + | \<^Const_>\All _ for _\ => atomize(r RS @{thm spec}) + | \<^Const_>\True\ => [] (*True is DELETED*) + | \<^Const_>\False\ => [] (*should False do something?*) | _ => [r]) | _ => []) (*ignore theorem unless it has precisely one conclusion*) | _ => [r]; (*Make meta-equalities.*) fun mk_meta_eq ctxt th = case Thm.concl_of th of - Const(\<^const_name>\Pure.eq\,_)$_$_ => th - | Const(\<^const_name>\Trueprop\,_) $ Abs(_,_,a) $ Abs(_,_,c) => + \<^Const_>\Pure.eq _ for _ _\ => th + | \<^Const_>\Trueprop for \Abs(_,_,a)\ \Abs(_,_,c)\\ => (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of ([], [p]) => (case p of - (Const(\<^const_name>\equal\,_)$_$_) => th RS @{thm eq_reflection} - | (Const(\<^const_name>\iff\,_)$_$_) => th RS @{thm iff_reflection} - | (Const(\<^const_name>\Not\,_)$_) => th RS @{thm iff_reflection_F} + \<^Const_>\equal _ for _ _\ => th RS @{thm eq_reflection} + | \<^Const_>\iff for _ _\ => th RS @{thm iff_reflection} + | \<^Const_>\Not for _\ => th RS @{thm iff_reflection_F} | _ => th RS @{thm iff_reflection_T}) | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th));