<commit_before>(*  Title:      HOL/Import/HOL_Light_Maps.thy
    Author:     <NAME>, University of Innsbruck
    Author:     <NAME>, QAware GmbH

Based on earlier code by <NAME> and <NAME>
*)

header {* Type and constant mappings of HOL Light importer *}

theory HOL_Light_Maps
imports Import_Setup
begin

lemma [import_const T]:
  "True = ((\<lambda>p :: bool. p) = (\<lambda>p. p))"
  by simp

lemma [import_const "/\\"]:
  "(op \<and>) = (\<lambda>p q. (\<lambda>f. f p q \<Colon> bool) = (\<lambda>f. f True True))"
  by metis

lemma [import_const "==>"]:
  "(op \<longrightarrow>) = (\<lambda>(p\<Colon>bool) q\<Colon>bool. (p \<and> q) = p)"
  by auto

lemma [import_const "!"]:
  "All = (\<lambda>P\<Colon>'A \<Rightarrow> bool. P = (\<lambda>x\<Colon>'A. True))"
  by auto

lemma [import_const "?"]:
  "Ex = (\<lambda>P\<Colon>'A \<Rightarrow> bool. All (\<lambda>q\<Colon>bool. (All (\<lambda>x\<Colon>'A\<Colon>type. (P x) \<longrightarrow> q)) \<longrightarrow> q))"
  by auto

lemma [import_const "\\/"]:
  "(op \<or>) = (\<lambda>p q. \<forall>r. (p \<longrightarrow> r) \<longrightarrow> (q \<longrightarrow> r) \<longrightarrow> r)"
  by auto

lemma [import_const F]:
  "False = (\<forall>p. p)"
  by auto

lemma [import_const "~"]:
  "Not = (\<lambda>p. p \<longrightarrow> False)"
  by simp

lemma [import_const "?!"]:
  "Ex1 = (\<lambda>P\<Colon>'A \<Rightarrow> bool. Ex P \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y))"
  by auto

lemma [import_const "_FALSITY_"]: "False = False"
  by simp

lemma hl_ax1: "\<forall>t\<Colon>'A \<Rightarrow> 'B. (\<lambda>x. t x) = t"
  by metis

lemma hl_ax2: "\<forall>P x\<Colon>'A. P x \<longrightarrow> P (Eps P)"
  by (auto intro: someI)

lemma [import_const COND]:
  "If = (\<lambda>t (t1 :: 'A) t2. SOME x. (t = True \<longrightarrow> x = t1) \<and> (t = False \<longrightarrow> x = t2))"
  unfolding fun_eq_iff by auto

lemma [import_const o]:
  "(op \<circ>) = (\<lambda>(f\<Colon>'B \<Rightarrow> 'C) g x\<Colon>'A. f (g x))"
  unfolding fun_eq_iff by simp

lemma [import_const I]: "id = (\<lambda>x\<Colon>'A. x)"
  by auto

lemma [import_type 1 one_ABS one_REP]:
  "type_definition Rep_unit Abs_unit (Collect (\<lambda>b. b))"
  by (metis (full_types) Collect_cong singleton_conv2 type_definition_unit)

lemma [import_const one]: "() = (SOME x\<Colon>unit. True)"
  by auto

lemma [import_const mk_pair]:
  "Pair_Rep = (\<lambda>(x\<Colon>'A) (y\<Colon>'B) (a\<Colon>'A) b\<Colon>'B. a = x \<and> 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 (\<lambda>x\<Colon>'A \<Rightarrow> 'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b))"
  using type_definition_prod[unfolded Product_Type.prod_def] by simp

lemma [import_const ","]: "Pair = (\<lambda>(x\<Colon>'A) y\<Colon>'B. Abs_prod (Pair_Rep x y))"
  by (metis Pair_def)

lemma [import_const FST]:
  "fst = (\<lambda>p\<Colon>'A \<times> 'B. SOME x\<Colon>'A. \<exists>y\<Colon>'B. p = (x, y))"
  by auto

lemma [import_const SND]:
  "snd = (\<lambda>p\<Colon>'A \<times> 'B. SOME y\<Colon>'B. \<exists>x\<Colon>'A. p = (x, y))"
  by auto

lemma CURRY_DEF[import_const CURRY]:
  "curry = (\<lambda>(f\<Colon>'A \<times> 'B \<Rightarrow> 'C) x y. f (x, y))"
  using curry_def .

