Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ZF_examples.thy Sprache: Isabelle

Original von: Isabelle^©

section\<open>Examples of Reasoning in ZF Set Theory\<close>

theory ZF_examples imports ZFC begin

subsection \<open>Binary Trees\<close>

consts
  bt :: "i => i"

datatype "bt(A)" =
  Lf | Br ("a \ A", "t1 \ bt(A)", "t2 \ bt(A)")

declare bt.intros [simp]

text\<open>Induction via tactic emulation\<close>
lemma Br_neq_left [rule_format]: "l \ bt(A) ==> \x r. Br(x, l, r) \ l"
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
  apply (induct_tac l)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
  apply auto
  done

(*
  apply (Inductive.case_tac l)
  apply (tactic {*exhaust_tac "l" 1*})
*)

text\<open>The new induction method, which I don't understand\<close>
lemma Br_neq_left': "l \ bt(A) ==> (!!x r. Br(x, l, r) \ l)"
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
  apply (induct set: bt)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
  apply auto
  done

lemma Br_iff: "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'"
  \<comment> \<open>Proving a freeness theorem.\<close>
  by (blast elim!: bt.free_elims)

inductive_cases Br_in_bt: "Br(a,l,r) \ bt(A)"
  \<comment> \<open>An elimination rule, for type-checking.\<close>

text \<open>
@{thm[display] Br_in_bt[no_vars]}
\<close>

subsection\<open>Primitive recursion\<close>

consts  n_nodes :: "i => i"
primrec
  "n_nodes(Lf) = 0"
  "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"

lemma n_nodes_type [simp]: "t \ bt(A) ==> n_nodes(t) \ nat"
  by (induct_tac t, auto)

consts  n_nodes_aux :: "i => i"
primrec
  "n_nodes_aux(Lf) = (\k \ nat. k)"
  "n_nodes_aux(Br(a,l,r)) =
      (\<lambda>k \<in> nat. n_nodes_aux(r) `  (n_nodes_aux(l) ` succ(k)))"

lemma n_nodes_aux_eq [rule_format]:
     "t \ bt(A) ==> \k \ nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
  by (induct_tac t, simp_all)

definition n_nodes_tail :: "i => i" where
   "n_nodes_tail(t) == n_nodes_aux(t) ` 0"

lemma "t \ bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
by (simp add: n_nodes_tail_def n_nodes_aux_eq)

subsection \<open>Inductive definitions\<close>

consts  Fin       :: "i=>i"
inductive
  domains   "Fin(A)" \<subseteq> "Pow(A)"
  intros
    emptyI:  "0 \ Fin(A)"
    consI:   "[| a \ A; b \ Fin(A) |] ==> cons(a,b) \ Fin(A)"
  type_intros  empty_subsetI cons_subsetI PowI
  type_elims   PowD [elim_format]

consts  acc :: "i => i"
inductive
  domains "acc(r)" \<subseteq> "field(r)"
  intros
    vimage:  "[| r-``{a}: Pow(acc(r)); a \ field(r) |] ==> a \ acc(r)"
  monos      Pow_mono

consts
  llist  :: "i=>i"

codatatype
  "llist(A)" = LNil | LCons ("a \ A", "l \ llist(A)")

(*Coinductive definition of equality*)
consts
  lleq :: "i=>i"

(*Previously used <*> in the domain and variant pairs as elements.  But
  standard pairs work just as well.  To use variant pairs, must change prefix
  a q/Q to the Sigma, Pair and converse rules.*)
coinductive
  domains "lleq(A)" \<subseteq> "llist(A) * llist(A)"
  intros
    LNil:  " \ lleq(A)"
    LCons: "[| a \ A; \ lleq(A) |]
            ==> <LCons(a,l), LCons(a,l')> \ lleq(A)"
  type_intros  llist.intros

subsection\<open>Powerset example\<close>

lemma Pow_mono: "A\B ==> Pow(A) \ Pow(B)"
apply (rule subsetI)
apply (rule PowI)
apply (drule PowD)
apply (erule subset_trans, assumption)
done

lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule equalityI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule Int_greatest)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule Int_lower1 [THEN Pow_mono])
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule Int_lower2 [THEN Pow_mono])
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule subsetI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule IntE)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule PowI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (drule PowD)+
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule Int_greatest)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (assumption+)
done

text\<open>Trying again from the beginning in order to use \<open>blast\<close>\<close>
lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
by blast

lemma "C\D ==> Union(C) \ Union(D)"
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule subsetI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule UnionE)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule UnionI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule subsetD)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
done

text\<open>A more abstract version of the same proof\<close>

lemma "C\D ==> Union(C) \ Union(D)"
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule Union_least)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule Union_upper)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule subsetD, assumption)
done

lemma "[| a \ A; f \ A->B; g \ C->D; A \ C = 0 |] ==> (f \ g)`a = f`a"
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule apply_equality)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule UnI1)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule apply_Pair)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule fun_disjoint_Un)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
done

end

¤ Dauer der Verarbeitung: 0.16 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.