Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Union.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      ZF/UNITY/Union.thy
    Author:     Sidi O Ehmety, Computer Laboratory
    Copyright   2001  University of Cambridge

Unions of programs

Partly from Misra's Chapter 5 \<in> Asynchronous Compositions of Programs

Theory ported form HOL..

*)

theory Union imports SubstAx FP
begin

definition
  (*FIXME: conjoin Init(F) \<inter> Init(G) \<noteq> 0 *)
  ok :: "[i, i] => o"     (infixl \<open>ok\<close> 65)  where
    "F ok G == Acts(F) \ AllowedActs(G) &
               Acts(G) \<subseteq> AllowedActs(F)"

definition
  (*FIXME: conjoin (\<Inter>i \<in> I. Init(F(i))) \<noteq> 0 *)
  OK  :: "[i, i=>i] => o"  where
    "OK(I,F) == (\i \ I. \j \ I-{i}. Acts(F(i)) \ AllowedActs(F(j)))"

definition
  JOIN  :: "[i, i=>i] => i"  where
  "JOIN(I,F) == if I = 0 then SKIP else
                 mk_program(\<Inter>i \<in> I. Init(F(i)), \<Union>i \<in> I. Acts(F(i)),
                 \<Inter>i \<in> I. AllowedActs(F(i)))"

definition
  Join :: "[i, i] => i"  (infixl \<open>\<squnion>\<close> 65)  where
  "F \ G == mk_program (Init(F) \ Init(G), Acts(F) \ Acts(G),
                                AllowedActs(F) \<inter> AllowedActs(G))"
definition
  (*Characterizes safety properties.  Used with specifying AllowedActs*)
  safety_prop :: "i => o"  where
  "safety_prop(X) == X\program &
      SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)"

syntax
  "_JOIN1"  :: "[pttrns, i] => i"     (\<open>(3\<Squnion>_./ _)\<close> 10)
  "_JOIN"   :: "[pttrn, i, i] => i"   (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10)

translations
  "\x \ A. B" == "CONST JOIN(A, (\x. B))"
  "\x y. B" == "\x. \y. B"
  "\x. B" == "CONST JOIN(CONST state, (\x. B))"

subsection\<open>SKIP\<close>

lemma reachable_SKIP [simp]: "reachable(SKIP) = state"
by (force elim: reachable.induct intro: reachable.intros)

text\<open>Elimination programify from ok and \<squnion>\<close>

lemma ok_programify_left [iff]: "programify(F) ok G \ F ok G"
by (simp add: ok_def)

lemma ok_programify_right [iff]: "F ok programify(G) \ F ok G"
by (simp add: ok_def)

lemma Join_programify_left [simp]: "programify(F) \ G = F \ G"
by (simp add: Join_def)

lemma Join_programify_right [simp]: "F \ programify(G) = F \ G"
by (simp add: Join_def)

subsection\<open>SKIP and safety properties\<close>

lemma SKIP_in_constrains_iff [iff]: "(SKIP \ A co B) \ (A\B & st_set(A))"
by (unfold constrains_def st_set_def, auto)

lemma SKIP_in_Constrains_iff [iff]: "(SKIP \ A Co B)\ (state \ A\B)"
by (unfold Constrains_def, auto)

lemma SKIP_in_stable [iff]: "SKIP \ stable(A) \ st_set(A)"
by (auto simp add: stable_def)

lemma SKIP_in_Stable [iff]: "SKIP \ Stable(A)"
by (unfold Stable_def, auto)

subsection\<open>Join and JOIN types\<close>

lemma Join_in_program [iff,TC]: "F \ G \ program"
by (unfold Join_def, auto)

lemma JOIN_in_program [iff,TC]: "JOIN(I,F) \ program"
by (unfold JOIN_def, auto)

subsection\<open>Init, Acts, and AllowedActs of Join and JOIN\<close>
lemma Init_Join [simp]: "Init(F \ G) = Init(F) \ Init(G)"
by (simp add: Int_assoc Join_def)

lemma Acts_Join [simp]: "Acts(F \ G) = Acts(F) \ Acts(G)"
by (simp add: Int_Un_distrib2 cons_absorb Join_def)

