|
8011
|
1 |
(* Title: HOL/MicroJava/J/Prog.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: David von Oheimb
|
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [
|
|
|
8 |
rtac finite_map_of 1]);
|
|
|
9 |
|
|
|
10 |
val is_classI = prove_goalw thy [is_class_def]
|
|
|
11 |
"\\<And>G. class G C = Some c \\<Longrightarrow> is_class G C" (K [Auto_tac]);
|
|
|
12 |
|
|
|
13 |
val is_classD = prove_goalw thy [is_class_def]
|
|
|
14 |
"\\<And>G. is_class G C \\<Longrightarrow> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
|
|
|
15 |
not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
|