(* Title: HOL/Bali/Basis.thy ID: $Id: Basis.thy,v 1.15 2005/06/17 14:13:06 haftmann Exp $ Author: David von Oheimb *) header {* Definitions extending HOL as logical basis of Bali *} theory Basis imports Main begin ML {* Unify.search_bound := 40; Unify.trace_bound := 40; *} (*print_depth 100;*) (*Syntax.ambiguity_level := 1;*) section "misc" declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *) ML {* fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat] (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm)); *} declare split_if_asm [split] option.split [split] option.split_asm [split] ML {* simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) *} declare if_weak_cong [cong del] option.weak_case_cong [cong del] declare length_Suc_conv [iff]; (*###to be phased out *) ML {* bind_thm ("make_imp", rearrange_prems [1,0] mp) *} lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}" apply auto done lemma subset_insertD: "A <= insert x B ==> A <= B & x ~: A | (EX B'. A = insert x B' & B' <= B)" apply (case_tac "x:A") apply (rule disjI2) apply (rule_tac x = "A-{x}" in exI) apply fast+ done syntax "3" :: nat ("3") "4" :: nat ("4") translations "3" == "Suc 2" "4" == "Suc 3" (*unused*) lemma range_bool_domain: "range f = {f True, f False}" apply auto apply (case_tac "xa") apply auto done (* irrefl_tranclI in Transitive_Closure.thy is more general *) lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+" by(blast elim: tranclE dest: trancl_into_rtrancl) lemma trancl_rtrancl_trancl: "[|(x,y)∈r^+; (y,z)∈r^*|] ==> (x,z)∈r^+" by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2) lemma rtrancl_into_trancl3: "[|(a,b)∈r^*; a≠b|] ==> (a,b)∈r^+" apply (drule rtranclD) apply auto done lemma rtrancl_into_rtrancl2: "[| (a, b) ∈ r; (b, c) ∈ r^* |] ==> (a, c) ∈ r^*" by (auto intro: r_into_rtrancl rtrancl_trans) lemma triangle_lemma: "[| !! a b c. [|(a,b)∈r; (a,c)∈r|] ==> b=c; (a,x)∈r*; (a,y)∈r*|] ==> (x,y)∈r* ∨ (y,x)∈r*" proof - note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1] note converse_rtranclE = converse_rtranclE [consumes 1] assume unique: "!! a b c. [|(a,b)∈r; (a,c)∈r|] ==> b=c" assume "(a,x)∈r*" then show "(a,y)∈r* ==> (x,y)∈r* ∨ (y,x)∈r*" proof (induct rule: converse_rtrancl_induct) assume "(x,y)∈r*" then show ?thesis by blast next fix a v assume a_v_r: "(a, v) ∈ r" and v_x_rt: "(v, x) ∈ r*" and a_y_rt: "(a, y) ∈ r*" and hyp: "(v, y) ∈ r* ==> (x, y) ∈ r* ∨ (y, x) ∈ r*" from a_y_rt show "(x, y) ∈ r* ∨ (y, x) ∈ r*" proof (cases rule: converse_rtranclE) assume "a=y" with a_v_r v_x_rt have "(y,x) ∈ r*" by (auto intro: r_into_rtrancl rtrancl_trans) then show ?thesis by blast next fix w assume a_w_r: "(a, w) ∈ r" and w_y_rt: "(w, y) ∈ r*" from a_v_r a_w_r unique have "v=w" by auto with w_y_rt hyp show ?thesis by blast qed qed qed lemma rtrancl_cases [consumes 1, case_names Refl Trancl]: "[|(a,b)∈r*; a = b ==> P; (a,b)∈r+ ==> P|] ==> P" apply (erule rtranclE) apply (auto dest: rtrancl_into_trancl1) done (* ### To Transitive_Closure *) theorems converse_rtrancl_induct = converse_rtrancl_induct [consumes 1,case_names Id Step] theorems converse_trancl_induct = converse_trancl_induct [consumes 1,case_names Single Step] (* context (theory "Set") *) lemma Ball_weaken:"[|Ball s P;!! x. P x-->Q x|]==>Ball s Q" by auto (* context (theory "Finite") *) lemma finite_SetCompr2: "[| finite (Collect P); !y. P y --> finite (range (f y)) |] ==> finite {f y x |x y. P y}" apply (subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (%y. range (f y))") prefer 2 apply fast apply (erule ssubst) apply (erule finite_UN_I) apply fast done (* ### TO theory "List" *) lemma list_all2_trans: "∀ a b c. P1 a b --> P2 b c --> P3 a c ==> ∀xs2 xs3. list_all2 P1 xs1 xs2 --> list_all2 P2 xs2 xs3 --> list_all2 P3 xs1 xs3" apply (induct_tac "xs1") apply simp apply (rule allI) apply (induct_tac "xs2") apply simp apply (rule allI) apply (induct_tac "xs3") apply auto done section "pairs" lemma surjective_pairing5: "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))), snd (snd (snd (snd p))))" apply auto done lemma fst_splitE [elim!]: "[| fst s' = x'; !!x s. [| s' = (x,s); x = x' |] ==> Q |] ==> Q" apply (cut_tac p = "s'" in surjective_pairing) apply auto done lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l --> x : fst ` set l" apply (induct_tac "l") apply auto done section "quantifiers" (*###to be phased out *) ML {* fun noAll_simpset () = simpset() setmksimps mksimps (List.filter (fn (x,_) => x<>"All") mksimps_pairs) *} lemma All_Ex_refl_eq2 [simp]: "(!x. (? b. x = f b & Q b) --> P x) = (!b. Q b --> P (f b))" apply auto done lemma ex_ex_miniscope1 [simp]: "(EX w v. P w v & Q v) = (EX v. (EX w. P w v) & Q v)" apply auto done lemma ex_miniscope2 [simp]: "(EX v. P v & Q & R v) = (Q & (EX v. P v & R v))" apply auto done lemma ex_reorder31: "(∃z x y. P x y z) = (∃x y z. P x y z)" apply auto done lemma All_Ex_refl_eq1 [simp]: "(!x. (? b. x = f b) --> P x) = (!b. P (f b))" apply auto done section "sums" hide const In0 In1 syntax fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80) translations "fun_sum" == "sum_case" consts the_Inl :: "'a + 'b => 'a" the_Inr :: "'a + 'b => 'b" primrec "the_Inl (Inl a) = a" primrec "the_Inr (Inr b) = b" datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c consts the_In1 :: "('a, 'b, 'c) sum3 => 'a" the_In2 :: "('a, 'b, 'c) sum3 => 'b" the_In3 :: "('a, 'b, 'c) sum3 => 'c" primrec "the_In1 (In1 a) = a" primrec "the_In2 (In2 b) = b" primrec "the_In3 (In3 c) = c" syntax In1l :: "'al => ('al + 'ar, 'b, 'c) sum3" In1r :: "'ar => ('al + 'ar, 'b, 'c) sum3" translations "In1l e" == "In1 (Inl e)" "In1r c" == "In1 (Inr c)" syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 => 'al" the_In1r :: "('al + 'ar, 'b, 'c) sum3 => 'ar" translations "the_In1l" == "the_Inl o the_In1" "the_In1r" == "the_Inr o the_In1" ML {* fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[not_None_eq]) (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"] *} (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) translations "option"<= (type) "Datatype.option" "list" <= (type) "List.list" "sum3" <= (type) "Basis.sum3" section "quantifiers for option type" 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∀_∈_:/ _)" [0,0,10] 10) Oex :: "[pttrn, 'a option, bool] => bool" ("(3∃_∈_:/ _)" [0,0,10] 10) translations "! x:A: P" == "! x:o2s A. P" "? x:A: P" == "? x:o2s A. P" section "unique association lists" constdefs unique :: "('a × 'b) list => bool" "unique ≡ distinct o map fst" lemma uniqueD [rule_format (no_asm)]: "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'--> y=y'))" apply (unfold unique_def o_def) apply (induct_tac "l") apply (auto dest: fst_in_set_lemma) done lemma unique_Nil [simp]: "unique []" apply (unfold unique_def) apply (simp (no_asm)) done lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))" apply (unfold unique_def) apply (auto dest: fst_in_set_lemma) done lemmas unique_ConsI = conjI [THEN unique_Cons [THEN iffD2], standard] lemma unique_single [simp]: "!!p. unique [p]" apply auto done lemma unique_ConsD: "unique (x#xs) ==> unique xs" apply (simp add: unique_def) done lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l --> (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')" apply (induct_tac "l") apply (auto dest: fst_in_set_lemma) done lemma unique_map_inj [rule_format (no_asm)]: "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)" apply (induct_tac "l") apply (auto dest: fst_in_set_lemma simp add: inj_eq) done lemma map_of_SomeI [rule_format (no_asm)]: "unique l --> (k, x) : set l --> map_of l k = Some x" apply (induct_tac "l") apply auto done section "list patterns" 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)" lemma lsplit [simp]: "lsplit c (x#xs) = c x xs" apply (unfold lsplit_def) apply (simp (no_asm)) done lemma lsplit2 [simp]: "lsplit P (x#xs) y z = P x xs y z" apply (unfold lsplit_def) apply simp done section "dummy pattern for quantifiers, let, etc." syntax "@dummy_pat" :: pttrn ("'_") parse_translation {* let fun dummy_pat_tr [] = Free ("_",dummyT) | dummy_pat_tr ts = raise TERM ("dummy_pat_tr", ts); in [("@dummy_pat", dummy_pat_tr)] end *} end
theorem make_imp:
[| P; P --> Q |] ==> Q
lemma Collect_split_eq:
{p. P (split f p)} = {(a, b). P (f a b)}
lemma subset_insertD:
A ⊆ insert x B ==> A ⊆ B ∧ x ∉ A ∨ (∃B'. A = insert x B' ∧ B' ⊆ B)
lemma range_bool_domain:
range f = {f True, f False}
lemma irrefl_tranclI':
r^-1 ∩ r+ = {} ==> ∀x. (x, x) ∉ r+
lemma trancl_rtrancl_trancl:
[| (x, y) ∈ r+; (y, z) ∈ r* |] ==> (x, z) ∈ r+
lemma rtrancl_into_trancl3:
[| (a, b) ∈ r*; a ≠ b |] ==> (a, b) ∈ r+
lemma rtrancl_into_rtrancl2:
[| (a, b) ∈ r; (b, c) ∈ r* |] ==> (a, c) ∈ r*
lemma triangle_lemma:
[| !!a b c. [| (a, b) ∈ r; (a, c) ∈ r |] ==> b = c; (a, x) ∈ r*; (a, y) ∈ r* |] ==> (x, y) ∈ r* ∨ (y, x) ∈ r*
lemma rtrancl_cases:
[| (a, b) ∈ r*; a = b ==> P; (a, b) ∈ r+ ==> P |] ==> P
theorems converse_rtrancl_induct:
[| (a, b) ∈ r*; P b; !!y z. [| (y, z) ∈ r; (z, b) ∈ r*; P z |] ==> P y |] ==> P a
theorems converse_rtrancl_induct:
[| (a, b) ∈ r*; P b; !!y z. [| (y, z) ∈ r; (z, b) ∈ r*; P z |] ==> P y |] ==> P a
theorems converse_trancl_induct:
[| (a, b) ∈ r+; !!y. (y, b) ∈ r ==> P y; !!y z. [| (y, z) ∈ r; (z, b) ∈ r+; P z |] ==> P y |] ==> P a
theorems converse_trancl_induct:
[| (a, b) ∈ r+; !!y. (y, b) ∈ r ==> P y; !!y z. [| (y, z) ∈ r; (z, b) ∈ r+; P z |] ==> P y |] ==> P a
lemma Ball_weaken:
[| Ball s P; !!x. P x --> Q x |] ==> Ball s Q
lemma finite_SetCompr2:
[| finite (Collect P); ∀y. P y --> finite (range (f y)) |] ==> finite {f y x |x y. P y}
lemma list_all2_trans:
∀a b c. P1.0 a b --> P2.0 b c --> P3.0 a c ==> ∀xs2 xs3. list_all2 P1.0 xs1.0 xs2 --> list_all2 P2.0 xs2 xs3 --> list_all2 P3.0 xs1.0 xs3
lemma surjective_pairing5:
p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))), snd (snd (snd (snd p))))
lemma fst_splitE:
[| fst s' = x'; !!x s. [| s' = (x, s); x = x' |] ==> Q |] ==> Q
lemma fst_in_set_lemma:
(x, y) ∈ set l ==> x ∈ fst ` set l
lemma All_Ex_refl_eq2:
(∀x. (∃b. x = f b ∧ Q b) --> P x) = (∀b. Q b --> P (f b))
lemma ex_ex_miniscope1:
(∃w v. P w v ∧ Q v) = (∃v. (∃w. P w v) ∧ Q v)
lemma ex_miniscope2:
(∃v. P v ∧ Q ∧ R v) = (Q ∧ (∃v. P v ∧ R v))
lemma ex_reorder31:
(∃z x y. P x y z) = (∃x y z. P x y z)
lemma All_Ex_refl_eq1:
(∀x. (∃b. x = f b) --> P x) = (∀b. P (f b))
lemma uniqueD:
[| unique l; (x, y) ∈ set l; (x', y') ∈ set l; x = x' |] ==> y = y'
lemma unique_Nil:
unique []
lemma unique_Cons:
unique ((x, y) # l) = (unique l ∧ (∀y. (x, y) ∉ set l))
lemmas unique_ConsI:
[| unique l; ∀y. (x, y) ∉ set l |] ==> unique ((x, y) # l)
lemmas unique_ConsI:
[| unique l; ∀y. (x, y) ∉ set l |] ==> unique ((x, y) # l)
lemma unique_single:
unique [p]
lemma unique_ConsD:
unique (x # xs) ==> unique xs
lemma unique_append:
[| unique l'; unique l; ∀(x, y)∈set l. ∀(x', y')∈set l'. x' ≠ x |] ==> unique (l @ l')
lemma unique_map_inj:
[| unique l; inj f |] ==> unique (map (%(k, x). (f k, g k x)) l)
lemma map_of_SomeI:
[| unique l; (k, x) ∈ set l |] ==> map_of l k = Some x
lemma lsplit:
lsplit c (x # xs) = c x xs
lemma lsplit2:
lsplit P (x # xs) y z = P x xs y z