equal
deleted
inserted
replaced
24 consts |
24 consts |
25 propn :: i |
25 propn :: i |
26 |
26 |
27 datatype propn = |
27 datatype propn = |
28 Fls |
28 Fls |
29 | Var ("n \<in> nat") ("#_" [100] 100) |
29 | Var ("n \<in> nat") (\<open>#_\<close> [100] 100) |
30 | Imp ("p \<in> propn", "q \<in> propn") (infixr "=>" 90) |
30 | Imp ("p \<in> propn", "q \<in> propn") (infixr \<open>=>\<close> 90) |
31 |
31 |
32 |
32 |
33 subsection \<open>The proof system\<close> |
33 subsection \<open>The proof system\<close> |
34 |
34 |
35 consts thms :: "i => i" |
35 consts thms :: "i => i" |
36 |
36 |
37 abbreviation |
37 abbreviation |
38 thms_syntax :: "[i,i] => o" (infixl "|-" 50) |
38 thms_syntax :: "[i,i] => o" (infixl \<open>|-\<close> 50) |
39 where "H |- p == p \<in> thms(H)" |
39 where "H |- p == p \<in> thms(H)" |
40 |
40 |
41 inductive |
41 inductive |
42 domains "thms(H)" \<subseteq> "propn" |
42 domains "thms(H)" \<subseteq> "propn" |
43 intros |
43 intros |
84 For every valuation, if all elements of \<open>H\<close> are true then so |
84 For every valuation, if all elements of \<open>H\<close> are true then so |
85 is \<open>p\<close>. |
85 is \<open>p\<close>. |
86 \<close> |
86 \<close> |
87 |
87 |
88 definition |
88 definition |
89 logcon :: "[i,i] => o" (infixl "|=" 50) where |
89 logcon :: "[i,i] => o" (infixl \<open>|=\<close> 50) where |
90 "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)" |
90 "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)" |
91 |
91 |
92 |
92 |
93 text \<open> |
93 text \<open> |
94 A finite set of hypotheses from \<open>t\<close> and the \<open>Var\<close>s in |
94 A finite set of hypotheses from \<open>t\<close> and the \<open>Var\<close>s in |