lemma AllowedActs_Join [simp]: "AllowedActs(F \ G) =
  AllowedActs(F) \<inter> AllowedActs(G)"
apply (simp add: Int_assoc cons_absorb Join_def)
done

subsection\<open>Join's algebraic laws\<close>

lemma Join_commute: "F \ G = G \ F"
by (simp add: Join_def Un_commute Int_commute)

lemma Join_left_commute: "A \ (B \ C) = B \ (A \ C)"
apply (simp add: Join_def Int_Un_distrib2 cons_absorb)
apply (simp add: Un_ac Int_ac Int_Un_distrib2 cons_absorb)
done

lemma Join_assoc: "(F \ G) \ H = F \ (G \ H)"
by (simp add: Un_ac Join_def cons_absorb Int_assoc Int_Un_distrib2)

subsection\<open>Needed below\<close>
lemma cons_id [simp]: "cons(id(state), Pow(state * state)) = Pow(state*state)"
by auto

lemma Join_SKIP_left [simp]: "SKIP \ F = programify(F)"
apply (unfold Join_def SKIP_def)
apply (auto simp add: Int_absorb cons_eq)
done

lemma Join_SKIP_right [simp]: "F \ SKIP = programify(F)"
apply (subst Join_commute)
apply (simp add: Join_SKIP_left)
done

lemma Join_absorb [simp]: "F \ F = programify(F)"
by (rule program_equalityI, auto)

lemma Join_left_absorb: "F \ (F \ G) = F \ G"
by (simp add: Join_assoc [symmetric])

subsection\<open>Join is an AC-operator\<close>
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute

subsection\<open>Eliminating programify form JOIN and OK expressions\<close>

lemma OK_programify [iff]: "OK(I, %x. programify(F(x))) \ OK(I, F)"
by (simp add: OK_def)

lemma JOIN_programify [iff]: "JOIN(I, %x. programify(F(x))) = JOIN(I, F)"
by (simp add: JOIN_def)

subsection\<open>JOIN\<close>

lemma JOIN_empty [simp]: "JOIN(0, F) = SKIP"
by (unfold JOIN_def, auto)

lemma Init_JOIN [simp]:
     "Init(\i \ I. F(i)) = (if I=0 then state else (\i \ I. Init(F(i))))"
by (simp add: JOIN_def INT_extend_simps del: INT_simps)

lemma Acts_JOIN [simp]:
     "Acts(JOIN(I,F)) = cons(id(state), \i \ I. Acts(F(i)))"
apply (unfold JOIN_def)
apply (auto simp del: INT_simps UN_simps)
apply (rule equalityI)
apply (auto dest: Acts_type [THEN subsetD])
done

lemma AllowedActs_JOIN [simp]:
     "AllowedActs(\i \ I. F(i)) =
      (if I=0 then Pow(state*state) else (\<Inter>i \<in> I. AllowedActs(F(i))))"
apply (unfold JOIN_def, auto)
apply (rule equalityI)
apply (auto elim!: not_emptyE dest: AllowedActs_type [THEN subsetD])
done

lemma JOIN_cons [simp]: "(\i \ cons(a,I). F(i)) = F(a) \ (\i \ I. F(i))"
by (rule program_equalityI, auto)

lemma JOIN_cong [cong]:
    "[| I=J; !!i. i \ J ==> F(i) = G(i) |] ==>
     (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> J. G(i))"
by (simp add: JOIN_def)

subsection\<open>JOIN laws\<close>
lemma JOIN_absorb: "k \ I ==>F(k) \ (\i \ I. F(i)) = (\i \ I. F(i))"
apply (subst JOIN_cons [symmetric])
apply (auto simp add: cons_absorb)
done

lemma JOIN_Un: "(\i \ I \ J. F(i)) = ((\i \ I. F(i)) \ (\i \ J. F(i)))"
apply (rule program_equalityI)
apply (simp_all add: UN_Un INT_Un)
apply (simp_all del: INT_simps add: INT_extend_simps, blast)
done

