51 |
51 |
52 lemma one_not_0: "1~=0" |
52 lemma one_not_0: "1~=0" |
53 by (simp add: bool_defs ) |
53 by (simp add: bool_defs ) |
54 |
54 |
55 (** 1=0 ==> R **) |
55 (** 1=0 ==> R **) |
56 lemmas one_neq_0 = one_not_0 [THEN notE, standard] |
56 lemmas one_neq_0 = one_not_0 [THEN notE] |
57 |
57 |
58 lemma boolE: |
58 lemma boolE: |
59 "[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P" |
59 "[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P" |
60 by (simp add: bool_defs, blast) |
60 by (simp add: bool_defs, blast) |
61 |
61 |
80 by simp |
80 by simp |
81 |
81 |
82 lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d" |
82 lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d" |
83 by simp |
83 by simp |
84 |
84 |
85 lemmas not_1 = not_def [THEN def_cond_1, standard, simp] |
85 lemmas not_1 = not_def [THEN def_cond_1, simp] |
86 lemmas not_0 = not_def [THEN def_cond_0, standard, simp] |
86 lemmas not_0 = not_def [THEN def_cond_0, simp] |
87 |
87 |
88 lemmas and_1 = and_def [THEN def_cond_1, standard, simp] |
88 lemmas and_1 = and_def [THEN def_cond_1, simp] |
89 lemmas and_0 = and_def [THEN def_cond_0, standard, simp] |
89 lemmas and_0 = and_def [THEN def_cond_0, simp] |
90 |
90 |
91 lemmas or_1 = or_def [THEN def_cond_1, standard, simp] |
91 lemmas or_1 = or_def [THEN def_cond_1, simp] |
92 lemmas or_0 = or_def [THEN def_cond_0, standard, simp] |
92 lemmas or_0 = or_def [THEN def_cond_0, simp] |
93 |
93 |
94 lemmas xor_1 = xor_def [THEN def_cond_1, standard, simp] |
94 lemmas xor_1 = xor_def [THEN def_cond_1, simp] |
95 lemmas xor_0 = xor_def [THEN def_cond_0, standard, simp] |
95 lemmas xor_0 = xor_def [THEN def_cond_0, simp] |
96 |
96 |
97 lemma not_type [TC]: "a:bool ==> not(a) : bool" |
97 lemma not_type [TC]: "a:bool ==> not(a) : bool" |
98 by (simp add: not_def) |
98 by (simp add: not_def) |
99 |
99 |
100 lemma and_type [TC]: "[| a:bool; b:bool |] ==> a and b : bool" |
100 lemma and_type [TC]: "[| a:bool; b:bool |] ==> a and b : bool" |