src/HOL/Import/HOL4Setup.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 14620 1be590fd2422 child 16417 9bc16273c2d4 permissions -rw-r--r--
import -> imports
```     1 (*  Title:      HOL/Import/HOL4Setup.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Sebastian Skalberg (TU Muenchen)
```
```     4 *)
```
```     5
```
```     6 theory HOL4Setup = MakeEqual
```
```     7   files ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML"):
```
```     8
```
```     9 section {* General Setup *}
```
```    10
```
```    11 lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q"
```
```    12   by auto
```
```    13
```
```    14 lemma HOLallI: "(!! bogus. P bogus) \<Longrightarrow> (ALL bogus. P bogus)"
```
```    15 proof -
```
```    16   assume "!! bogus. P bogus"
```
```    17   thus "ALL x. P x"
```
```    18     ..
```
```    19 qed
```
```    20
```
```    21 consts
```
```    22   ONE_ONE :: "('a => 'b) => bool"
```
```    23   ONTO    :: "('a => 'b) => bool"
```
```    24
```
```    25 defs
```
```    26   ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
```
```    27   ONTO_DEF   : "ONTO f == ALL y. EX x. y = f x"
```
```    28
```
```    29 lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV"
```
```    30   by (simp add: ONE_ONE_DEF inj_on_def)
```
```    31
```
```    32 lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(ONTO f))"
```
```    33 proof (rule exI,safe)
```
```    34   show "inj Suc_Rep"
```
```    35     by (rule inj_Suc_Rep)
```
```    36 next
```
```    37   assume "ONTO Suc_Rep"
```
```    38   hence "ALL y. EX x. y = Suc_Rep x"
```
```    39     by (simp add: ONTO_DEF surj_def)
```
```    40   hence "EX x. Zero_Rep = Suc_Rep x"
```
```    41     by (rule spec)
```
```    42   thus False
```
```    43   proof (rule exE)
```
```    44     fix x
```
```    45     assume "Zero_Rep = Suc_Rep x"
```
```    46     hence "Suc_Rep x = Zero_Rep"
```
```    47       ..
```
```    48     with Suc_Rep_not_Zero_Rep
```
```    49     show False
```
```    50       ..
```
```    51   qed
```
```    52 qed
```
```    53
```
```    54 lemma EXISTS_DEF: "Ex P = P (Eps P)"
```
```    55 proof (rule iffI)
```
```    56   assume "Ex P"
```
```    57   thus "P (Eps P)"
```
```    58     ..
```
```    59 next
```
```    60   assume "P (Eps P)"
```
```    61   thus "Ex P"
```
```    62     ..
```
```    63 qed
```
```    64
```
```    65 consts
```
```    66   TYPE_DEFINITION :: "('a => bool) => ('b => 'a) => bool"
```
```    67
```
```    68 defs
```
```    69   TYPE_DEFINITION: "TYPE_DEFINITION p rep == ((ALL x y. (rep x = rep y) --> (x = y)) & (ALL x. (p x = (EX y. x = rep y))))"
```
```    70
```
```    71 lemma ex_imp_nonempty: "Ex P ==> EX x. x : (Collect P)"
```
```    72   by simp
```
```    73
```
```    74 lemma light_ex_imp_nonempty: "P t ==> EX x. x : (Collect P)"
```
```    75 proof -
```
```    76   assume "P t"
```
```    77   hence "EX x. P x"
```
```    78     ..
```
```    79   thus ?thesis
```
```    80     by (rule ex_imp_nonempty)
```
```    81 qed
```
```    82
```
```    83 lemma light_imp_as: "[| Q --> P; P --> Q |] ==> P = Q"
```
```    84   by blast
```
```    85
```
```    86 lemma typedef_hol2hol4:
```
```    87   assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)"
```
```    88   shows "EX rep. TYPE_DEFINITION P (rep::'a=>'b)"
```
```    89 proof -
```
```    90   from a
```
```    91   have td: "(ALL x. P (Rep x)) & (ALL x. Abs (Rep x) = x) & (ALL y. P y \<longrightarrow> Rep (Abs y) = y)"
```
```    92     by (simp add: type_definition_def)
```
```    93   have ed: "TYPE_DEFINITION P Rep"
```
```    94   proof (auto simp add: TYPE_DEFINITION)
```
```    95     fix x y
```
```    96     assume "Rep x = Rep y"
```
```    97     from td have "x = Abs (Rep x)"
```
```    98       by auto
```
```    99     also have "Abs (Rep x) = Abs (Rep y)"
```
```   100       by (simp add: prems)
```
```   101     also from td have "Abs (Rep y) = y"
```
```   102       by auto
```
```   103     finally show "x = y" .
```
```   104   next
```
```   105     fix x
```
```   106     assume "P x"
```
```   107     with td
```
```   108     have "Rep (Abs x) = x"
```
```   109       by auto
```
```   110     hence "x = Rep (Abs x)"
```
```   111       ..
```
```   112     thus "EX y. x = Rep y"
```
```   113       ..
```
```   114   next
```
```   115     fix y
```
```   116     from td
```
```   117     show "P (Rep y)"
```
```   118       by auto
```
```   119   qed
```
```   120   show ?thesis
```
```   121     apply (rule exI [of _ Rep])
```
```   122     apply (rule ed)
```
```   123     .
```
```   124 qed
```
```   125
```
```   126 lemma typedef_hol2hollight:
```
```   127   assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)"
```
```   128   shows "(Abs (Rep a) = a) & (P r = (Rep (Abs r) = r))"
```
```   129 proof
```
```   130   from a
```
```   131   show "Abs (Rep a) = a"
```
```   132     by (rule type_definition.Rep_inverse)
```
```   133 next
```
```   134   show "P r = (Rep (Abs r) = r)"
```
```   135   proof
```
```   136     assume "P r"
```
```   137     hence "r \<in> (Collect P)"
```
```   138       by simp
```
```   139     with a
```
```   140     show "Rep (Abs r) = r"
```
```   141       by (rule type_definition.Abs_inverse)
```
```   142   next
```
```   143     assume ra: "Rep (Abs r) = r"
```
```   144     from a
```
```   145     have "Rep (Abs r) \<in> (Collect P)"
```
```   146       by (rule type_definition.Rep)
```
```   147     thus "P r"
```
```   148       by (simp add: ra)
```
```   149   qed
```
```   150 qed
```
```   151
```
```   152 lemma termspec_help: "[| Ex P ; c == Eps P |] ==> P c"
```
```   153   apply simp
```
```   154   apply (rule someI_ex)
```
```   155   .
```
```   156
```
```   157 lemma typedef_helper: "EX x. P x \<Longrightarrow> EX x. x \<in> (Collect P)"
```
```   158   by simp
```
```   159
```
```   160 use "hol4rews.ML"
```
```   161
```
```   162 setup hol4_setup
```
```   163 parse_ast_translation smarter_trueprop_parsing
```
```   164
```
```   165 use "proof_kernel.ML"
```
```   166 use "replay.ML"
```
```   167 use "import_package.ML"
```
```   168
```
```   169 setup ImportPackage.setup
```
```   170
```
```   171 end
```