# HG changeset patch # User wenzelm # Date 1318704013 -7200 # Node ID 2dd44cd8f9633342e4097ffff9a7d048133c1ca2 # Parent cf6a5de94bfcf5879cfb4d61e9058014e0f81068 misc tuning and modernization; diff -r cf6a5de94bfc -r 2dd44cd8f963 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Sat Oct 15 18:14:36 2011 +0200 +++ b/src/HOL/Bali/Basis.thy Sat Oct 15 20:40:13 2011 +0200 @@ -3,8 +3,9 @@ *) header {* Definitions extending HOL as logical basis of Bali *} -theory Basis imports Main "~~/src/HOL/Library/Old_Recdef" begin - +theory Basis +imports Main "~~/src/HOL/Library/Old_Recdef" +begin section "misc" @@ -14,162 +15,130 @@ declare length_Suc_conv [iff] lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}" -apply auto -done + by auto -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 +lemma subset_insertD: "A \ insert x B \ A \ B \ x \ A \ (\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 -abbreviation nat3 :: nat ("3") where "3 == Suc 2" -abbreviation nat4 :: nat ("4") where "4 == Suc 3" - -(*unused*) -lemma range_bool_domain: "range f = {f True, f False}" -apply auto -apply (case_tac "xa") -apply auto -done +abbreviation nat3 :: nat ("3") where "3 \ Suc 2" +abbreviation nat4 :: nat ("4") where "4 \ Suc 3" (* 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 irrefl_tranclI': "r\ \ r\<^sup>+ = {} \ \x. (x, x) \ r\<^sup>+" + 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 trancl_rtrancl_trancl: "\(x, y) \ r\<^sup>+; (y, z) \ r\<^sup>*\ \ (x, z) \ r\<^sup>+" + 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_trancl3: "\(a, b) \ r\<^sup>*; a \ b\ \ (a, b) \ r\<^sup>+" + 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 rtrancl_into_rtrancl2: "\(a, b) \ r; (b, c) \ r\<^sup>*\ \ (a, c) \ r\<^sup>*" + by (auto intro: rtrancl_trans) lemma triangle_lemma: - "\ \ a b c. \(a,b)\r; (a,c)\r\ \ b=c; (a,x)\r\<^sup>*; (a,y)\r\<^sup>*\ - \ (x,y)\r\<^sup>* \ (y,x)\r\<^sup>*" -proof - - assume unique: "\ a b c. \(a,b)\r; (a,c)\r\ \ b=c" - assume "(a,x)\r\<^sup>*" - then show "(a,y)\r\<^sup>* \ (x,y)\r\<^sup>* \ (y,x)\r\<^sup>*" - proof (induct rule: converse_rtrancl_induct) - assume "(x,y)\r\<^sup>*" - then show ?thesis - by blast + assumes unique: "\a b c. \(a,b)\r; (a,c)\r\ \ b = c" + and ax: "(a,x)\r\<^sup>*" and ay: "(a,y)\r\<^sup>*" + shows "(x,y)\r\<^sup>* \ (y,x)\r\<^sup>*" + using ax ay +proof (induct rule: converse_rtrancl_induct) + assume "(x,y)\r\<^sup>*" + then show ?thesis by blast +next + fix a v + assume a_v_r: "(a, v) \ r" + and v_x_rt: "(v, x) \ r\<^sup>*" + and a_y_rt: "(a, y) \ r\<^sup>*" + and hyp: "(v, y) \ r\<^sup>* \ (x, y) \ r\<^sup>* \ (y, x) \ r\<^sup>*" + from a_y_rt show "(x, y) \ r\<^sup>* \ (y, x) \ r\<^sup>*" + proof (cases rule: converse_rtranclE) + assume "a = y" + with a_v_r v_x_rt have "(y,x) \ r\<^sup>*" + by (auto intro: rtrancl_trans) + then show ?thesis by blast next - fix a v - assume a_v_r: "(a, v) \ r" and - v_x_rt: "(v, x) \ r\<^sup>*" and - a_y_rt: "(a, y) \ r\<^sup>*" and - hyp: "(v, y) \ r\<^sup>* \ (x, y) \ r\<^sup>* \ (y, x) \ r\<^sup>*" - from a_y_rt - show "(x, y) \ r\<^sup>* \ (y, x) \ r\<^sup>*" - proof (cases rule: converse_rtranclE) - assume "a=y" - with a_v_r v_x_rt have "(y,x) \ r\<^sup>*" - 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\<^sup>*" - from a_v_r a_w_r unique - have "v=w" - by auto - with w_y_rt hyp - show ?thesis - by blast - qed + fix w + assume a_w_r: "(a, w) \ r" + and w_y_rt: "(w, y) \ r\<^sup>*" + from a_v_r a_w_r unique have "v=w" by auto + with w_y_rt hyp show ?thesis by blast qed qed -lemma rtrancl_cases [consumes 1, case_names Refl Trancl]: - "\(a,b)\r\<^sup>*; a = b \ P; (a,b)\r\<^sup>+ \ P\ \ P" -apply (erule rtranclE) -apply (auto dest: rtrancl_into_trancl1) -done +lemma rtrancl_cases: + assumes "(a,b)\r\<^sup>*" + obtains (Refl) "a = b" + | (Trancl) "(a,b)\r\<^sup>+" + apply (rule rtranclE [OF assms]) + apply (auto dest: rtrancl_into_trancl1) + done -(* context (theory "Set") *) -lemma Ball_weaken:"\Ball s P;\ x. P x\Q x\\Ball s Q" -by auto +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 - +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 +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 surjective_pairing5: + "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))), + snd (snd (snd (snd p))))" + by auto -lemma fst_splitE [elim!]: -"[| fst s' = x'; !!x s. [| s' = (x,s); x = x' |] ==> Q |] ==> Q" -by (cases s') auto +lemma fst_splitE [elim!]: + assumes "fst s' = x'" + obtains x s where "s' = (x,s)" and "x = x'" + using assms by (cases s') auto -lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l --> x : fst ` set l" -apply (induct_tac "l") -apply auto -done +lemma fst_in_set_lemma: "(x, y) : set l \ x : fst ` set l" + by (induct l) auto section "quantifiers" -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 All_Ex_refl_eq2 [simp]: "(\x. (\b. x = f b \ Q b) \ P x) = (\b. Q b \ P (f b))" + by auto -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_ex_miniscope1 [simp]: "(\w v. P w v \ Q v) = (\v. (\w. P w v) \ Q v)" + by auto -lemma ex_miniscope2 [simp]: - "(EX v. P v & Q & R v) = (Q & (EX v. P v & R v))" -apply auto -done +lemma ex_miniscope2 [simp]: "(\v. P v \ Q \ R v) = (Q \ (\v. P v \ R v))" + by auto lemma ex_reorder31: "(\z x y. P x y z) = (\x y z. P x y z)" -apply auto -done + by auto -lemma All_Ex_refl_eq1 [simp]: "(!x. (? b. x = f b) --> P x) = (!b. P (f b))" -apply auto -done +lemma All_Ex_refl_eq1 [simp]: "(\x. (\b. x = f b) \ P x) = (\b. P (f b))" + by auto section "sums" @@ -178,38 +147,38 @@ notation sum_case (infixr "'(+')"80) -primrec the_Inl :: "'a + 'b \ 'a" +primrec the_Inl :: "'a + 'b \ 'a" where "the_Inl (Inl a) = a" -primrec the_Inr :: "'a + 'b \ 'b" +primrec the_Inr :: "'a + 'b \ 'b" where "the_Inr (Inr b) = b" datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c -primrec the_In1 :: "('a, 'b, 'c) sum3 \ 'a" +primrec the_In1 :: "('a, 'b, 'c) sum3 \ 'a" where "the_In1 (In1 a) = a" -primrec the_In2 :: "('a, 'b, 'c) sum3 \ 'b" +primrec the_In2 :: "('a, 'b, 'c) sum3 \ 'b" where "the_In2 (In2 b) = b" -primrec the_In3 :: "('a, 'b, 'c) sum3 \ 'c" +primrec the_In3 :: "('a, 'b, 'c) sum3 \ 'c" where "the_In3 (In3 c) = c" -abbreviation In1l :: "'al \ ('al + 'ar, 'b, 'c) sum3" - where "In1l e == In1 (Inl e)" +abbreviation In1l :: "'al \ ('al + 'ar, 'b, 'c) sum3" + where "In1l e \ In1 (Inl e)" -abbreviation In1r :: "'ar \ ('al + 'ar, 'b, 'c) sum3" - where "In1r c == In1 (Inr c)" +abbreviation In1r :: "'ar \ ('al + 'ar, 'b, 'c) sum3" + where "In1r c \ In1 (Inr c)" abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \ 'al" - where "the_In1l == the_Inl \ the_In1" + where "the_In1l \ the_Inl \ the_In1" abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \ 'ar" - where "the_In1r == the_Inr \ the_In1" + where "the_In1r \ the_Inr \ the_In1" ML {* fun sum3_instantiate ctxt thm = map (fn s => - simplify (simpset_of ctxt delsimps[@{thm not_None_eq}]) + simplify (simpset_of ctxt delsimps [@{thm not_None_eq}]) (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"] *} (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) @@ -218,107 +187,83 @@ 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) + "_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) + "_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:CONST Option.set A. P" - "? x:A: P" == "? x:CONST Option.set A. P" + "\x\A: P" \ "\x\CONST Option.set A. P" + "\x\A: P" \ "\x\CONST Option.set A. P" + section "Special map update" text{* Deemed too special for theory Map. *} -definition - chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)" - where "chg_map f a m = (case m a of None => m | Some b => m(a|->f b))" +definition chg_map :: "('b \ 'b) \ 'a \ ('a \ 'b) \ ('a \ 'b)" + where "chg_map f a m = (case m a of None \ m | Some b \ m(a\f b))" -lemma chg_map_new[simp]: "m a = None ==> chg_map f a m = m" -by (unfold chg_map_def, auto) +lemma chg_map_new[simp]: "m a = None \ chg_map f a m = m" + unfolding chg_map_def by auto -lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)" -by (unfold chg_map_def, auto) +lemma chg_map_upd[simp]: "m a = Some b \ chg_map f a m = m(a\f b)" + unfolding chg_map_def by auto lemma chg_map_other [simp]: "a \ b \ chg_map f a m b = m b" -by (auto simp: chg_map_def split add: option.split) + by (auto simp: chg_map_def) section "unique association lists" -definition - unique :: "('a \ 'b) list \ bool" +definition unique :: "('a \ 'b) list \ bool" where "unique = distinct \ 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 uniqueD: "unique l \ (x, y) \ set l \ (x', y') \ set l \ x = x' \ y = y'" + unfolding unique_def o_def + by (induct l) (auto dest: fst_in_set_lemma) lemma unique_Nil [simp]: "unique []" -apply (unfold unique_def) -apply (simp (no_asm)) -done + by (simp add: unique_def) -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 +lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l \ (\y. (x,y) \ set l))" + by (auto simp: unique_def dest: fst_in_set_lemma) -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" + by (simp add: unique_def) -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_single [simp]: "\p. unique [p]" + by simp -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 unique_append [rule_format (no_asm)]: "unique l' \ unique l \ + (\(x,y)\set l. \(x',y')\set l'. x' \ x) \ unique (l @ l')" + by (induct l) (auto dest: fst_in_set_lemma) -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 +lemma unique_map_inj: "unique l \ inj f \ unique (map (\(k,x). (f k, g k x)) l)" + by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq) + +lemma map_of_SomeI: "unique l \ (k, x) : set l \ map_of l k = Some x" + by (induct l) auto section "list patterns" -definition - lsplit :: "[['a, 'a list] => 'b, 'a list] => 'b" where - "lsplit = (\f l. f (hd l) (tl l))" +definition lsplit :: "[['a, 'a list] \ 'b, 'a list] \ 'b" + where "lsplit = (\f l. f (hd l) (tl l))" text {* list patterns -- extends pre-defined type "pttrn" used in abstractions *} syntax - "_lpttrn" :: "[pttrn,pttrn] => pttrn" ("_#/_" [901,900] 900) + "_lpttrn" :: "[pttrn, pttrn] \ pttrn" ("_#/_" [901,900] 900) translations - "%y#x#xs. b" == "CONST lsplit (%y x#xs. b)" - "%x#xs . b" == "CONST lsplit (%x xs . b)" + "\y # x # xs. b" \ "CONST lsplit (\y x # xs. b)" + "\x # xs. b" \ "CONST lsplit (\x xs. b)" lemma lsplit [simp]: "lsplit c (x#xs) = c x xs" -apply (unfold lsplit_def) -apply (simp (no_asm)) -done + by (simp add: lsplit_def) lemma lsplit2 [simp]: "lsplit P (x#xs) y z = P x xs y z" -apply (unfold lsplit_def) -apply simp -done - + by (simp add: lsplit_def) end