Modified a few defs and proofs because of the changes to theory Finite.thy.
authornipkow
Thu Jun 05 14:40:35 1997 +0200 (1997-06-05)
changeset 3414804c8a178a7f
parent 3413 c1f63cc3a768
child 3415 c068bd2f0bbd
Modified a few defs and proofs because of the changes to theory Finite.thy.
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
src/HOL/Induct/Mutil.ML
src/HOL/Induct/PropLog.ML
     1.1 --- a/src/HOL/Auth/Shared.ML	Thu Jun 05 14:39:22 1997 +0200
     1.2 +++ b/src/HOL/Auth/Shared.ML	Thu Jun 05 14:40:35 1997 +0200
     1.3 @@ -313,36 +313,34 @@
     1.4  (*** Supply fresh keys for possibility theorems. ***)
     1.5  
     1.6  goal thy "EX K. Key K ~: used evs";
     1.7 -by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
     1.8 +by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
     1.9  by (Blast_tac 1);
    1.10  qed "Key_supply1";
    1.11  
    1.12 -val Fin_UNIV_insertI = UNIV_I RS Fin.insertI;
    1.13 -
    1.14  goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
    1.15 -by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
    1.16 +by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
    1.17  by (etac exE 1);
    1.18  by (cut_inst_tac [("evs","evs'")] 
    1.19 -    (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
    1.20 +    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
    1.21  by (Auto_tac());
    1.22  qed "Key_supply2";
    1.23  
    1.24  goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
    1.25  \                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
    1.26 -by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
    1.27 +by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
    1.28  by (etac exE 1);
    1.29  by (cut_inst_tac [("evs","evs'")] 
    1.30 -    (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
    1.31 +    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
    1.32  by (etac exE 1);
    1.33  by (cut_inst_tac [("evs","evs''")] 
    1.34 -    (Fin.emptyI RS Fin_UNIV_insertI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
    1.35 +    (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
    1.36  by (Step_tac 1);
    1.37  by (Full_simp_tac 1);
    1.38  by (fast_tac (!claset addSEs [allE]) 1);
    1.39  qed "Key_supply3";
    1.40  
    1.41  goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
    1.42 -by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
    1.43 +by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
    1.44  by (rtac selectI 1);
    1.45  by (Blast_tac 1);
    1.46  qed "Key_supply";
     2.1 --- a/src/HOL/Auth/Shared.thy	Thu Jun 05 14:39:22 1997 +0200
     2.2 +++ b/src/HOL/Auth/Shared.thy	Thu Jun 05 14:40:35 1997 +0200
     2.3 @@ -59,7 +59,7 @@
     2.4      assumes that their keys are dispersed so as to leave room for infinitely
     2.5      many fresh session keys.  We could, alternatively, restrict agents to
     2.6      an unspecified finite number.*)
     2.7 -  Key_supply_ax  "KK: Fin UNIV ==> EX K. K ~: KK & Key K ~: used evs"
     2.8 +  Key_supply_ax  "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
     2.9  
    2.10  
    2.11  (*Agents generate random (symmetric) keys and nonces.
     3.1 --- a/src/HOL/Induct/Mutil.ML	Thu Jun 05 14:39:22 1997 +0200
     3.2 +++ b/src/HOL/Induct/Mutil.ML	Thu Jun 05 14:40:35 1997 +0200
     3.3 @@ -117,8 +117,7 @@
     3.4  qed "domino_singleton";
     3.5  
     3.6  goal thy "!!d. d:domino ==> finite d";
     3.7 -by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
     3.8 -                      addSEs [domino.elim]) 1);
     3.9 +by (blast_tac (!claset addSEs [domino.elim]) 1);
    3.10  qed "domino_finite";
    3.11  
    3.12  
    3.13 @@ -126,7 +125,7 @@
    3.14  
    3.15  goal thy "!!t. t:tiling domino ==> finite t";
    3.16  by (eresolve_tac [tiling.induct] 1);
    3.17 -by (rtac finite_emptyI 1);
    3.18 +by (rtac Finites.emptyI 1);
    3.19  by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
    3.20  qed "tiling_domino_finite";
    3.21  
     4.1 --- a/src/HOL/Induct/PropLog.ML	Thu Jun 05 14:39:22 1997 +0200
     4.2 +++ b/src/HOL/Induct/PropLog.ML	Thu Jun 05 14:40:35 1997 +0200
     4.3 @@ -167,13 +167,16 @@
     4.4  by (Fast_tac 1);
     4.5  qed "insert_Diff_subset2";
     4.6  
     4.7 -(*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
     4.8 - could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
     4.9 -goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})";
    4.10 +goal PropLog.thy "finite(hyps p t)";
    4.11 +by (induct_tac "p" 1);
    4.12 +by (ALLGOALS Asm_simp_tac);
    4.13 +qed "hyps_finite";
    4.14 +
    4.15 +goal PropLog.thy "hyps p t <= (UN v. {#v, #v->false})";
    4.16  by (PropLog.pl.induct_tac "p" 1);
    4.17  by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
    4.18 -by (ALLGOALS (fast_tac (!claset addSIs Fin.intrs@[Fin_UnI])));
    4.19 -qed "hyps_finite";
    4.20 +by (Blast_tac 1);
    4.21 +qed "hyps_subset";
    4.22  
    4.23  val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
    4.24  
    4.25 @@ -181,9 +184,9 @@
    4.26    We may repeatedly subtract assumptions until none are left!*)
    4.27  val [sat] = goal PropLog.thy
    4.28      "{} |= p ==> !t. hyps p t - hyps p t0 |- p";
    4.29 -by (rtac (hyps_finite RS Fin_induct) 1);
    4.30 +by (rtac (hyps_subset RS (hyps_finite RS finite_subset_induct)) 1);
    4.31  by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
    4.32 -by (safe_tac (!claset));
    4.33 +by (Step_tac 1);
    4.34  (*Case hyps(p,t)-insert(#v,Y) |- p *)
    4.35  by (rtac thms_excluded_middle_rule 1);
    4.36  by (rtac (insert_Diff_same RS weaken_left) 1);
    4.37 @@ -212,8 +215,8 @@
    4.38  by (Fast_tac 1);
    4.39  qed "sat_imp";
    4.40  
    4.41 -val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
    4.42 -by (rtac (finite RS Fin_induct) 1);
    4.43 +goal PropLog.thy "!!H. finite H ==> !p. H |= p --> H |- p";
    4.44 +by (etac finite_induct 1);
    4.45  by (safe_tac ((claset_of "Fun") addSIs [completeness_0]));
    4.46  by (rtac (weaken_left_insert RS thms.MP) 1);
    4.47  by (fast_tac ((claset_of "Fun") addSIs [sat_imp]) 1);
    4.48 @@ -222,8 +225,6 @@
    4.49  
    4.50  val completeness = completeness_lemma RS spec RS mp;
    4.51  
    4.52 -val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)";
    4.53 -by (fast_tac (!claset addSEs [soundness, finite RS completeness]) 1);
    4.54 -qed "thms_iff";
    4.55 -
    4.56 -writeln"Reached end of file.";
    4.57 +goal PropLog.thy "!!H. finite H ==> (H |- p) = (H |= p)";
    4.58 +by (fast_tac (!claset addSEs [soundness, completeness]) 1);
    4.59 +qed "syntax_iff_semantics";