Quelle HOL_Light_Maps.thy Sprache: Isabelle

(*  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 (full_types))

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 num_Axiom:
  "\(e::'A) f. \!fn. fn 0 = e \ (\n. fn (Suc n) = f (fn n) n)"
  apply (intro allI)
  subgoal for e f
    apply (rule ex1I [where a = "Nat.rec_nat e (\a b. f b a)"])
     apply simp
    apply (rule ext)
    subgoal for fn x by (induct x) simp_all
    done
  done

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])
  subgoal for fn
    apply (rule ext)
    subgoal for x by (induct x) simp_all
    done
  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 (simp add: fun_eq_iff)

lemma DEF_MIN[import_const "MIN"]:
  "min = (\x y :: nat. if x \ y then x else y)"
  by (simp add: 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"
  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 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]:
  "\R. wfP R \ (\P. (\x :: 'A. P x) \ (\x. P x \ (\y. R y x \ \ P y)))"
proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
  fix R :: "'a \ 'a \ bool" and P :: "'a \ bool" and x z :: "'a"
  {
    fix Q
    assume a: "x \ Q"
    assume "\P. (\x. P x) \ (\x. P x \ (\y. R y x \ \ P y))"
    then have "(\x. x \ Q) \ (\x. (\x. x \ Q) x \ (\y. R y x \ y \ Q))" by auto
    with a show "\x\Q. \y. R y x \ y \ Q" by auto
  next
    assume "P x" "z \ {a. P a}" "\y. R y z \ y \ {a. P a}"
    then show "\x. P x \ (\y. R y x \ \ P y)" by auto
  }
qed auto

end

quality100%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.