lemma JOIN_constant: "(\i \ I. c) = (if I=0 then SKIP else programify(c))"
by (rule program_equalityI, auto)

lemma JOIN_Join_distrib:
     "(\i \ I. F(i) \ G(i)) = (\i \ I. F(i)) \ (\i \ I. G(i))"
apply (rule program_equalityI)
apply (simp_all add: INT_Int_distrib, blast)
done

lemma JOIN_Join_miniscope: "(\i \ I. F(i) \ G) = ((\i \ I. F(i) \ G))"
by (simp add: JOIN_Join_distrib JOIN_constant)

text\<open>Used to prove guarantees_JOIN_I\<close>
lemma JOIN_Join_diff: "i \ I==>F(i) \ JOIN(I - {i}, F) = JOIN(I, F)"
apply (rule program_equalityI)
apply (auto elim!: not_emptyE)
done

subsection\<open>Safety: co, stable, FP\<close>

(*Fails if I=0 because it collapses to SKIP \<in> A co B, i.e. to A\<subseteq>B.  So an
  alternative precondition is A\<subseteq>B, but most proofs using this rule require
  I to be nonempty for other reasons anyway.*)

lemma JOIN_constrains:
"i \ I==>(\i \ I. F(i)) \ A co B \ (\i \ I. programify(F(i)) \ A co B)"

apply (unfold constrains_def JOIN_def st_set_def, auto)
prefer 2 apply blast
apply (rename_tac j act y z)
apply (cut_tac F = "F (j) " in Acts_type)
apply (drule_tac x = act in bspec, auto)
done

lemma Join_constrains [iff]:
     "(F \ G \ A co B) \ (programify(F) \ A co B & programify(G) \ A co B)"
by (auto simp add: constrains_def)

lemma Join_unless [iff]:
     "(F \ G \ A unless B) \
    (programify(F) \<in> A unless B & programify(G) \<in> A unless B)"
by (simp add: Join_constrains unless_def)

(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
  reachable (F \<squnion> G) could be much bigger than reachable F, reachable G
*)

lemma Join_constrains_weaken:
     "[| F \ A co A'; G \ B co B' |]
      ==> F \<squnion> G \<in> (A \<inter> B) co (A' \<union> B')"
apply (subgoal_tac "st_set (A) & st_set (B) & F \ program & G \ program")
prefer 2 apply (blast dest: constrainsD2, simp)
apply (blast intro: constrains_weaken)
done

(*If I=0, it degenerates to SKIP \<in> state co 0, which is false.*)
lemma JOIN_constrains_weaken:
  assumes major: "(!!i. i \ I ==> F(i) \ A(i) co A'(i))"
      and minor: "i \ I"
  shows "(\i \ I. F(i)) \ (\i \ I. A(i)) co (\i \ I. A'(i))"
apply (cut_tac minor)
apply (simp (no_asm_simp) add: JOIN_constrains)
apply clarify
apply (rename_tac "j")
apply (frule_tac i = j in major)
apply (frule constrainsD2, simp)
apply (blast intro: constrains_weaken)
done

lemma JOIN_stable:
     "(\i \ I. F(i)) \ stable(A) \ ((\i \ I. programify(F(i)) \ stable(A)) & st_set(A))"
apply (auto simp add: stable_def constrains_def JOIN_def)
apply (cut_tac F = "F (i) " in Acts_type)
apply (drule_tac x = act in bspec, auto)
done

lemma initially_JOIN_I:
  assumes major: "(!!i. i \ I ==>F(i) \ initially(A))"
      and minor: "i \ I"
  shows  "(\i \ I. F(i)) \ initially(A)"
apply (cut_tac minor)
apply (auto elim!: not_emptyE simp add: Inter_iff initially_def)
apply (frule_tac i = x in major)
apply (auto simp add: initially_def)
done

lemma invariant_JOIN_I:
  assumes major: "(!!i. i \ I ==> F(i) \ invariant(A))"
      and minor: "i \ I"
  shows "(\i \ I. F(i)) \ invariant(A)"
