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

diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index bd832f5f9..d532c3186 100644
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -12,80 +12,80 @@
 include "basics/relations.ma".
 
 (********** bool **********)
-inductive bool: Type[0] ≝ 
+img class="anchor" src="icons/tick.png" id="bool"inductive bool: Type[0] ≝ 
   | true : bool
   | false : bool.
 
 (* destruct does not work *)
-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.
+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.
 
-definition notb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+img class="anchor" src="icons/tick.png" id="notb"definition notb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
 λ b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. match b with [true ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a|false ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a ].
 
 interpretation "boolean not" 'not x = (notb x).
 
-theorem notb_elim: ∀ b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
+img class="anchor" src="icons/tick.png" id="notb_elim"theorem notb_elim: ∀ b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
 match b with
 [ true ⇒ P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a
 | false ⇒ P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a] → P (a href="cic:/matita/basics/bool/notb.def(1)"notb/a b).
 #b #P elim b normalize // qed.
 
-theorem notb_notb: ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. a href="cic:/matita/basics/bool/notb.def(1)"notb/a (a href="cic:/matita/basics/bool/notb.def(1)"notb/a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b.
+img class="anchor" src="icons/tick.png" id="notb_notb"theorem notb_notb: ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. a href="cic:/matita/basics/bool/notb.def(1)"notb/a (a href="cic:/matita/basics/bool/notb.def(1)"notb/a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b.
 #b elim b // qed.
 
-theorem injective_notb: a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/basics/bool/notb.def(1)"notb/a.
+img class="anchor" src="icons/tick.png" id="injective_notb"theorem injective_notb: a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/basics/bool/notb.def(1)"notb/a.
 #b1 #b2 #H // qed.
 
-theorem noteq_to_eqnot: ∀b1,b2. b1 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a b2 → b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/notb.def(1)"notb/a b2.
+img class="anchor" src="icons/tick.png" id="noteq_to_eqnot"theorem noteq_to_eqnot: ∀b1,b2. b1 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a b2 → b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/notb.def(1)"notb/a b2.
 * * // #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
 qed.
 
-theorem eqnot_to_noteq: ∀b1,b2. b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/notb.def(1)"notb/a b2 → b1 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a b2.
+img class="anchor" src="icons/tick.png" id="eqnot_to_noteq"theorem eqnot_to_noteq: ∀b1,b2. b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/notb.def(1)"notb/a b2 → b1 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a b2.
 * * normalize // #H @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … a href="cic:/matita/basics/bool/not_eq_true_false.def(3)"not_eq_true_false/a) //
 qed.
 
-definition andb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+img class="anchor" src="icons/tick.png" id="andb"definition andb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
 λb1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. match b1 with [ true ⇒ b2 | false ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ].
 
 interpretation "boolean and" 'and x y = (andb x y).
 
-theorem andb_elim: ∀ b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. ∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
+img class="anchor" src="icons/tick.png" id="andb_elim"theorem andb_elim: ∀ b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. ∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
 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.
 
-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.
+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.
 
-theorem andb_true_r: ∀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 → 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.
+img class="anchor" src="icons/tick.png" id="andb_true_r"theorem andb_true_r: ∀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 → 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 #b2 (cases b1) normalize // (cases b2) // qed.
 
-theorem andb_true: ∀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 a title="logical 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.
+img class="anchor" src="icons/tick.png" id="andb_true"theorem andb_true: ∀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 a title="logical 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.
 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/basics/bool/andb_true_r.def(4)"andb_true_r/a, a href="cic:/matita/basics/bool/andb_true_l.def(4)"andb_true_l/a/span/span/ qed.
 
-definition orb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+img class="anchor" src="icons/tick.png" id="orb"definition orb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
 λb1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.match b1 with [ true ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | false ⇒ b2].
  
 interpretation "boolean or" 'or x y = (orb x y).
 
-theorem orb_elim: ∀ b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. ∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
+img class="anchor" src="icons/tick.png" id="orb_elim"theorem orb_elim: ∀ b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. ∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
 match b1 with [ true ⇒ P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | false ⇒ P b2] → P (a href="cic:/matita/basics/bool/orb.def(1)"orb/a b1 b2).
 #b1 #b2 #P (elim b1) normalize // qed.
 
-lemma orb_true_r1: ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. 
+img class="anchor" src="icons/tick.png" id="orb_true_r1"lemma orb_true_r1: ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/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 a title="boolean or" 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 #b2 #H >H // qed.
 
-lemma orb_true_r2: ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. 
+img class="anchor" src="icons/tick.png" id="orb_true_r2"lemma orb_true_r2: ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/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 or" 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 #b2 #H >H cases b1 // qed.
 
-lemma orb_true_l: ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. 
+img class="anchor" src="icons/tick.png" id="orb_true_l"lemma orb_true_l: ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. 
   (b1 a title="boolean or" 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) a title="logical or" 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).
 * normalize /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.
 
-definition xorb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+img class="anchor" src="icons/tick.png" id="xorb"definition xorb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
 λb1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
  match b1 with
   [ true ⇒  match b2 with [ true ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a | false ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a ]
@@ -97,6 +97,11 @@ notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative wi
 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]  }. 
 
-definition ite ≝ λA:Type[0].λe.λt,f:A.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).
+#b1 #b2 (cases b1) (cases b2) /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/ %2 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/ qed.
+
+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.
 
-interpretation "if then else" 'ite e t f = (ite ? e t f).