author | wenzelm |
Sat, 24 Mar 2018 20:51:42 +0100 | |
changeset 67945 | 984c3dc46cc0 |
parent 67399 | eab6ce8368fa |
child 73869 | 7181130f5872 |
permissions | -rw-r--r-- |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
1 |
(* Title: HOL/Import/HOL_Light_Maps.thy |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
2 |
Author: Cezary Kaliszyk, University of Innsbruck |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
3 |
Author: Alexander Krauss, QAware GmbH |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
4 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
5 |
Based on earlier code by Steven Obua and Sebastian Skalberg |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
6 |
*) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
7 |
|
63167 | 8 |
section \<open>Type and constant mappings of HOL Light importer\<close> |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
9 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
10 |
theory HOL_Light_Maps |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
11 |
imports Import_Setup |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
12 |
begin |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
13 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
14 |
lemma [import_const T]: |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
15 |
"True = ((\<lambda>p :: bool. p) = (\<lambda>p. p))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
16 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
17 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
18 |
lemma [import_const "/\\"]: |
67399 | 19 |
"(\<and>) = (\<lambda>p q. (\<lambda>f. f p q :: bool) = (\<lambda>f. f True True))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
20 |
by metis |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
21 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
22 |
lemma [import_const "==>"]: |
67399 | 23 |
"(\<longrightarrow>) = (\<lambda>(p::bool) q::bool. (p \<and> q) = p)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
24 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
25 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
26 |
lemma [import_const "!"]: |
61076 | 27 |
"All = (\<lambda>P::'A \<Rightarrow> bool. P = (\<lambda>x::'A. True))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
28 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
29 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
30 |
lemma [import_const "?"]: |
61076 | 31 |
"Ex = (\<lambda>P::'A \<Rightarrow> bool. All (\<lambda>q::bool. (All (\<lambda>x::'A::type. (P x) \<longrightarrow> q)) \<longrightarrow> q))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
32 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
33 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
34 |
lemma [import_const "\\/"]: |
67399 | 35 |
"(\<or>) = (\<lambda>p q. \<forall>r. (p \<longrightarrow> r) \<longrightarrow> (q \<longrightarrow> r) \<longrightarrow> r)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
36 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
37 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
38 |
lemma [import_const F]: |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
39 |
"False = (\<forall>p. p)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
40 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
41 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
42 |
lemma [import_const "~"]: |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
43 |
"Not = (\<lambda>p. p \<longrightarrow> False)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
44 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
45 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
46 |
lemma [import_const "?!"]: |
61076 | 47 |
"Ex1 = (\<lambda>P::'A \<Rightarrow> bool. Ex P \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
48 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
49 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
50 |
lemma [import_const "_FALSITY_"]: "False = False" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
51 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
52 |
|
61076 | 53 |
lemma hl_ax1: "\<forall>t::'A \<Rightarrow> 'B. (\<lambda>x. t x) = t" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
54 |
by metis |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
55 |
|
61076 | 56 |
lemma hl_ax2: "\<forall>P x::'A. P x \<longrightarrow> P (Eps P)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
57 |
by (auto intro: someI) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
58 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
59 |
lemma [import_const COND]: |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
60 |
"If = (\<lambda>t (t1 :: 'A) t2. SOME x. (t = True \<longrightarrow> x = t1) \<and> (t = False \<longrightarrow> x = t2))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
61 |
unfolding fun_eq_iff by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
62 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
63 |
lemma [import_const o]: |
67399 | 64 |
"(\<circ>) = (\<lambda>(f::'B \<Rightarrow> 'C) g x::'A. f (g x))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
65 |
unfolding fun_eq_iff by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
66 |
|
61076 | 67 |
lemma [import_const I]: "id = (\<lambda>x::'A. x)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
68 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
69 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
70 |
lemma [import_type 1 one_ABS one_REP]: |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
71 |
"type_definition Rep_unit Abs_unit (Collect (\<lambda>b. b))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
72 |
by (metis (full_types) Collect_cong singleton_conv2 type_definition_unit) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
73 |
|
61076 | 74 |
lemma [import_const one]: "() = (SOME x::unit. True)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
75 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
76 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
77 |
lemma [import_const mk_pair]: |
61076 | 78 |
"Pair_Rep = (\<lambda>(x::'A) (y::'B) (a::'A) b::'B. a = x \<and> b = y)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
79 |
by (simp add: Pair_Rep_def fun_eq_iff) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
80 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
81 |
lemma [import_type prod ABS_prod REP_prod]: |
61076 | 82 |
"type_definition Rep_prod Abs_prod (Collect (\<lambda>x::'A \<Rightarrow> 'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
83 |
using type_definition_prod[unfolded Product_Type.prod_def] by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
84 |
|
61076 | 85 |
lemma [import_const ","]: "Pair = (\<lambda>(x::'A) y::'B. Abs_prod (Pair_Rep x y))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
86 |
by (metis Pair_def) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
87 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
88 |
lemma [import_const FST]: |
61076 | 89 |
"fst = (\<lambda>p::'A \<times> 'B. SOME x::'A. \<exists>y::'B. p = (x, y))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
90 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
91 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
92 |
lemma [import_const SND]: |
61076 | 93 |
"snd = (\<lambda>p::'A \<times> 'B. SOME y::'B. \<exists>x::'A. p = (x, y))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
94 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
95 |
|
47364
637074507956
HOL/Import more precise map types
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47258
diff
changeset
|
96 |
lemma CURRY_DEF[import_const CURRY]: |
61076 | 97 |
"curry = (\<lambda>(f::'A \<times> 'B \<Rightarrow> 'C) x y. f (x, y))" |
47364
637074507956
HOL/Import more precise map types
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47258
diff
changeset
|
98 |
using curry_def . |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
99 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
100 |
lemma [import_const ONE_ONE : inj]: |
61076 | 101 |
"inj = (\<lambda>(f::'A \<Rightarrow> 'B). \<forall>x1 x2. f x1 = f x2 \<longrightarrow> x1 = x2)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
102 |
by (auto simp add: fun_eq_iff inj_on_def) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
103 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
104 |
lemma [import_const ONTO : surj]: |
61076 | 105 |
"surj = (\<lambda>(f::'A \<Rightarrow> 'B). \<forall>y. \<exists>x. y = f x)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
106 |
by (auto simp add: fun_eq_iff) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
107 |
|
61076 | 108 |
lemma hl_ax3: "\<exists>f::ind \<Rightarrow> ind. inj f \<and> \<not> surj f" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
109 |
by (rule_tac x="Suc_Rep" in exI) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
110 |
(metis Suc_Rep_inject' injI Suc_Rep_not_Zero_Rep surjD) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
111 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
112 |
import_type_map num : nat |
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
113 |
import_const_map "_0" : zero_class.zero |
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
114 |
import_const_map SUC : Suc |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
115 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
116 |
lemma NOT_SUC: "\<forall>n. Suc n \<noteq> 0" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
117 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
118 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
119 |
lemma SUC_INJ: "\<forall>m n. (Suc m = Suc n) = (m = n)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
120 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
121 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
122 |
lemma num_INDUCTION: |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
123 |
"\<forall>P. P 0 \<and> (\<forall>n. P n \<longrightarrow> P (Suc n)) \<longrightarrow> (\<forall>n. P n)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
124 |
by (auto intro: nat.induct) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
125 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
126 |
lemma [import_const NUMERAL]: "id = (\<lambda>x :: nat. x)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
127 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
128 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
129 |
definition [simp]: "bit0 n = 2 * n" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
130 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
131 |
lemma [import_const BIT0]: |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
132 |
"bit0 = (SOME fn. fn (id 0) = id 0 \<and> (\<forall>n. fn (Suc n) = Suc (Suc (fn n))))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
133 |
apply (auto intro!: some_equality[symmetric]) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
134 |
apply (auto simp add: fun_eq_iff) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
135 |
apply (induct_tac x) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
136 |
apply auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
137 |
done |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
138 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
139 |
definition [import_const BIT1, simp]: |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
140 |
"bit1 = (\<lambda>x. Suc (bit0 x))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
141 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
142 |
definition [simp]: "pred n = n - 1" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
143 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
144 |
lemma PRE[import_const PRE : pred]: |
61076 | 145 |
"pred (id (0::nat)) = id (0::nat) \<and> (\<forall>n::nat. pred (Suc n) = n)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
146 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
147 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
148 |
lemma ADD[import_const "+" : plus]: |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
149 |
"(\<forall>n :: nat. (id 0) + n = n) \<and> (\<forall>m n. (Suc m) + n = Suc (m + n))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
150 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
151 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
152 |
lemma MULT[import_const "*" : times]: |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
153 |
"(\<forall>n :: nat. (id 0) * n = id 0) \<and> (\<forall>m n. (Suc m) * n = (m * n) + n)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
154 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
155 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
156 |
lemma EXP[import_const EXP : power]: |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
157 |
"(\<forall>m. m ^ (id 0) = id (bit1 0)) \<and> (\<forall>(m :: nat) n. m ^ (Suc n) = m * (m ^ n))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
158 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
159 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
160 |
lemma LE[import_const "<=" : less_eq]: |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
161 |
"(\<forall>m :: nat. m \<le> (id 0) = (m = id 0)) \<and> (\<forall>m n. m \<le> (Suc n) = (m = Suc n \<or> m \<le> n))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
162 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
163 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
164 |
lemma LT[import_const "<" : less]: |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
165 |
"(\<forall>m :: nat. m < (id 0) = False) \<and> (\<forall>m n. m < (Suc n) = (m = n \<or> m < n))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
166 |
by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
167 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
168 |
lemma DEF_GE[import_const ">=" : greater_eq]: |
67399 | 169 |
"(\<ge>) = (\<lambda>x y :: nat. y \<le> x)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
170 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
171 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
172 |
lemma DEF_GT[import_const ">" : greater]: |
67399 | 173 |
"(>) = (\<lambda>x y :: nat. y < x)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
174 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
175 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
176 |
lemma DEF_MAX[import_const "MAX"]: |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
177 |
"max = (\<lambda>x y :: nat. if x \<le> y then y else x)" |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
47364
diff
changeset
|
178 |
by (auto simp add: max.absorb_iff2 fun_eq_iff) |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
179 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
180 |
lemma DEF_MIN[import_const "MIN"]: |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
181 |
"min = (\<lambda>x y :: nat. if x \<le> y then x else y)" |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
47364
diff
changeset
|
182 |
by (auto simp add: min.absorb_iff1 fun_eq_iff) |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
183 |
|
58773
1b2e7b78a337
explicit definition restores HOL Light import after cb9d84d3e7f2
haftmann
parents:
56266
diff
changeset
|
184 |
definition even |
1b2e7b78a337
explicit definition restores HOL Light import after cb9d84d3e7f2
haftmann
parents:
56266
diff
changeset
|
185 |
where |
1b2e7b78a337
explicit definition restores HOL Light import after cb9d84d3e7f2
haftmann
parents:
56266
diff
changeset
|
186 |
"even = Parity.even" |
1b2e7b78a337
explicit definition restores HOL Light import after cb9d84d3e7f2
haftmann
parents:
56266
diff
changeset
|
187 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
188 |
lemma EVEN[import_const "EVEN" : even]: |
61076 | 189 |
"even (id 0::nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))" |
58773
1b2e7b78a337
explicit definition restores HOL Light import after cb9d84d3e7f2
haftmann
parents:
56266
diff
changeset
|
190 |
by (simp add: even_def) |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
191 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
192 |
lemma SUB[import_const "-" : minus]: |
61076 | 193 |
"(\<forall>m::nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
194 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
195 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
196 |
lemma FACT[import_const "FACT" : fact]: |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
197 |
"fact (id 0) = id (bit1 0) \<and> (\<forall>n. fact (Suc n) = Suc n * fact n)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
198 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
199 |
|
63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63167
diff
changeset
|
200 |
import_const_map MOD : modulo |
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
58889
diff
changeset
|
201 |
import_const_map DIV : divide |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
202 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
203 |
lemma DIVISION_0: |
61076 | 204 |
"\<forall>m n::nat. if n = id 0 then m div n = id 0 \<and> m mod n = m else m = m div n * n + m mod n \<and> m mod n < n" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
205 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
206 |
|
47364
637074507956
HOL/Import more precise map types
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47258
diff
changeset
|
207 |
lemmas [import_type sum "_dest_sum" "_mk_sum"] = type_definition_sum[where 'a="'A" and 'b="'B"] |
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
208 |
import_const_map INL : Inl |
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
209 |
import_const_map INR : Inr |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
210 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
211 |
lemma sum_INDUCT: |
47364
637074507956
HOL/Import more precise map types
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47258
diff
changeset
|
212 |
"\<forall>P. (\<forall>a :: 'A. P (Inl a)) \<and> (\<forall>a :: 'B. P (Inr a)) \<longrightarrow> (\<forall>x. P x)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
213 |
by (auto intro: sum.induct) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
214 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
215 |
lemma sum_RECURSION: |
47364
637074507956
HOL/Import more precise map types
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47258
diff
changeset
|
216 |
"\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>a :: 'B. fn (Inr a) = Inr' a)" |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55413
diff
changeset
|
217 |
by (intro allI, rule_tac x="case_sum Inl' Inr'" in exI) auto |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
218 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
219 |
lemma OUTL[import_const "OUTL" : projl]: |
55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
54863
diff
changeset
|
220 |
"Sum_Type.projl (Inl x) = x" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
221 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
222 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
223 |
lemma OUTR[import_const "OUTR" : projr]: |
55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
54863
diff
changeset
|
224 |
"Sum_Type.projr (Inr y) = y" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
225 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
226 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
227 |
import_type_map list : list |
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
228 |
import_const_map NIL : Nil |
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
229 |
import_const_map CONS : Cons |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
230 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
231 |
lemma list_INDUCT: |
61076 | 232 |
"\<forall>P::'A list \<Rightarrow> bool. P [] \<and> (\<forall>a0 a1. P a1 \<longrightarrow> P (a0 # a1)) \<longrightarrow> (\<forall>x. P x)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
233 |
using list.induct by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
234 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
235 |
lemma list_RECURSION: |
61076 | 236 |
"\<forall>nil' cons'. \<exists>fn::'A list \<Rightarrow> 'Z. fn [] = nil' \<and> (\<forall>(a0::'A) a1::'A list. fn (a0 # a1) = cons' a0 a1 (fn a1))" |
55413
a8e96847523c
adapted theories to '{case,rec}_{list,option}' names
blanchet
parents:
55393
diff
changeset
|
237 |
by (intro allI, rule_tac x="rec_list nil' cons'" in exI) auto |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
238 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
239 |
lemma HD[import_const HD : hd]: |
61076 | 240 |
"hd ((h::'A) # t) = h" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
241 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
242 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
243 |
lemma TL[import_const TL : tl]: |
61076 | 244 |
"tl ((h::'A) # t) = t" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
245 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
246 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
247 |
lemma APPEND[import_const APPEND : append]: |
61076 | 248 |
"(\<forall>l::'A list. [] @ l = l) \<and> (\<forall>(h::'A) t l. (h # t) @ l = h # t @ l)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
249 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
250 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
251 |
lemma REVERSE[import_const REVERSE : rev]: |
61076 | 252 |
"rev [] = ([] :: 'A list) \<and> rev ((x::'A) # l) = rev l @ [x]" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
253 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
254 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
255 |
lemma LENGTH[import_const LENGTH : length]: |
61076 | 256 |
"length ([] :: 'A list) = id 0 \<and> (\<forall>(h::'A) t. length (h # t) = Suc (length t))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
257 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
258 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
259 |
lemma MAP[import_const MAP : map]: |
61076 | 260 |
"(\<forall>f::'A \<Rightarrow> 'B. map f [] = []) \<and> |
261 |
(\<forall>(f::'A \<Rightarrow> 'B) h t. map f (h # t) = f h # map f t)" |
|
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
262 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
263 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
264 |
lemma LAST[import_const LAST : last]: |
61076 | 265 |
"last ((h::'A) # t) = (if t = [] then h else last t)" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
266 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
267 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
268 |
lemma BUTLAST[import_const BUTLAST : butlast]: |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
269 |
"butlast [] = ([] :: 't18337 list) \<and> |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
270 |
butlast ((h :: 't18337) # t) = (if t = [] then [] else h # butlast t)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
271 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
272 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
273 |
lemma REPLICATE[import_const REPLICATE : replicate]: |
61076 | 274 |
"replicate (id (0::nat)) (x::'t18358) = [] \<and> |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
275 |
replicate (Suc n) x = x # replicate n x" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
276 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
277 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
278 |
lemma NULL[import_const NULL : List.null]: |
61076 | 279 |
"List.null ([]::'t18373 list) = True \<and> List.null ((h::'t18373) # t) = False" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
280 |
unfolding null_def by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
281 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
282 |
lemma ALL[import_const ALL : list_all]: |
61076 | 283 |
"list_all (P::'t18393 \<Rightarrow> bool) [] = True \<and> |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
284 |
list_all P (h # t) = (P h \<and> list_all P t)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
285 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
286 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
287 |
lemma EX[import_const EX : list_ex]: |
61076 | 288 |
"list_ex (P::'t18414 \<Rightarrow> bool) [] = False \<and> |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
289 |
list_ex P (h # t) = (P h \<or> list_ex P t)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
290 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
291 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
292 |
lemma ITLIST[import_const ITLIST : foldr]: |
61076 | 293 |
"foldr (f::'t18437 \<Rightarrow> 't18436 \<Rightarrow> 't18436) [] b = b \<and> |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
294 |
foldr f (h # t) b = f h (foldr f t b)" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
295 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
296 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
297 |
lemma ALL2_DEF[import_const ALL2 : list_all2]: |
61076 | 298 |
"list_all2 (P::'t18495 \<Rightarrow> 't18502 \<Rightarrow> bool) [] (l2::'t18502 list) = (l2 = []) \<and> |
299 |
list_all2 P ((h1::'t18495) # (t1::'t18495 list)) l2 = |
|
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
300 |
(if l2 = [] then False else P h1 (hd l2) \<and> list_all2 P t1 (tl l2))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
301 |
by simp (induct_tac l2, simp_all) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
302 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
303 |
lemma FILTER[import_const FILTER : filter]: |
61076 | 304 |
"filter (P::'t18680 \<Rightarrow> bool) [] = [] \<and> |
305 |
filter P ((h::'t18680) # t) = (if P h then h # filter P t else filter P t)" |
|
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
306 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
307 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
308 |
lemma ZIP[import_const ZIP : zip]: |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
309 |
"zip [] [] = ([] :: ('t18824 \<times> 't18825) list) \<and> |
61076 | 310 |
zip ((h1::'t18849) # t1) ((h2::'t18850) # t2) = (h1, h2) # zip t1 t2" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
311 |
by simp |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
312 |
|
56266
da5f22a60cb3
formal check of user input, avoiding direct references of interal names;
wenzelm
parents:
55524
diff
changeset
|
313 |
lemma WF[import_const WF : wfP]: |
47364
637074507956
HOL/Import more precise map types
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47258
diff
changeset
|
314 |
"\<forall>u. wfP u \<longleftrightarrow> (\<forall>P. (\<exists>x :: 'A. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))" |
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
315 |
proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred]) |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
316 |
fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
317 |
assume a: "xa \<in> Q" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
318 |
assume "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
319 |
then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
320 |
then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
321 |
next |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
322 |
fix x P and xa :: 'A and z |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
323 |
assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}" |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
324 |
then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
325 |
qed auto |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
326 |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
327 |
end |
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
328 |