src/ZF/Coind/Language.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 931
diff changeset
     1
(*  Title:      ZF/Coind/Language.ML
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 931
diff changeset
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     4
    Copyright   1995  University of Cambridge
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     5
*)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     6
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     7
(* ############################################################ *)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     8
(* General lemmas                                               *)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     9
(* ############################################################ *)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    10
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    11
goal ZF.thy "!!a.~a=b ==> ~a:{b}";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    12
by (fast_tac ZF_cs 1);    
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    13
qed "notsingletonI";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    14
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    15
goal ZF.thy "!!a.~a:{b} ==> ~a=b";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    16
by (fast_tac ZF_cs 1);    
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    17
qed "notsingletonD";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    18
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    19
val prems = goal ZF.thy "[| a~:{b}; a~=b ==> P |] ==> P";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    20
by (cut_facts_tac prems 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    21
by (resolve_tac prems 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    22
by (fast_tac ZF_cs 1);    
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    23
qed "notsingletonE";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    24
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    25
goal ZF.thy "!!x. x : A Un B ==> x: B Un A";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    26
by (fast_tac ZF_cs 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    27
qed "lem_fix";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    28
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    29
goal ZF.thy "!!A.[| x~:A; x=y |] ==> y~:A";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    30
by (fast_tac ZF_cs 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    31
qed "map_lem1";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    32
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    33
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    34
open Language;
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    35