X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Fbool.ma;h=7762657aec90514366049386a6453b8f275ec1e8;hb=dd93a0919b67bead0d4f07d49dfc198006edc9aa;hp=d532c3186fdca7ffd11fdd611183db88b228f89e;hpb=c0ac63fead67ea1902e3d923ce877a2779cf501e;p=helm.git

diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index d532c3186..7762657ae 100644
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -16,7 +16,6 @@ include "basics/relations.ma".
   | true : bool
   | false : bool.
 
-(* destruct does not work *)
 img class="anchor" src="icons/tick.png" id="not_eq_true_false"theorem not_eq_true_false : a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
 @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq change with match a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a with [true ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a|false ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a]
 >Heq // qed.
@@ -55,6 +54,10 @@ interpretation "boolean and" 'and x y = (andb x y).
 match b1 with [ true ⇒ P b2 | false ⇒ P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a] → P (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2).
 #b1 #b2 #P (elim b1) normalize // qed.
 
+img class="anchor" src="icons/tick.png" id="true_to_andb_true"theorem true_to_andb_true: ∀b1,b2. b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#b1 cases b1 normalize //
+qed.
+
 img class="anchor" src="icons/tick.png" id="andb_true_l"theorem andb_true_l: ∀ b1,b2. (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 #b1 (cases b1) normalize // qed.
 
@@ -92,10 +95,9 @@ match b1 with [ true ⇒ P a href="cic:/matita/basics/bool/bool.con(0,1,0)"tru
   | false ⇒  match b2 with [ true ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | false ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ]].
 
 notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
-(* notation > "£ term 46 e & term 46 t & term 46 f" non associative with precedence 46 *)
- for @{ 'ite $e $t $f }.
+ for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
 notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46
- for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }. 
+ for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
 
 img class="anchor" src="icons/tick.png" id="bool_to_decidable_eq"theorem bool_to_decidable_eq: 
   ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (b1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ab2).
@@ -103,5 +105,4 @@ notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp
 
 img class="anchor" src="icons/tick.png" id="true_or_false"theorem true_or_false:
 ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
-#b (cases b) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed.
-
+#b (cases b) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed.
\ No newline at end of file