# HG changeset patch
# User nipkow
# Date 865514435 -7200
# Node ID 804c8a178a7f98c4cbb1491edd2c05d517485422
# Parent  c1f63cc3a7681af26dfd2a01c880cd79d20e5cfd
Modified a few defs and proofs because of the changes to theory Finite.thy.

diff -r c1f63cc3a768 -r 804c8a178a7f src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Thu Jun 05 14:39:22 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Thu Jun 05 14:40:35 1997 +0200
@@ -313,36 +313,34 @@
 (*** Supply fresh keys for possibility theorems. ***)
 
 goal thy "EX K. Key K ~: used evs";
-by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
+by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
 by (Blast_tac 1);
 qed "Key_supply1";
 
-val Fin_UNIV_insertI = UNIV_I RS Fin.insertI;
-
 goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
-by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
+by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
 by (etac exE 1);
 by (cut_inst_tac [("evs","evs'")] 
-    (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
+    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
 by (Auto_tac());
 qed "Key_supply2";
 
 goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
 \                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
-by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
+by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
 by (etac exE 1);
 by (cut_inst_tac [("evs","evs'")] 
-    (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
+    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
 by (etac exE 1);
 by (cut_inst_tac [("evs","evs''")] 
-    (Fin.emptyI RS Fin_UNIV_insertI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
+    (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
 by (Step_tac 1);
 by (Full_simp_tac 1);
 by (fast_tac (!claset addSEs [allE]) 1);
 qed "Key_supply3";
 
 goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
-by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
+by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
 by (rtac selectI 1);
 by (Blast_tac 1);
 qed "Key_supply";
diff -r c1f63cc3a768 -r 804c8a178a7f src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Thu Jun 05 14:39:22 1997 +0200
+++ b/src/HOL/Auth/Shared.thy	Thu Jun 05 14:40:35 1997 +0200
@@ -59,7 +59,7 @@
     assumes that their keys are dispersed so as to leave room for infinitely
     many fresh session keys.  We could, alternatively, restrict agents to
     an unspecified finite number.*)
-  Key_supply_ax  "KK: Fin UNIV ==> EX K. K ~: KK & Key K ~: used evs"
+  Key_supply_ax  "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
 
 
 (*Agents generate random (symmetric) keys and nonces.
diff -r c1f63cc3a768 -r 804c8a178a7f src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Thu Jun 05 14:39:22 1997 +0200
+++ b/src/HOL/Induct/Mutil.ML	Thu Jun 05 14:40:35 1997 +0200
@@ -117,8 +117,7 @@
 qed "domino_singleton";
 
 goal thy "!!d. d:domino ==> finite d";
-by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
-                      addSEs [domino.elim]) 1);
+by (blast_tac (!claset addSEs [domino.elim]) 1);
 qed "domino_finite";
 
 
@@ -126,7 +125,7 @@
 
 goal thy "!!t. t:tiling domino ==> finite t";
 by (eresolve_tac [tiling.induct] 1);
-by (rtac finite_emptyI 1);
+by (rtac Finites.emptyI 1);
 by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
 qed "tiling_domino_finite";
 
diff -r c1f63cc3a768 -r 804c8a178a7f src/HOL/Induct/PropLog.ML
--- a/src/HOL/Induct/PropLog.ML	Thu Jun 05 14:39:22 1997 +0200
+++ b/src/HOL/Induct/PropLog.ML	Thu Jun 05 14:40:35 1997 +0200
@@ -167,13 +167,16 @@
 by (Fast_tac 1);
 qed "insert_Diff_subset2";
 
-(*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
- could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
-goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})";
+goal PropLog.thy "finite(hyps p t)";
+by (induct_tac "p" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "hyps_finite";
+
+goal PropLog.thy "hyps p t <= (UN v. {#v, #v->false})";
 by (PropLog.pl.induct_tac "p" 1);
 by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (ALLGOALS (fast_tac (!claset addSIs Fin.intrs@[Fin_UnI])));
-qed "hyps_finite";
+by (Blast_tac 1);
+qed "hyps_subset";
 
 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
 
@@ -181,9 +184,9 @@
   We may repeatedly subtract assumptions until none are left!*)
 val [sat] = goal PropLog.thy
     "{} |= p ==> !t. hyps p t - hyps p t0 |- p";
-by (rtac (hyps_finite RS Fin_induct) 1);
+by (rtac (hyps_subset RS (hyps_finite RS finite_subset_induct)) 1);
 by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
-by (safe_tac (!claset));
+by (Step_tac 1);
 (*Case hyps(p,t)-insert(#v,Y) |- p *)
 by (rtac thms_excluded_middle_rule 1);
 by (rtac (insert_Diff_same RS weaken_left) 1);
@@ -212,8 +215,8 @@
 by (Fast_tac 1);
 qed "sat_imp";
 
-val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
-by (rtac (finite RS Fin_induct) 1);
+goal PropLog.thy "!!H. finite H ==> !p. H |= p --> H |- p";
+by (etac finite_induct 1);
 by (safe_tac ((claset_of "Fun") addSIs [completeness_0]));
 by (rtac (weaken_left_insert RS thms.MP) 1);
 by (fast_tac ((claset_of "Fun") addSIs [sat_imp]) 1);
@@ -222,8 +225,6 @@
 
 val completeness = completeness_lemma RS spec RS mp;
 
-val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)";
-by (fast_tac (!claset addSEs [soundness, finite RS completeness]) 1);
-qed "thms_iff";
-
-writeln"Reached end of file.";
+goal PropLog.thy "!!H. finite H ==> (H |- p) = (H |= p)";
+by (fast_tac (!claset addSEs [soundness, completeness]) 1);
+qed "syntax_iff_semantics";