lemma [import_const ONE_ONE : inj]:
  "inj = (\<lambda>(f\<Colon>'A \<Rightarrow> 'B). \<forall>x1 x2. f x1 = f x2 \<longrightarrow> x1 = x2)"
  by (auto simp add: fun_eq_iff inj_on_def)

lemma [import_const ONTO : surj]:
  "surj = (\<lambda>(f\<Colon>'A \<Rightarrow> 'B). \<forall>y. \<exists>x. y = f x)"
  by (auto simp add: fun_eq_iff)

lemma hl_ax3: "\<exists>f\<Colon>ind \<Rightarrow> ind. inj f \<and> \<not> 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: "\<forall>n. Suc n \<noteq> 0"
  by simp

lemma SUC_INJ: "\<forall>m n. (Suc m = Suc n) = (m = n)"
  by simp

lemma num_INDUCTION:
  "\<forall>P. P 0 \<and> (\<forall>n. P n \<longrightarrow> P (Suc n)) \<longrightarrow> (\<forall>n. P n)"
  by (auto intro: nat.induct)

lemma [import_const NUMERAL]: "id = (\<lambda>x :: nat. x)"
  by auto

definition [simp]: "bit0 n = 2 * n"

lemma [import_const BIT0]:
  "bit0 = (SOME fn. fn (id 0) = id 0 \<and> (\<forall>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 = (\<lambda>x. Suc (bit0 x))"

definition [simp]: "pred n = n - 1"

lemma PRE[import_const PRE : pred]:
  "pred (id (0\<Colon>nat)) = id (0\<Colon>nat) \<and> (\<forall>n\<Colon>nat. pred (Suc n) = n)"
  by simp

lemma ADD[import_const "+" : plus]:
  "(\<forall>n :: nat. (id 0) + n = n) \<and> (\<forall>m n. (Suc m) + n = Suc (m + n))"
  by simp

lemma MULT[import_const "*" : times]:
  "(\<forall>n :: nat. (id 0) * n = id 0) \<and> (\<forall>m n. (Suc m) * n = (m * n) + n)"
  by simp

lemma EXP[import_const EXP : power]:
  "(\<forall>m. m ^ (id 0) = id (bit1 0)) \<and> (\<forall>(m :: nat) n. m ^ (Suc n) = m * (m ^ n))"
  by simp

lemma LE[import_const "<=" : less_eq]:
  "(\<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))"
  by auto

lemma LT[import_const "<" : less]:
  "(\<forall>m :: nat. m < (id 0) = False) \<and> (\<forall>m n. m < (Suc n) = (m = n \<or> m < n))"
  by auto

lemma DEF_GE[import_const ">=" : greater_eq]:
  "(op \<ge>) = (\<lambda>x y :: nat. y \<le> x)"
  by simp

lemma DEF_GT[import_const ">" : greater]:
  "(op >) = (\<lambda>x y :: nat. y < x)"
  by simp

lemma DEF_MAX[import_const "MAX"]:
  "max = (\<lambda>x y :: nat. if x \<le> y then y else x)"
  by (auto simp add: max.absorb_iff2 fun_eq_iff)

lemma DEF_MIN[import_const "MIN"]:
  "min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
  by (auto simp add: min.absorb_iff1 fun_eq_iff)

lemma EVEN[import_const "EVEN" : even]:
  "even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
  by simp

lemma SUB[import_const "-" : minus]:
  "(\<forall>m\<Colon>nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))"
  by simp

lemma FACT[import_const "FACT" : fact]:
  "fact (id 0) = id (bit1 0) \<and> (\<forall>n. fact (Suc n) = Suc n * fact n)"
  by simp

import_const_map MOD : mod
import_const_map DIV : div

lemma DIVISION_0:
  "\<forall>m n\<Colon>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"
  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:
  "\<forall>P. (\<forall>a :: 'A. P (Inl a)) \<and> (\<forall>a :: 'B. P (Inr a)) \<longrightarrow> (\<forall>x. P x)"
  by (auto intro: sum.induct)

lemma sum_RECURSION:
  "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>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]:<commit_msg>explicit definition restores HOL Light import after cb9d84d3e7f2<commit_after>(*  Title:      HOL/Import/HOL_Light_Maps.thy
    Author:     <NAME>, University of Innsbruck
    Author:     <NAME>, QAware GmbH

