45 hyps :: "[i,i] => i" |
45 hyps :: "[i,i] => i" |
46 |
46 |
47 defs |
47 defs |
48 |
48 |
49 prop_rec_def |
49 prop_rec_def |
50 "prop_rec(p,b,c,h) == \ |
50 "prop_rec(p,b,c,h) == |
51 \ Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))" |
51 Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))" |
52 |
52 |
53 (** Semantics of propositional logic **) |
53 (** Semantics of propositional logic **) |
54 is_true_def |
54 is_true_def |
55 "is_true(p,t) == prop_rec(p, 0, %v. if(v:t, 1, 0), \ |
55 "is_true(p,t) == prop_rec(p, 0, %v. if(v:t, 1, 0), |
56 \ %p q tp tq. if(tp=1,tq,1)) = 1" |
56 %p q tp tq. if(tp=1,tq,1)) = 1" |
57 |
57 |
58 (*Logical consequence: for every valuation, if all elements of H are true |
58 (*Logical consequence: for every valuation, if all elements of H are true |
59 then so is p*) |
59 then so is p*) |
60 logcon_def "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)" |
60 logcon_def "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)" |
61 |
61 |
62 (** A finite set of hypotheses from t and the Vars in p **) |
62 (** A finite set of hypotheses from t and the Vars in p **) |
63 hyps_def |
63 hyps_def |
64 "hyps(p,t) == prop_rec(p, 0, %v. {if(v:t, #v, #v=>Fls)}, \ |
64 "hyps(p,t) == prop_rec(p, 0, %v. {if(v:t, #v, #v=>Fls)}, |
65 \ %p q Hp Hq. Hp Un Hq)" |
65 %p q Hp Hq. Hp Un Hq)" |
66 |
66 |
67 end |
67 end |