Up to index of Isabelle/Bali4
theory Basis = PreBasis(* Title: isabelle/Bali/Basis.thy
ID: $Id: Basis.thy,v 1.28 2000/07/14 14:48:59 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Definitions extending HOL as logical basis of Bali
*)
Basis = PreBasis +
constdefs
the_Inl :: "'a + 'b \<Rightarrow> 'a"
"the_Inl x \<equiv> \<epsilon>a. x = Inl a"
the_Inr :: "'a + 'b \<Rightarrow> 'b"
"the_Inr x \<equiv> \<epsilon>b. x = Inr b"
datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
constdefs
the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
"the_In1 x \<equiv> \<epsilon>a. x = In1 a"
the_In2 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
"the_In2 x \<equiv> \<epsilon>b. x = In2 b"
the_In3 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
"the_In3 x \<equiv> \<epsilon>c. x = In3 c"
syntax
In1l :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
translations
"In1l e" == "In1 (Inl e)"
"In1r c" == "In1 (Inr c)"
translations
"option"<= (type) "Option.option"
"list" <= (type) "List.list"
"sum3" <= (type) "Basis.sum3"
syntax
fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
translations
"fun_sum" == "sum_case"
syntax
"@Oall" :: [pttrn, 'a option, bool] => bool ("(3! _:_:/ _)" [0,0,10] 10)
"@Oex" :: [pttrn, 'a option, bool] => bool ("(3? _:_:/ _)" [0,0,10] 10)
syntax (symbols)
"@Oall" :: [pttrn, 'a option, bool] => bool ("(3\<forall>_\<in>_:/ _)" [0,0,10] 10)
"@Oex" :: [pttrn, 'a option, bool] => bool ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
translations
"! x:A: P" == "! x:o2s A. P"
"? x:A: P" == "? x:o2s A. P"
constdefs
unique :: "('a × 'b) list \<Rightarrow> bool"
"unique \<equiv> nodups \<circ> map fst"
consts
lsplit :: "[['a, 'a list] => 'b, 'a list] => 'b"
defs
lsplit_def "lsplit == %f l. f (hd l) (tl l)"
(* list patterns -- extends pre-defined type "pttrn" used in abstractions *)
syntax
"_lpttrn" :: [pttrn,pttrn] => pttrn ("_#/_" [901,900] 900)
translations
"%y#x#xs. b" == "lsplit (%y x#xs. b)"
"%x#xs . b" == "lsplit (%x xs . b)"
syntax
"@dummy_pat" :: pttrn ("'_")
end
ML
fun dummy_pat_tr [] = Free ("_",dummyT)
| dummy_pat_tr ts = raise TERM ("dummy_pat_tr", ts);
val parse_translation = ("@dummy_pat", dummy_pat_tr)::parse_translation;
theorem diff_single_insert:
[| A - {x} <= B; x : A |] ==> A <= insert x B
theorem subset_image_iff:
(B <= f `` A) = (EX A'. A' <= A & B = f `` A')
theorem eta_contract_eq:
f = f
theorem eta_contract_rl:
x == x
theorem if_def2:
(if Q then x else y) = ((Q --> x) & (¬ Q --> y))
theorem All_Ex_refl_eq2:
(ALL x. (EX b. x = f b & Q b) --> P x) = (ALL b. Q b --> P (f b))
theorem ex_ex_miniscope1:
(EX w v. P w v & Q v) = (EX v. (EX w. P w v) & Q v)
theorem ex_miniscope2:
(EX v. P v & Q & R v) = (Q & (EX v. P v & R v))
theorem ex_reorder31:
(EX z x y. P x y z) = (EX x y z. P x y z)
theorem Collect_split_eq:
{p. P (split f p)} = {(a, b). P (f a b)}
theorem subset_insertD:
A <= insert x B ==> A <= B & x ~: A | (EX B'. A = insert x B' & B' <= B)
theorem surjective_pairing5:
p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))),
snd (snd (snd (snd p))))
theorem fst_splitE:
[| fst s' = x'; !!x s. [| s' = (x, s); x = x' |] ==> Q |] ==> Q
theorem All_Ex_refl_eq1:
(ALL x. (EX b. x = f b) --> P x) = (ALL b. P (f b))
theorem range_bool_domain:
range f = {f True, f False}
theorem finite_SetCompr2:
[| finite (Collect P); ALL y. P y --> finite (range (f y)) |]
==> finite {f y x |x y. P y}
theorem the_Inl_Inl:
the_Inl (Inl e) = e
theorem the_Inr_Inr:
the_Inr (Inr e) = e
theorem the_In1_In1:
the_In1 (In1 e) = e
theorem the_In2_In2:
the_In2 (In2 e) = e
theorem the_In3_In3:
the_In3 (In3 e) = e
theorem fst_in_set_lemma:
(x, y) : set l ==> x : fst `` set l
theorem uniqueD:
[| unique l; (x, y) : set l; (x', y') : set l; x = x' |] ==> y = y'
theorem unique_Nil:
unique []
theorem unique_Cons:
unique ((x, y) # l) = (unique l & (ALL y. (x, y) ~: set l))
theorem unique_ConsI:
[| unique l; ALL y. (x, y) ~: set l |] ==> unique ((x, y) # l)
theorem unique_single:
unique [p]
theorem unique_ConsD:
unique (x # xs) ==> unique xs
theorem unique_append:
[| unique l'; unique l; ALL (x, y):set l. ALL (x', y'):set l'. x' ~= x |] ==> unique (l @ l')
theorem unique_map_inj:
[| unique l; inj f |] ==> unique (map (%(k, x). (f k, g k x)) l)
theorem map_of_SomeI:
[| unique l; (k, x) : set l |] ==> map_of l k = Some x
theorem lsplit:
lsplit c (x # xs) = c x xs
theorem lsplit2:
lsplit P (x # xs) y z = P x xs y z
theorem lsplit_beta:
lsplit c l = c (hd l) (tl l)