products/sources/formale Sprachen/Isabelle/HOL/Import image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: HOL_Light_Maps.thy   Sprache: Isabelle

Original von: 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

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.14 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff