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