Based on earlier code by <NAME> and <NAME>
*)

header {* Type and constant mappings of HOL Light importer *}

theory HOL_Light_Maps
imports Import_Setup
begin

lemma [import_const T]:
  "True = ((\<lambda>p :: bool. p) = (\<lambda>p. p))"
  by simp

lemma [import_const "/\\"]:
  "(op \<and>) = (\<lambda>p q. (\<lambda>f. f p q \<Colon> bool) = (\<lambda>f. f True True))"
  by metis

lemma [import_const "==>"]:
  "(op \<longrightarrow>) = (\<lambda>(p\<Colon>bool) q\<Colon>bool. (p \<and> q) = p)"
  by auto

lemma [import_const "!"]:
  "All = (\<lambda>P\<Colon>'A \<Rightarrow> bool. P = (\<lambda>x\<Colon>'A. True))"
  by auto

lemma [import_const "?"]:
  "Ex = (\<lambda>P\<Colon>'A \<Rightarrow> bool. All (\<lambda>q\<Colon>bool. (All (\<lambda>x\<Colon>'A\<Colon>type. (P x) \<longrightarrow> q)) \<longrightarrow> q))"
  by auto

lemma [import_const "\\/"]:
  "(op \<or>) = (\<lambda>p q. \<forall>r. (p \<longrightarrow> r) \<longrightarrow> (q \<longrightarrow> r) \<longrightarrow> r)"
  by auto

lemma [import_const F]:
  "False = (\<forall>p. p)"
  by auto

lemma [import_const "~"]:
  "Not = (\<lambda>p. p \<longrightarrow> False)"
  by simp

lemma [import_const "?!"]:
  "Ex1 = (\<lambda>P\<Colon>'A \<Rightarrow> bool. Ex P \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y))"
  by auto

lemma [import_const "_FALSITY_"]: "False = False"
  by simp

lemma hl_ax1: "\<forall>t\<Colon>'A \<Rightarrow> 'B. (\<lambda>x. t x) = t"
  by metis

lemma hl_ax2: "\<forall>P x\<Colon>'A. P x \<longrightarrow> P (Eps P)"
  by (auto intro: someI)

lemma [import_const COND]:
  "If = (\<lambda>t (t1 :: 'A) t2. SOME x. (t = True \<longrightarrow> x = t1) \<and> (t = False \<longrightarrow> x = t2))"
  unfolding fun_eq_iff by auto

lemma [import_const o]:
  "(op \<circ>) = (\<lambda>(f\<Colon>'B \<Rightarrow> 'C) g x\<Colon>'A. f (g x))"
  unfolding fun_eq_iff by simp

lemma [import_const I]: "id = (\<lambda>x\<Colon>'A. x)"
  by auto

lemma [import_type 1 one_ABS one_REP]:
  "type_definition Rep_unit Abs_unit (Collect (\<lambda>b. b))"
  by (metis (full_types) Collect_cong singleton_conv2 type_definition_unit)

lemma [import_const one]: "() = (SOME x\<Colon>unit. True)"
  by auto

lemma [import_const mk_pair]:
  "Pair_Rep = (\<lambda>(x\<Colon>'A) (y\<Colon>'B) (a\<Colon>'A) b\<Colon>'B. a = x \<and> 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 (\<lambda>x\<Colon>'A \<Rightarrow> 'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b))"
  using type_definition_prod[unfolded Product_Type.prod_def] by simp

lemma [import_const ","]: "Pair = (\<lambda>(x\<Colon>'A) y\<Colon>'B. Abs_prod (Pair_Rep x y))"
  by (metis Pair_def)

lemma [import_const FST]:
  "fst = (\<lambda>p\<Colon>'A \<times> 'B. SOME x\<Colon>'A. \<exists>y\<Colon>'B. p = (x, y))"
  by auto

lemma [import_const SND]:
  "snd = (\<lambda>p\<Colon>'A \<times> 'B. SOME y\<Colon>'B. \<exists>x\<Colon>'A. p = (x, y))"
  by auto

lemma CURRY_DEF[import_const CURRY]:
  "curry = (\<lambda>(f\<Colon>'A \<times> 'B \<Rightarrow> 'C) x y. f (x, y))"
  using curry_def .

