src/HOL/Import/HOLLightCompat.thy
 author obua Mon Sep 12 15:52:00 2005 +0200 (2005-09-12) changeset 17322 781abf7011e6 child 19064 bf19cc5a7899 permissions -rw-r--r--
 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` obua@17322 ` 33` ```constdefs ``` obua@17322 ` 34` ``` Pred :: "nat \ nat" ``` obua@17322 ` 35` ``` "Pred n \ n - (Suc 0)" ``` obua@17322 ` 36` obua@17322 ` 37` ```lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))" ``` obua@17322 ` 38` ``` apply (rule some_equality[symmetric]) ``` obua@17322 ` 39` ``` apply (simp add: Pred_def) ``` obua@17322 ` 40` ``` apply (rule ext) ``` obua@17322 ` 41` ``` apply (induct_tac x) ``` obua@17322 ` 42` ``` apply (auto simp add: Pred_def) ``` obua@17322 ` 43` ``` done ``` obua@17322 ` 44` obua@17322 ` 45` ```lemma NUMERAL_rew[hol4rew]: "NUMERAL x = x" by (simp add: NUMERAL_def) ``` obua@17322 ` 46` obua@17322 ` 47` ```lemma REP_ABS_PAIR: "\ x y. Rep_Prod (Abs_Prod (Pair_Rep x y)) = Pair_Rep x y" ``` obua@17322 ` 48` ``` apply (subst Abs_Prod_inverse) ``` obua@17322 ` 49` ``` apply (auto simp add: Prod_def) ``` obua@17322 ` 50` ``` done ``` obua@17322 ` 51` obua@17322 ` 52` ```lemma fst_altdef: "fst = (%p. SOME x. EX y. p = (x, y))" ``` obua@17322 ` 53` ``` apply (rule ext, rule someI2) ``` obua@17322 ` 54` ``` apply (auto intro: fst_conv[symmetric]) ``` obua@17322 ` 55` ``` done ``` obua@17322 ` 56` obua@17322 ` 57` ```lemma snd_altdef: "snd = (%p. SOME x. EX y. p = (y, x))" ``` obua@17322 ` 58` ``` apply (rule ext, rule someI2) ``` obua@17322 ` 59` ``` apply (auto intro: snd_conv[symmetric]) ``` obua@17322 ` 60` ``` done ``` obua@17322 ` 61` obua@17322 ` 62` ```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 ` 63` ``` apply (rule some_equality[symmetric]) ``` obua@17322 ` 64` ``` apply auto ``` obua@17322 ` 65` ``` apply (rule ext)+ ``` obua@17322 ` 66` ``` apply (induct_tac x) ``` obua@17322 ` 67` ``` apply auto ``` obua@17322 ` 68` ``` done ``` obua@17322 ` 69` obua@17322 ` 70` ```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 ` 71` ``` apply (rule some_equality[symmetric]) ``` obua@17322 ` 72` ``` apply auto ``` obua@17322 ` 73` ``` apply (rule ext)+ ``` obua@17322 ` 74` ``` apply (induct_tac x) ``` obua@17322 ` 75` ``` apply auto ``` obua@17322 ` 76` ``` done ``` obua@17322 ` 77` obua@17322 ` 78` ```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 ` 79` ``` apply (simp add: Pred_def) ``` obua@17322 ` 80` ``` apply (rule some_equality[symmetric]) ``` obua@17322 ` 81` ``` apply auto ``` obua@17322 ` 82` ``` apply (rule ext)+ ``` obua@17322 ` 83` ``` apply (induct_tac xa) ``` obua@17322 ` 84` ``` apply auto ``` obua@17322 ` 85` ``` done ``` obua@17322 ` 86` obua@17322 ` 87` ```constdefs ``` obua@17322 ` 88` ``` NUMERAL_BIT0 :: "nat \ nat" ``` obua@17322 ` 89` ``` "NUMERAL_BIT0 n \ n + n" ``` obua@17322 ` 90` obua@17322 ` 91` ```lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)" ``` obua@17322 ` 92` ``` by (simp add: NUMERAL_BIT1_def) ``` obua@17322 ` 93` obua@17322 ` 94` obua@17322 ` 95` obua@17322 ` 96` ```end ```