1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
(* ========================================================================= *)
(* Isabelle Light *)
(* Isabelle/Procedural style additions and other user-friendly shortcuts. *)
(* *)
(* Petros Papapanagiotou, Jacques Fleuriot *)
(* Center of Intelligent Systems and their Applications *)
(* University of Edinburgh *)
(* 2009-2012 *)
(* ========================================================================= *)
(* FILE : make.ml *)
(* DESCRIPTION : Makefile. Simply calls the loader but it was written to *)
(* match the rest of HOL Light's packages and for future use. *)
(* LAST MODIFIED: October 2010 *)
(* ========================================================================= *)
loads "IsabelleLight/isalight.ml";;
(* Some examples: *)
prove( `p/\q==>q`, rule impI THEN erule conjE THEN assumption);;
prove (`(!x. P x) ==> P (y+1)`, rule impI THEN erule_tac [`a`,`y+1`] allE THEN assumption);;
prove (`p\/q==>q\/p`, rule impI THEN erule disjE THENL [ rule disjI2 ; rule disjI1 ] THEN assumption);;
prove (`p/\q ==> p\/q`, rule impI THEN rule disjI1 THEN drule conjunct1 THEN assumption);;
prove (`p/\q ==> p\/q`, DISCH_TAC THEN DISJ1_TAC THEN FIRST_ASSUM(CONJUNCTS_THEN ACCEPT_TAC));;
prove (`P x /\ x =0 ==> P 0`, rule impI THEN erule conjE THEN simp[]);;
|
