1(* Title: Sequents/Sequents.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1993 University of Cambridge 4*) 5 6section \<open>Parsing and pretty-printing of sequences\<close> 7 8theory Sequents 9imports Pure 10keywords "print_pack" :: diag 11begin 12 13setup Pure_Thy.old_appl_syntax_setup 14 15declare [[unify_trace_bound = 20, unify_search_bound = 40]] 16 17typedecl o 18 19 20subsection \<open>Sequences\<close> 21 22typedecl seq' 23consts 24 SeqO' :: "[o,seq']\<Rightarrow>seq'" 25 Seq1' :: "o\<Rightarrow>seq'" 26 27 28subsection \<open>Concrete syntax\<close> 29 30nonterminal seq and seqobj and seqcont 31 32syntax 33 "_SeqEmp" :: seq ("") 34 "_SeqApp" :: "[seqobj,seqcont] \<Rightarrow> seq" ("__") 35 36 "_SeqContEmp" :: seqcont ("") 37 "_SeqContApp" :: "[seqobj,seqcont] \<Rightarrow> seqcont" (",/ __") 38 39 "_SeqO" :: "o \<Rightarrow> seqobj" ("_") 40 "_SeqId" :: "'a \<Rightarrow> seqobj" ("$_") 41 42type_synonym single_seqe = "[seq,seqobj] \<Rightarrow> prop" 43type_synonym single_seqi = "[seq'\<Rightarrow>seq',seq'\<Rightarrow>seq'] \<Rightarrow> prop" 44type_synonym two_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop" 45type_synonym two_seqe = "[seq, seq] \<Rightarrow> prop" 46type_synonym three_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop" 47type_synonym three_seqe = "[seq, seq, seq] \<Rightarrow> prop" 48type_synonym four_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop" 49type_synonym four_seqe = "[seq, seq, seq, seq] \<Rightarrow> prop" 50type_synonym sequence_name = "seq'\<Rightarrow>seq'" 51 52 53syntax 54 (*Constant to allow definitions of SEQUENCES of formulas*) 55 "_Side" :: "seq\<Rightarrow>(seq'\<Rightarrow>seq')" ("<<(_)>>") 56 57ML \<open> 58 59(* parse translation for sequences *) 60 61fun abs_seq' t = Abs ("s", Type (\<^type_name>\<open>seq'\<close>, []), t); 62 63fun seqobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>, _) $ f) = 64 Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f 65 | seqobj_tr (_ $ i) = i; 66 67fun seqcont_tr (Const (\<^syntax_const>\<open>_SeqContEmp\<close>, _)) = Bound 0 68 | seqcont_tr (Const (\<^syntax_const>\<open>_SeqContApp\<close>, _) $ so $ sc) = 69 seqobj_tr so $ seqcont_tr sc; 70 71fun seq_tr (Const (\<^syntax_const>\<open>_SeqEmp\<close>, _)) = abs_seq' (Bound 0) 72 | seq_tr (Const (\<^syntax_const>\<open>_SeqApp\<close>, _) $ so $ sc) = 73 abs_seq'(seqobj_tr so $ seqcont_tr sc); 74 75fun singlobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>,_) $ f) = 76 abs_seq' ((Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f) $ Bound 0); 77 78 79(* print translation for sequences *) 80 81fun seqcont_tr' (Bound 0) = 82 Const (\<^syntax_const>\<open>_SeqContEmp\<close>, dummyT) 83 | seqcont_tr' (Const (\<^const_syntax>\<open>SeqO'\<close>, _) $ f $ s) = 84 Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $ 85 (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s 86 | seqcont_tr' (i $ s) = 87 Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $ 88 (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s; 89 90fun seq_tr' s = 91 let 92 fun seq_itr' (Bound 0) = Const (\<^syntax_const>\<open>_SeqEmp\<close>, dummyT) 93 | seq_itr' (Const (\<^const_syntax>\<open>SeqO'\<close>, _) $ f $ s) = 94 Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $ 95 (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s 96 | seq_itr' (i $ s) = 97 Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $ 98 (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s 99 in 100 case s of 101 Abs (_, _, t) => seq_itr' t 102 | _ => s $ Bound 0 103 end; 104 105 106fun single_tr c [s1, s2] = 107 Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2; 108 109fun two_seq_tr c [s1, s2] = 110 Const (c, dummyT) $ seq_tr s1 $ seq_tr s2; 111 112fun three_seq_tr c [s1, s2, s3] = 113 Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3; 114 115fun four_seq_tr c [s1, s2, s3, s4] = 116 Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4; 117 118 119fun singlobj_tr' (Const (\<^const_syntax>\<open>SeqO'\<close>,_) $ fm) = fm 120 | singlobj_tr' id = Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ id; 121 122 123fun single_tr' c [s1, s2] = 124 Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 125 126fun two_seq_tr' c [s1, s2] = 127 Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 128 129fun three_seq_tr' c [s1, s2, s3] = 130 Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; 131 132fun four_seq_tr' c [s1, s2, s3, s4] = 133 Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; 134 135 136 137(** for the <<...>> notation **) 138 139fun side_tr [s1] = seq_tr s1; 140\<close> 141 142parse_translation \<open>[(\<^syntax_const>\<open>_Side\<close>, K side_tr)]\<close> 143 144 145subsection \<open>Proof tools\<close> 146 147ML_file \<open>prover.ML\<close> 148 149end 150