src/ZF/Induct/Acc.thy
author nipkow
Sun, 04 Nov 2018 12:07:24 +0100
changeset 69232 2b913054a9cf
parent 65449 c82e63b11b8b
child 69593 3dda49e08b9d
permissions -rw-r--r--
Faster Braun tree functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
     1
(*  Title:      ZF/Induct/Acc.thy
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
     3
    Copyright   1994  University of Cambridge
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
     4
*)
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
     5
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
     6
section \<open>The accessible part of a relation\<close>
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
     7
65449
c82e63b11b8b clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents: 61798
diff changeset
     8
theory Acc imports ZF begin
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
     9
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    10
text \<open>
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    11
  Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}.
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    12
\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    13
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    14
consts
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    15
  acc :: "i => i"
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    16
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    17
inductive
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    18
  domains "acc(r)" \<subseteq> "field(r)"
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    19
  intros
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    20
    vimage:  "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    21
  monos      Pow_mono
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    22
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    23
text \<open>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    24
  The introduction rule must require @{prop "a \<in> field(r)"},
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    25
  otherwise \<open>acc(r)\<close> would be a proper class!
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    26
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    27
  \medskip
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    28
  The intended introduction rule:
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    29
\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    30
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    31
lemma accI: "[| !!b. <b,a>:r ==> b \<in> acc(r);  a \<in> field(r) |] ==> a \<in> acc(r)"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    32
  by (blast intro: acc.intros)
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    33
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    34
lemma acc_downward: "[| b \<in> acc(r);  <a,b>: r |] ==> a \<in> acc(r)"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    35
  by (erule acc.cases) blast
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    36
18414
560f89584ada acc_induct: proper tags;
wenzelm
parents: 16417
diff changeset
    37
lemma acc_induct [consumes 1, case_names vimage, induct set: acc]:
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    38
    "[| a \<in> acc(r);
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 35762
diff changeset
    39
        !!x. [| x \<in> acc(r);  \<forall>y. <y,x>:r \<longrightarrow> P(y) |] ==> P(x)
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    40
     |] ==> P(a)"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    41
  by (erule acc.induct) (blast intro: acc.intros)
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    42
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    43
lemma wf_on_acc: "wf[acc(r)](r)"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    44
  apply (rule wf_onI2)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    45
  apply (erule acc_induct)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    46
  apply fast
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    47
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    48
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    49
lemma acc_wfI: "field(r) \<subseteq> acc(r) \<Longrightarrow> wf(r)"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    50
  by (erule wf_on_acc [THEN wf_on_subset_A, THEN wf_on_field_imp_wf])
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    51
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    52
lemma acc_wfD: "wf(r) ==> field(r) \<subseteq> acc(r)"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    53
  apply (rule subsetI)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    54
  apply (erule wf_induct2, assumption)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    55
   apply (blast intro: accI)+
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    56
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    57
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 35762
diff changeset
    58
lemma wf_acc_iff: "wf(r) \<longleftrightarrow> field(r) \<subseteq> acc(r)"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    59
  by (rule iffI, erule acc_wfD, erule acc_wfI)
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    60
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    61
end