lemma [import_const ONE_ONE : inj]:
  "inj = (\<lambda>(f\<Colon>'A \<Rightarrow> 'B). \<forall>x1 x2. f x1 = f x2 \<longrightarrow> x1 = x2)"
  by (auto simp add: fun_eq_iff inj_on_def)

lemma [import_const ONTO : surj]:
  "surj = (\<lambda>(f\<Colon>'A \<Rightarrow> 'B). \<forall>y. \<exists>x. y = f x)"
  by (auto simp add: fun_eq_iff)

lemma hl_ax3: "\<exists>f\<Colon>ind \<Rightarrow> ind. inj f \<and> \<not> 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: "\<forall>n. Suc n \<noteq> 0"
  by simp

lemma SUC_INJ: "\<forall>m n. (Suc m = Suc n) = (m = n)"
  by simp

lemma num_INDUCTION:
  "\<forall>P. P 0 \<and> (\<forall>n. P n \<longrightarrow> P (Suc n)) \<longrightarrow> (\<forall>n. P n)"
  by (auto intro: nat.induct)

lemma [import_const NUMERAL]: "id = (\<lambda>x :: nat. x)"
  by auto

definition [simp]: "bit0 n = 2 * n"

lemma [import_const BIT0]:
  "bit0 = (SOME fn. fn (id 0) = id 0 \<and> (\<forall>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 = (\<lambda>x. Suc (bit0 x))"

definition [simp]: "pred n = n - 1"

lemma PRE[import_const PRE : pred]:
  "pred (id (0\<Colon>nat)) = id (0\<Colon>nat) \<and> (\<forall>n\<Colon>nat. pred (Suc n) = n)"
  by simp

lemma ADD[import_const "+" : plus]:
  "(\<forall>n :: nat. (id 0) + n = n) \<and> (\<forall>m n. (Suc m) + n = Suc (m + n))"
  by simp

lemma MULT[import_const "*" : times]:
  "(\<forall>n :: nat. (id 0) * n = id 0) \<and> (\<forall>m n. (Suc m) * n = (m * n) + n)"
  by simp

lemma EXP[import_const EXP : power]:
  "(\<forall>m. m ^ (id 0) = id (bit1 0)) \<and> (\<forall>(m :: nat) n. m ^ (Suc n) = m * (m ^ n))"
  by simp

lemma LE[import_const "<=" : less_eq]:
  "(\<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))"
  by auto

lemma LT[import_const "<" : less]:
  "(\<forall>m :: nat. m < (id 0) = False) \<and> (\<forall>m n. m < (Suc n) = (m = n \<or> m < n))"
  by auto

lemma DEF_GE[import_const ">=" : greater_eq]:
  "(op \<ge>) = (\<lambda>x y :: nat. y \<le> x)"
  by simp

lemma DEF_GT[import_const ">" : greater]:
  "(op >) = (\<lambda>x y :: nat. y < x)"
  by simp

lemma DEF_MAX[import_const "MAX"]:
  "max = (\<lambda>x y :: nat. if x \<le> y then y else x)"
  by (auto simp add: max.absorb_iff2 fun_eq_iff)

lemma DEF_MIN[import_const "MIN"]:
  "min = (\<lambda>x y :: nat. if x \<le> 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\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
  by (simp add: even_def)

lemma SUB[import_const "-" : minus]:
  "(\<forall>m\<Colon>nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))"
  by simp

lemma FACT[import_const "FACT" : fact]:
  "fact (id 0) = id (bit1 0) \<and> (\<forall>n. fact (Suc n) = Suc n * fact n)"
  by simp

import_const_map MOD : mod
import_const_map DIV : div

lemma DIVISION_0:
  "\<forall>m n\<Colon>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"
  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:
  "\<forall>P. (\<forall>a :: 'A. P (Inl a)) \<and> (\<forall>a :: 'B. P (Inr a)) \<longrightarrow> (\<forall>x. P x)"
  by (auto intro: sum.induct)

lemma sum_RECURSION:
  "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>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]:
{'fraction_non_alphanumeric': 0.20752915501602673, 'fraction_numerical': 0.0072290799972720456, 'mean_word_length': 3.4954015941140404, 'pattern_counts': {'":': 0, '<': 385, '<?xml version=': 0, '>': 379, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5304458', 'n_tokens_mistral': 6537, 'n_tokens_neox': 6039, 'n_words': 1841}