src/HOL/Import/HOLLightCompat.thy
 author haftmann Mon Mar 01 13:40:23 2010 +0100 (2010-03-01) changeset 35416 d8d7d1b785af parent 19064 bf19cc5a7899 child 41589 bbd861837ebc permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
 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 \ nat" where ``` obua@17322 ` 34` ``` "Pred n \ 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: "\ 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 \ nat" where ``` obua@17322 ` 87` ``` "NUMERAL_BIT0 n \ 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 \ 'c) \ ('b \ 'c) \ (('a + 'b) \ '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: "\ f. (\ a. f (Inl a) = Inl' a) \ (\ 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 ```