isabelle: src/Sequents/Modal0.thy@8ae1af3f88b1 (annotated)

17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	1	(* Title: Sequents/Modal0.thy
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	2	Author: Martin Coen
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	3	Copyright 1991 University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	4	*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	5
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	6	theory Modal0
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	7	imports LK0
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	8	begin
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	9
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 35113 diff changeset	10	ML_file "modal.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 35113 diff changeset	11
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	12	consts
61385 538100cc4399 more symbols; wenzelm parents: 60770 diff changeset	13	box :: "o\<Rightarrow>o" ("[]_" [50] 50)
538100cc4399 more symbols; wenzelm parents: 60770 diff changeset	14	dia :: "o\<Rightarrow>o" ("<>_" [50] 50)
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	15	Lstar :: "two_seqi"
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	16	Rstar :: "two_seqi"
14765 bafb24c150c1 proper use of 'syntax'; wenzelm parents: 7098 diff changeset	17
bafb24c150c1 proper use of 'syntax'; wenzelm parents: 7098 diff changeset	18	syntax
35113 1a0c129bb2e0 modernized translations; wenzelm parents: 21426 diff changeset	19	"_Lstar" :: "two_seqe" ("(_)\|L>(_)" [6,6] 5)
1a0c129bb2e0 modernized translations; wenzelm parents: 21426 diff changeset	20	"_Rstar" :: "two_seqe" ("(_)\|R>(_)" [6,6] 5)
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	21
60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 52143 diff changeset	22	ML \<open>
35113 1a0c129bb2e0 modernized translations; wenzelm parents: 21426 diff changeset	23	fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
1a0c129bb2e0 modernized translations; wenzelm parents: 21426 diff changeset	24	fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 52143 diff changeset	25	\<close>
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	26
60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 52143 diff changeset	27	parse_translation \<open>
52143 36ffe23b25f8 syntax translations always depend on context; wenzelm parents: 48891 diff changeset	28	[(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})),
36ffe23b25f8 syntax translations always depend on context; wenzelm parents: 48891 diff changeset	29	(@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))]
60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 52143 diff changeset	30	\<close>
35113 1a0c129bb2e0 modernized translations; wenzelm parents: 21426 diff changeset	31
60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 52143 diff changeset	32	print_translation \<open>
52143 36ffe23b25f8 syntax translations always depend on context; wenzelm parents: 48891 diff changeset	33	[(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})),
36ffe23b25f8 syntax translations always depend on context; wenzelm parents: 48891 diff changeset	34	(@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 52143 diff changeset	35	\<close>
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	36
62144 bdab93ccfaf8 eliminated old defs; wenzelm parents: 61386 diff changeset	37	definition strimp :: "[o,o]\<Rightarrow>o" (infixr "--<" 25)
bdab93ccfaf8 eliminated old defs; wenzelm parents: 61386 diff changeset	38	where "P --< Q == [](P \<longrightarrow> Q)"
bdab93ccfaf8 eliminated old defs; wenzelm parents: 61386 diff changeset	39
bdab93ccfaf8 eliminated old defs; wenzelm parents: 61386 diff changeset	40	definition streqv :: "[o,o]\<Rightarrow>o" (infixr ">-<" 25)
bdab93ccfaf8 eliminated old defs; wenzelm parents: 61386 diff changeset	41	where "P >-< Q == (P --< Q) \<and> (Q --< P)"
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	42
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	43
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	44	lemmas rewrite_rls = strimp_def streqv_def
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	45
61386 0a29a984a91b more symbols; wenzelm parents: 61385 diff changeset	46	lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F; $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F"
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	47	apply (unfold iff_def)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	48	apply (assumption \| rule conjR impR)+
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	49	done
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	50
61386 0a29a984a91b more symbols; wenzelm parents: 61385 diff changeset	51	lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q; $H,Q,P,$G \<turnstile> $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $E"
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	52	apply (unfold iff_def)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	53	apply (assumption \| rule conjL impL basic)+
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	54	done
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	55
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	56	lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	57	and unsafe_rls = allR exL
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	58	and bound_rls = allL exR
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	59
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	60	end

author	wenzelm
	Tue, 03 Jan 2017 17:33:08 +0100
changeset 64765	8ae1af3f88b1
parent 62144	bdab93ccfaf8
child 69593	3dda49e08b9d
permissions	-rw-r--r--