(**************************************************************************)
(* ********************************************************************** *)
-(* Progetto FreeScale *)
+(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
(* *)
-(* Questo materiale fa parte della tesi: *)
-(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
-(* *)
-(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
include "freescale/theory.ma".
(* BOOLEANI *)
(* ******** *)
-ndefinition bool_destruct :
- Πb1,b2:bool.ΠP:Prop.b1 = b2 →
+ndefinition bool_destruct_aux ≝
+Πb1,b2:bool.ΠP:Prop.b1 = b2 →
match b1 with
[ true ⇒ match b2 with [ true ⇒ P → P | false ⇒ P ]
| false ⇒ match b2 with [ true ⇒ P | false ⇒ P → P ]
].
+
+ndefinition bool_destruct : bool_destruct_aux.
#b1; #b2; #P;
nelim b1;
nelim b2;