(* Title: HOL/Import/HOL_Light_Maps.thy
Author: Cezary Kaliszyk, University of Innsbruck
Author: Alexander Krauss, QAware GmbH
Based on earlier code by Steven Obua and Sebastian Skalberg
*)
section \<open>Type and constant mappings of HOL Light importer\<close>
theory HOL_Light_Maps
imports Import_Setup
begin
lemma [import_const T]:
"True = ((\p :: bool. p) = (\p. p))"
by simp
lemma [import_const "/\\"]:
"(\) = (\p q. (\f. f p q :: bool) = (\f. f True True))"
by metis
lemma [import_const "==>"]:
"(\) = (\(p::bool) q::bool. (p \ q) = p)"
by auto
lemma [import_const "!"]:
"All = (\P::'A \ bool. P = (\x::'A. True))"
by auto
lemma [import_const "?"]:
"Ex = (\P::'A \ bool. All (\q::bool. (All (\x::'A::type. (P x) \ q)) \ q))"
by auto
lemma [import_const "\\/"]:
"(\) = (\p q. \r. (p \ r) \ (q \ r) \ r)"
by auto
lemma [import_const F]:
"False = (\p. p)"
by auto
lemma [import_const "~"]:
"Not = (\p. p \ False)"
by simp
lemma [import_const "?!"]:
"Ex1 = (\P::'A \ bool. Ex P \ (\x y. P x \ P y \ x = y))"
by auto
lemma [import_const "_FALSITY_"]: "False = False"
by simp
lemma hl_ax1: "\t::'A \ 'B. (\x. t x) = t"
by metis
lemma hl_ax2: "\P x::'A. P x \ P (Eps P)"
by (auto intro: someI)
lemma [import_const COND]:
"If = (\t (t1 :: 'A) t2. SOME x. (t = True \ x = t1) \ (t = False \ x = t2))"
unfolding fun_eq_iff by auto
lemma [import_const o]:
"(\) = (\(f::'B \ 'C) g x::'A. f (g x))"
unfolding fun_eq_iff by simp
lemma [import_const I]: "id = (\x::'A. x)"
by auto
lemma [import_type 1 one_ABS one_REP]:
"type_definition Rep_unit Abs_unit (Collect (\b. b))"
by (metis (full_types) Collect_cong singleton_conv2 type_definition_unit)
lemma [import_const one]: "() = (SOME x::unit. True)"
by auto
lemma [import_const mk_pair]:
"Pair_Rep = (\(x::'A) (y::'B) (a::'A) b::'B. a = x \ b = y)"
by (simp add: Pair_Rep_def fun_eq_iff)
lemma [import_type prod ABS_prod REP_prod]:
"type_definition Rep_prod Abs_prod (Collect (\x::'A \ 'B \ bool. \a b. x = Pair_Rep a b))"
using type_definition_prod[unfolded Product_Type.prod_def] by simp
lemma [import_const ","]: "Pair = (\(x::'A) y::'B. Abs_prod (Pair_Rep x y))"
by (metis Pair_def)
lemma [import_const FST]:
"fst = (\p::'A \ 'B. SOME x::'A. \y::'B. p = (x, y))"
by auto
lemma [import_const SND]:
"snd = (\p::'A \ 'B. SOME y::'B. \x::'A. p = (x, y))"
by auto
lemma CURRY_DEF[import_const CURRY]:
"curry = (\(f::'A \ 'B \ 'C) x y. f (x, y))"
using curry_def .
lemma [import_const ONE_ONE : inj]:
"inj = (\(f::'A \ 'B). \x1 x2. f x1 = f x2 \ x1 = x2)"
by (auto simp add: fun_eq_iff inj_on_def)
lemma [import_const ONTO : surj]:
"surj = (\(f::'A \ 'B). \y. \x. y = f x)"
by (auto simp add: fun_eq_iff)
lemma hl_ax3: "\f::ind \ ind. inj f \ \ surj f"
by (rule_tac x="Suc_Rep" in exI)
(metis Suc_Rep_inject' injI Suc_Rep_not_Zero_Rep surjD)
import_type_map num : nat
import_const_map "_0" : zero_class.zero
import_const_map SUC : Suc
lemma NOT_SUC: "\n. Suc n \ 0"
by simp
lemma SUC_INJ: "\m n. (Suc m = Suc n) = (m = n)"
by simp
lemma num_INDUCTION:
"\P. P 0 \ (\n. P n \ P (Suc n)) \ (\n. P n)"
by (auto intro: nat.induct)
lemma [import_const NUMERAL]: "id = (\x :: nat. x)"
by auto
definition [simp]: "bit0 n = 2 * n"
lemma [import_const BIT0]:
"bit0 = (SOME fn. fn (id 0) = id 0 \ (\n. fn (Suc n) = Suc (Suc (fn n))))"
apply (auto intro!: some_equality[symmetric])
apply (auto simp add: fun_eq_iff)
apply (induct_tac x)
apply auto
done
definition [import_const BIT1, simp]:
"bit1 = (\x. Suc (bit0 x))"
definition [simp]: "pred n = n - 1"
lemma PRE[import_const PRE : pred]:
"pred (id (0::nat)) = id (0::nat) \ (\n::nat. pred (Suc n) = n)"
by simp
lemma ADD[import_const "+" : plus]:
"(\n :: nat. (id 0) + n = n) \ (\m n. (Suc m) + n = Suc (m + n))"
by simp
lemma MULT[import_const "*" : times]:
"(\n :: nat. (id 0) * n = id 0) \ (\m n. (Suc m) * n = (m * n) + n)"
by simp
lemma EXP[import_const EXP : power]:
"(\m. m ^ (id 0) = id (bit1 0)) \ (\(m :: nat) n. m ^ (Suc n) = m * (m ^ n))"
by simp
lemma LE[import_const "<=" : less_eq]:
"(\m :: nat. m \ (id 0) = (m = id 0)) \ (\m n. m \ (Suc n) = (m = Suc n \ m \ n))"
by auto
lemma LT[import_const "<" : less]:
"(\m :: nat. m < (id 0) = False) \ (\m n. m < (Suc n) = (m = n \ m < n))"
by auto
lemma DEF_GE[import_const ">=" : greater_eq]:
"(\) = (\x y :: nat. y \ x)"
by simp
lemma DEF_GT[import_const ">" : greater]:
"(>) = (\x y :: nat. y < x)"
by simp
lemma DEF_MAX[import_const "MAX"]:
"max = (\x y :: nat. if x \ y then y else x)"
by (auto simp add: max.absorb_iff2 fun_eq_iff)
lemma DEF_MIN[import_const "MIN"]:
"min = (\x y :: nat. if x \ y then x else y)"
by (auto simp add: min.absorb_iff1 fun_eq_iff)
definition even
where
"even = Parity.even"
lemma EVEN[import_const "EVEN" : even]:
"even (id 0::nat) = True \ (\n. even (Suc n) = (\ even n))"
by (simp add: even_def)
lemma SUB[import_const "-" : minus]:
"(\m::nat. m - (id 0) = m) \ (\m n. m - (Suc n) = pred (m - n))"
by simp
lemma FACT[import_const "FACT" : fact]:
"fact (id 0) = id (bit1 0) \ (\n. fact (Suc n) = Suc n * fact n)"
by simp
import_const_map MOD : modulo
import_const_map DIV : divide
lemma DIVISION_0:
"\m n::nat. if n = id 0 then m div n = id 0 \ m mod n = m else m = m div n * n + m mod n \ m mod n < n"
by simp
lemmas [import_type sum "_dest_sum" "_mk_sum"] = type_definition_sum[where 'a="'A" and 'b="'B"]
import_const_map INL : Inl
import_const_map INR : Inr
lemma sum_INDUCT:
"\P. (\a :: 'A. P (Inl a)) \ (\a :: 'B. P (Inr a)) \ (\x. P x)"
by (auto intro: sum.induct)
lemma sum_RECURSION:
"\Inl' Inr'. \fn. (\a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \ (\a :: 'B. fn (Inr a) = Inr' a)"
by (intro allI, rule_tac x="case_sum Inl' Inr'" in exI) auto
lemma OUTL[import_const "OUTL" : projl]:
"Sum_Type.projl (Inl x) = x"
by simp
lemma OUTR[import_const "OUTR" : projr]:
"Sum_Type.projr (Inr y) = y"
by simp
import_type_map list : list
import_const_map NIL : Nil
import_const_map CONS : Cons
lemma list_INDUCT:
"\P::'A list \ bool. P [] \ (\a0 a1. P a1 \ P (a0 # a1)) \ (\x. P x)"
using list.induct by auto
lemma list_RECURSION:
"\nil' cons'. \fn::'A list \ 'Z. fn [] = nil' \ (\(a0::'A) a1::'A list. fn (a0 # a1) = cons' a0 a1 (fn a1))"
by (intro allI, rule_tac x="rec_list nil' cons'" in exI) auto
lemma HD[import_const HD : hd]:
"hd ((h::'A) # t) = h"
by simp
lemma TL[import_const TL : tl]:
"tl ((h::'A) # t) = t"
by simp
lemma APPEND[import_const APPEND : append]:
"(\l::'A list. [] @ l = l) \ (\(h::'A) t l. (h # t) @ l = h # t @ l)"
by simp
lemma REVERSE[import_const REVERSE : rev]:
"rev [] = ([] :: 'A list) \ rev ((x::'A) # l) = rev l @ [x]"
by simp
lemma LENGTH[import_const LENGTH : length]:
"length ([] :: 'A list) = id 0 \ (\(h::'A) t. length (h # t) = Suc (length t))"
by simp
lemma MAP[import_const MAP : map]:
"(\f::'A \ 'B. map f [] = []) \
(\<forall>(f::'A \<Rightarrow> 'B) h t. map f (h # t) = f h # map f t)"
by simp
lemma LAST[import_const LAST : last]:
"last ((h::'A) # t) = (if t = [] then h else last t)"
by simp
lemma BUTLAST[import_const BUTLAST : butlast]:
"butlast [] = ([] :: 't18337 list) \
butlast ((h :: 't18337) # t) = (if t = [] then [] else h # butlast t)"
by simp
lemma REPLICATE[import_const REPLICATE : replicate]:
"replicate (id (0::nat)) (x::'t18358) = [] \
replicate (Suc n) x = x # replicate n x"
by simp
lemma NULL[import_const NULL : List.null]:
"List.null ([]::'t18373 list) = True \ List.null ((h::'t18373) # t) = False"
unfolding null_def by simp
lemma ALL[import_const ALL : list_all]:
"list_all (P::'t18393 \ bool) [] = True \
list_all P (h # t) = (P h \<and> list_all P t)"
by simp
lemma EX[import_const EX : list_ex]:
"list_ex (P::'t18414 \ bool) [] = False \
list_ex P (h # t) = (P h \<or> list_ex P t)"
by simp
lemma ITLIST[import_const ITLIST : foldr]:
"foldr (f::'t18437 \ 't18436 \ 't18436) [] b = b \
foldr f (h # t) b = f h (foldr f t b)"
by simp
lemma ALL2_DEF[import_const ALL2 : list_all2]:
"list_all2 (P::'t18495 \ 't18502 \ bool) [] (l2::'t18502 list) = (l2 = []) \
list_all2 P ((h1::'t18495) # (t1::'t18495 list)) l2 =
(if l2 = [] then False else P h1 (hd l2) \<and> list_all2 P t1 (tl l2))"
by simp (induct_tac l2, simp_all)
lemma FILTER[import_const FILTER : filter]:
"filter (P::'t18680 \ bool) [] = [] \
filter P ((h::'t18680) # t) = (if P h then h # filter P t else filter P t)"
by simp
lemma ZIP[import_const ZIP : zip]:
"zip [] [] = ([] :: ('t18824 \ 't18825) list) \
zip ((h1::'t18849) # t1) ((h2::'t18850) # t2) = (h1, h2) # zip t1 t2"
by simp
lemma WF[import_const WF : wfP]:
"\u. wfP u \ (\P. (\x :: 'A. P x) \ (\x. P x \ (\y. u y x \ \ P y)))"
proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
fix x :: "'a \ 'a \ bool" and xa :: "'a" and Q
assume a: "xa \ Q"
assume "\P. Ex P \ (\xa. P xa \ (\y. x y xa \ \ P y))"
then have "Ex (\x. x \ Q) \ (\xa. (\x. x \ Q) xa \ (\y. x y xa \ \ (\x. x \ Q) y))" by auto
then show "\z\Q. \y. x y z \ y \ Q" using a by auto
next
fix x P and xa :: 'A and z
assume "P xa" "z \ {a. P a}" "\y. x y z \ y \ {a. P a}"
then show "\xa. P xa \ (\y. x y xa \ \ P y)" by auto
qed auto
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
