Theory HOL_Light_Maps

(*  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 ‹Type and constant mappings of HOL Light importer›

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 [] = []) ∧
       (∀(f::'A ⇒ '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 ∧ 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 ∨ 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) ∧ 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