apply (cut_tac minor)
apply (auto intro!: initially_JOIN_I dest: major simp add: invariant_def JOIN_stable)
apply (erule_tac V = "i \ I" in thin_rl)
apply (frule major)
apply (drule_tac [2] major)
apply (auto simp add: invariant_def)
apply (frule stableD2, force)+
done

lemma Join_stable [iff]:
     " (F \ G \ stable(A)) \
      (programify(F) \<in> stable(A) & programify(G) \<in>  stable(A))"
by (simp add: stable_def)

lemma initially_JoinI [intro!]:
     "[| F \ initially(A); G \ initially(A) |] ==> F \ G \ initially(A)"
by (unfold initially_def, auto)

lemma invariant_JoinI:
     "[| F \ invariant(A); G \ invariant(A) |]
      ==> F \<squnion> G \<in> invariant(A)"
apply (subgoal_tac "F \ program&G \ program")
prefer 2 apply (blast dest: invariantD2)
apply (simp add: invariant_def)
apply (auto intro: Join_in_program)
done

(* Fails if I=0 because \<Inter>i \<in> 0. A(i) = 0 *)
lemma FP_JOIN: "i \ I ==> FP(\i \ I. F(i)) = (\i \ I. FP (programify(F(i))))"
by (auto simp add: FP_def Inter_def st_set_def JOIN_stable)

subsection\<open>Progress: transient, ensures\<close>

lemma JOIN_transient:
     "i \ I ==>
      (\<Squnion>i \<in> I. F(i)) \<in> transient(A) \<longleftrightarrow> (\<exists>i \<in> I. programify(F(i)) \<in> transient(A))"
apply (auto simp add: transient_def JOIN_def)
apply (unfold st_set_def)
apply (drule_tac [2] x = act in bspec)
apply (auto dest: Acts_type [THEN subsetD])
done

lemma Join_transient [iff]:
     "F \ G \ transient(A) \
      (programify(F) \<in> transient(A) | programify(G) \<in> transient(A))"
apply (auto simp add: transient_def Join_def Int_Un_distrib2)
done

lemma Join_transient_I1: "F \ transient(A) ==> F \ G \ transient(A)"
by (simp add: Join_transient transientD2)

lemma Join_transient_I2: "G \ transient(A) ==> F \ G \ transient(A)"
by (simp add: Join_transient transientD2)

(*If I=0 it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A\<subseteq>B) *)
lemma JOIN_ensures:
     "i \ I ==>
      (\<Squnion>i \<in> I. F(i)) \<in> A ensures B \<longleftrightarrow>
      ((\<forall>i \<in> I. programify(F(i)) \<in> (A-B) co (A \<union> B)) &
      (\<exists>i \<in> I. programify(F(i)) \<in> A ensures B))"
by (auto simp add: ensures_def JOIN_constrains JOIN_transient)

lemma Join_ensures:
     "F \ G \ A ensures B \
      (programify(F) \<in> (A-B) co (A \<union> B) & programify(G) \<in> (A-B) co (A \<union> B) &
       (programify(F) \<in>  transient (A-B) | programify(G) \<in> transient (A-B)))"

apply (unfold ensures_def)
apply (auto simp add: Join_transient)
done

lemma stable_Join_constrains:
    "[| F \ stable(A); G \ A co A' |]
     ==> F \<squnion> G \<in> A co A'"
apply (unfold stable_def constrains_def Join_def st_set_def)
apply (cut_tac F = F in Acts_type)
apply (cut_tac F = G in Acts_type, force)
done

(*Premise for G cannot use Always because  F \<in> Stable A  is
   weaker than G \<in> stable A *)
lemma stable_Join_Always1:
     "[| F \ stable(A); G \ invariant(A) |] ==> F \ G \ Always(A)"
apply (subgoal_tac "F \ program & G \ program & st_set (A) ")
prefer 2 apply (blast dest: invariantD2 stableD2)
apply (simp add: Always_def invariant_def initially_def Stable_eq_stable)
apply (force intro: stable_Int)
done

(*As above, but exchanging the roles of F and G*)
lemma stable_Join_Always2:
     "[| F \ invariant(A); G \ stable(A) |] ==> F \ G \ Always(A)"
apply (subst Join_commute)
apply (blast intro: stable_Join_Always1)
done

lemma stable_Join_ensures1:
     "[| F \ stable(A); G \ A ensures B |] ==> F \ G \ A ensures B"
apply (subgoal_tac "F \ program & G \ program & st_set (A) ")
prefer 2 apply (blast dest: stableD2 ensures_type [THEN subsetD])
apply (simp (no_asm_simp) add: Join_ensures)
apply (simp add: stable_def ensures_def)
apply (erule constrains_weaken, auto)
done

(*As above, but exchanging the roles of F and G*)
lemma stable_Join_ensures2:
     "[| F \ A ensures B; G \ stable(A) |] ==> F \ G \ A ensures B"
apply (subst Join_commute)
apply (blast intro: stable_Join_ensures1)
done

subsection\<open>The ok and OK relations\<close>

lemma ok_SKIP1 [iff]: "SKIP ok F"
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)

lemma ok_SKIP2 [iff]: "F ok SKIP"
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)

lemma ok_Join_commute:
     "(F ok G & (F \ G) ok H) \ (G ok H & F ok (G \ H))"
by (auto simp add: ok_def)

lemma ok_commute: "(F ok G) \(G ok F)"
by (auto simp add: ok_def)

lemmas ok_sym = ok_commute [THEN iffD1]

lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) \ (F ok G & (F \ G) ok H)"
by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb
                 Int_Un_distrib2 Ball_def,  safe, force+)

lemma ok_Join_iff1 [iff]: "F ok (G \ H) \ (F ok G & F ok H)"
by (auto simp add: ok_def)

lemma ok_Join_iff2 [iff]: "(G \ H) ok F \ (G ok F & H ok F)"
by (auto simp add: ok_def)

(*useful?  Not with the previous two around*)
lemma ok_Join_commute_I: "[| F ok G; (F \ G) ok H |] ==> F ok (G \ H)"
by (auto simp add: ok_def)

lemma ok_JOIN_iff1 [iff]: "F ok JOIN(I,G) \ (\i \ I. F ok G(i))"
by (force dest: Acts_type [THEN subsetD] elim!: not_emptyE simp add: ok_def)

lemma ok_JOIN_iff2 [iff]: "JOIN(I,G) ok F \ (\i \ I. G(i) ok F)"
apply (auto elim!: not_emptyE simp add: ok_def)
apply (blast dest: Acts_type [THEN subsetD])
done

lemma OK_iff_ok: "OK(I,F) \ (\i \ I. \j \ I-{i}. F(i) ok (F(j)))"
by (auto simp add: ok_def OK_def)

lemma OK_imp_ok: "[| OK(I,F); i \ I; j \ I; i\j|] ==> F(i) ok F(j)"
by (auto simp add: OK_iff_ok)

lemma OK_0 [iff]: "OK(0,F)"
by (simp add: OK_def)

lemma OK_cons_iff:
     "OK(cons(i, I), F) \
      (i \<in> I & OK(I, F)) | (i\<notin>I & OK(I, F) & F(i) ok JOIN(I,F))"
apply (simp add: OK_iff_ok)
apply (blast intro: ok_sym)
done

subsection\<open>Allowed\<close>

lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program"
by (auto dest: Acts_type [THEN subsetD] simp add: Allowed_def)

lemma Allowed_Join [simp]:
     "Allowed(F \ G) =
   Allowed(programify(F)) \<inter> Allowed(programify(G))"
apply (auto simp add: Allowed_def)
done

lemma Allowed_JOIN [simp]:
     "i \ I ==>
   Allowed(JOIN(I,F)) = (\<Inter>i \<in> I. Allowed(programify(F(i))))"
apply (auto simp add: Allowed_def, blast)
done

lemma ok_iff_Allowed:
     "F ok G \ (programify(F) \ Allowed(programify(G)) &
   programify(G) \<in> Allowed(programify(F)))"
by (simp add: ok_def Allowed_def)

lemma OK_iff_Allowed:
     "OK(I,F) \
  (\<forall>i \<in> I. \<forall>j \<in> I-{i}. programify(F(i)) \<in> Allowed(programify(F(j))))"
