src/HOL/Import/HOLLightCompat.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 35416 d8d7d1b785af
child 41589 bbd861837ebc
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
obua@17322
     1
(*  Title:      HOL/Import/HOLLightCompat.thy
obua@17322
     2
    ID:         $Id$
obua@17322
     3
    Author:     Steven Obua and Sebastian Skalberg (TU Muenchen)
obua@17322
     4
*)
obua@17322
     5
obua@17322
     6
theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin
obua@17322
     7
obua@17322
     8
lemma light_imp_def: "(t1 --> t2) = ((t1 & t2) = t1)"
obua@17322
     9
  by auto;
obua@17322
    10
obua@17322
    11
lemma comb_rule: "[| P1 = P2 ; Q1 = Q2 |] ==> P1 Q1 = P2 Q2"
obua@17322
    12
  by simp
obua@17322
    13
obua@17322
    14
lemma light_and_def: "(t1 & t2) = ((%f. f t1 t2::bool) = (%f. f True True))"
obua@17322
    15
proof auto
obua@17322
    16
  assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
obua@17322
    17
  have b: "(%(x::bool) (y::bool). x) = (%x y. x)" ..
obua@17322
    18
  with a
obua@17322
    19
  have "t1 = True"
obua@17322
    20
    by (rule comb_rule)
obua@17322
    21
  thus t1
obua@17322
    22
    by simp
obua@17322
    23
next
obua@17322
    24
  assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
obua@17322
    25
  have b: "(%(x::bool) (y::bool). y) = (%x y. y)" ..
obua@17322
    26
  with a
obua@17322
    27
  have "t2 = True"
obua@17322
    28
    by (rule comb_rule)
obua@17322
    29
  thus t2
obua@17322
    30
    by simp
obua@17322
    31
qed
obua@17322
    32
haftmann@35416
    33
definition Pred :: "nat \<Rightarrow> nat" where
obua@17322
    34
   "Pred n \<equiv> n - (Suc 0)"
obua@17322
    35
obua@17322
    36
lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))"
obua@17322
    37
  apply (rule some_equality[symmetric])
obua@17322
    38
  apply (simp add: Pred_def)
obua@17322
    39
  apply (rule ext)
obua@17322
    40
  apply (induct_tac x)
obua@17322
    41
  apply (auto simp add: Pred_def)
obua@17322
    42
  done
obua@17322
    43
obua@17322
    44
lemma NUMERAL_rew[hol4rew]: "NUMERAL x = x" by (simp add: NUMERAL_def)
obua@17322
    45
obua@17322
    46
lemma REP_ABS_PAIR: "\<forall> x y. Rep_Prod (Abs_Prod (Pair_Rep x y)) = Pair_Rep x y"
obua@17322
    47
  apply (subst Abs_Prod_inverse)
obua@17322
    48
  apply (auto simp add: Prod_def)
obua@17322
    49
  done
obua@17322
    50
obua@17322
    51
lemma fst_altdef: "fst = (%p. SOME x. EX y. p = (x, y))"
obua@17322
    52
  apply (rule ext, rule someI2)
obua@17322
    53
  apply (auto intro: fst_conv[symmetric])
obua@17322
    54
  done
obua@17322
    55
obua@17322
    56
lemma snd_altdef: "snd = (%p. SOME x. EX y. p = (y, x))"
obua@17322
    57
  apply (rule ext, rule someI2)
obua@17322
    58
  apply (auto intro: snd_conv[symmetric])
obua@17322
    59
  done
obua@17322
    60
obua@17322
    61
lemma add_altdef: "op + = (SOME add. (ALL n. add 0 n = n) & (ALL m n. add (Suc m) n = Suc (add m n)))"
obua@17322
    62
  apply (rule some_equality[symmetric])
obua@17322
    63
  apply auto
obua@17322
    64
  apply (rule ext)+
obua@17322
    65
  apply (induct_tac x)
obua@17322
    66
  apply auto
obua@17322
    67
  done
obua@17322
    68
obua@17322
    69
lemma mult_altdef: "op * = (SOME mult. (ALL n. mult 0 n = 0) & (ALL m n. mult (Suc m) n = mult m n + n))"
obua@17322
    70
  apply (rule some_equality[symmetric])
obua@17322
    71
  apply auto
obua@17322
    72
  apply (rule ext)+
obua@17322
    73
  apply (induct_tac x)
obua@17322
    74
  apply auto
obua@17322
    75
  done
obua@17322
    76
obua@17322
    77
lemma sub_altdef: "op - = (SOME sub. (ALL m. sub m 0 = m) & (ALL m n. sub m (Suc n) = Pred (sub m n)))"
obua@17322
    78
  apply (simp add: Pred_def)
obua@17322
    79
  apply (rule some_equality[symmetric])
obua@17322
    80
  apply auto
obua@17322
    81
  apply (rule ext)+
obua@17322
    82
  apply (induct_tac xa)
obua@17322
    83
  apply auto
obua@17322
    84
  done
obua@17322
    85
haftmann@35416
    86
definition NUMERAL_BIT0 :: "nat \<Rightarrow> nat" where
obua@17322
    87
  "NUMERAL_BIT0 n \<equiv> n + n"
obua@17322
    88
obua@17322
    89
lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
obua@17322
    90
  by (simp add: NUMERAL_BIT1_def)
obua@17322
    91
obua@19064
    92
consts
obua@19064
    93
  sumlift :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> (('a + 'b) \<Rightarrow> 'c)"
obua@17322
    94
obua@19064
    95
primrec
obua@19064
    96
  "sumlift f g (Inl a) = f a"
obua@19064
    97
  "sumlift f g (Inr b) = g b"
obua@19064
    98
  
obua@19064
    99
lemma sum_Recursion: "\<exists> f. (\<forall> a. f (Inl a) = Inl' a) \<and> (\<forall> b. f (Inr b) = Inr' b)"
obua@19064
   100
  apply (rule exI[where x="sumlift Inl' Inr'"])
obua@19064
   101
  apply auto
obua@19064
   102
  done
obua@17322
   103
obua@17322
   104
end