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