apply (auto simp add: OK_iff_ok ok_iff_Allowed)
done

subsection\<open>safety_prop, for reasoning about given instances of "ok"\<close>

lemma safety_prop_Acts_iff:
     "safety_prop(X) ==> (Acts(G) \ cons(id(state), (\F \ X. Acts(F)))) \ (programify(G) \ X)"
apply (simp (no_asm_use) add: safety_prop_def)
apply clarify
apply (case_tac "G \ program", simp_all, blast, safe)
prefer 2 apply force
apply (force simp add: programify_def)
done

lemma safety_prop_AllowedActs_iff_Allowed:
     "safety_prop(X) ==>
  (\<Union>G \<in> X. Acts(G)) \<subseteq> AllowedActs(F) \<longleftrightarrow> (X \<subseteq> Allowed(programify(F)))"
apply (simp add: Allowed_def safety_prop_Acts_iff [THEN iff_sym]
                 safety_prop_def, blast)
done

lemma Allowed_eq:
     "safety_prop(X) ==> Allowed(mk_program(init, acts, \F \ X. Acts(F))) = X"
apply (subgoal_tac "cons (id (state), \(RepFun (X, Acts)) \ Pow (state * state)) = \(RepFun (X, Acts))")
apply (rule_tac [2] equalityI)
  apply (simp del: UN_simps add: Allowed_def safety_prop_Acts_iff safety_prop_def, auto)
apply (force dest: Acts_type [THEN subsetD] simp add: safety_prop_def)+
done

lemma def_prg_Allowed:
     "[| F == mk_program (init, acts, \F \ X. Acts(F)); safety_prop(X) |]
      ==> Allowed(F) = X"
by (simp add: Allowed_eq)

(*For safety_prop to hold, the property must be satisfiable!*)
lemma safety_prop_constrains [iff]:
     "safety_prop(A co B) \ (A \ B & st_set(A))"
by (simp add: safety_prop_def constrains_def st_set_def, blast)

(* To be used with resolution *)
lemma safety_prop_constrainsI [iff]:
     "[| A\B; st_set(A) |] ==>safety_prop(A co B)"
by auto

lemma safety_prop_stable [iff]: "safety_prop(stable(A)) \ st_set(A)"
by (simp add: stable_def)

lemma safety_prop_stableI: "st_set(A) ==> safety_prop(stable(A))"
by auto

lemma safety_prop_Int [simp]:
     "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X \ Y)"
apply (simp add: safety_prop_def, safe, blast)
apply (drule_tac [2] B = "\(RepFun (X \ Y, Acts))" and C = "\(RepFun (Y, Acts))" in subset_trans)
apply (drule_tac B = "\(RepFun (X \ Y, Acts))" and C = "\(RepFun (X, Acts))" in subset_trans)
apply blast+
done

(* If I=0 the conclusion becomes safety_prop(0) which is false *)
lemma safety_prop_Inter:
  assumes major: "(!!i. i \ I ==>safety_prop(X(i)))"
      and minor: "i \ I"
  shows "safety_prop(\i \ I. X(i))"
apply (simp add: safety_prop_def)
apply (cut_tac minor, safe)
apply (simp (no_asm_use) add: Inter_iff)
apply clarify
apply (frule major)
apply (drule_tac [2] i = xa in major)
apply (frule_tac [4] i = xa in major)
apply (auto simp add: safety_prop_def)
apply (drule_tac B = "\(RepFun (\(RepFun (I, X)), Acts))" and C = "\(RepFun (X (xa), Acts))" in subset_trans)
apply blast+
done

lemma def_UNION_ok_iff:
"[| F == mk_program(init,acts, \G \ X. Acts(G)); safety_prop(X) |]
      ==> F ok G \<longleftrightarrow> (programify(G) \<in> X & acts \<inter> Pow(state*state) \<subseteq> AllowedActs(G))"
apply (unfold ok_def)
apply (drule_tac G = G in safety_prop_Acts_iff)
apply (cut_tac F = G in AllowedActs_type)
apply (cut_tac F = G in Acts_type, auto)
done

end

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.