# HG changeset patch # User haftmann # Date 1267540755 -3600 # Node ID 5d88ffdb290c0d5ae3b9498950ba51c99c7683ce # Parent 6acef0aea07d72a6ab8b1f8854cd3add22842c40# Parent 118cda1736275727151e787d52592757819e09b1 merged diff -r 118cda173627 -r 5d88ffdb290c src/HOL/Bali/Decl.thy --- a/src/HOL/Bali/Decl.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/Bali/Decl.thy Tue Mar 02 15:39:15 2010 +0100 @@ -763,51 +763,57 @@ section "general recursion operators for the interface and class hiearchies" -consts - iface_rec :: "prog \ qtname \ \ (qtname \ iface \ 'a set \ 'a) \ 'a" - class_rec :: "prog \ qtname \ 'a \ (qtname \ class \ 'a \ 'a) \ 'a" - -recdef iface_rec "same_fst ws_prog (\G. (subint1 G)^-1)" -"iface_rec (G,I) = - (\f. case iface G I of +function + iface_rec :: "prog \ qtname \ \(qtname \ iface \ 'a set \ 'a) \ 'a" +where +[simp del]: "iface_rec G I f = + (case iface G I of None \ undefined | Some i \ if ws_prog G then f I i - ((\J. iface_rec (G,J) f)`set (isuperIfs i)) + ((\J. iface_rec G J f)`set (isuperIfs i)) else undefined)" -(hints recdef_wf: wf_subint1 intro: subint1I) -declare iface_rec.simps [simp del] +by auto +termination +by (relation "inv_image (same_fst ws_prog (\G. (subint1 G)^-1)) (%(x,y,z). (x,y))") + (auto simp: wf_subint1 subint1I wf_same_fst) lemma iface_rec: "\iface G I = Some i; ws_prog G\ \ - iface_rec (G,I) f = f I i ((\J. iface_rec (G,J) f)`set (isuperIfs i))" + iface_rec G I f = f I i ((\J. iface_rec G J f)`set (isuperIfs i))" apply (subst iface_rec.simps) apply simp done -recdef class_rec "same_fst ws_prog (\G. (subcls1 G)^-1)" -"class_rec(G,C) = - (\t f. case class G C of + +function + class_rec :: "prog \ qtname \ 'a \ (qtname \ class \ 'a \ 'a) \ 'a" +where +[simp del]: "class_rec G C t f = + (case class G C of None \ undefined | Some c \ if ws_prog G then f C c (if C = Object then t - else class_rec (G,super c) t f) + else class_rec G (super c) t f) else undefined)" -(hints recdef_wf: wf_subcls1 intro: subcls1I) -declare class_rec.simps [simp del] + +by auto +termination +by (relation "inv_image (same_fst ws_prog (\G. (subcls1 G)^-1)) (%(x,y,z,w). (x,y))") + (auto simp: wf_subcls1 subcls1I wf_same_fst) lemma class_rec: "\class G C = Some c; ws_prog G\ \ - class_rec (G,C) t f = - f C c (if C = Object then t else class_rec (G,super c) t f)" -apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]]) + class_rec G C t f = + f C c (if C = Object then t else class_rec G (super c) t f)" +apply (subst class_rec.simps) apply simp done definition imethds :: "prog \ qtname \ (sig,qtname \ mhead) tables" where --{* methods of an interface, with overriding and inheritance, cf. 9.2 *} "imethds G I - \ iface_rec (G,I) + \ iface_rec G I (\I i ts. (Un_tables ts) \\ (Option.set \ table_of (map (\(s,m). (s,I,m)) (imethods i))))" diff -r 118cda173627 -r 5d88ffdb290c src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/Bali/DeclConcepts.thy Tue Mar 02 15:39:15 2010 +0100 @@ -1381,7 +1381,7 @@ definition imethds :: "prog \ qtname \ (sig,qtname \ mhead) tables" where "imethds G I - \ iface_rec (G,I) + \ iface_rec G I (\I i ts. (Un_tables ts) \\ (Option.set \ table_of (map (\(s,m). (s,I,m)) (imethods i))))" text {* methods of an interface, with overriding and inheritance, cf. 9.2 *} @@ -1396,7 +1396,7 @@ definition methd :: "prog \ qtname \ (sig,qtname \ methd) table" where "methd G C - \ class_rec (G,C) empty + \ class_rec G C empty (\C c subcls_mthds. filter_tab (\sig m. G\C inherits method sig m) subcls_mthds @@ -1429,7 +1429,7 @@ then (case methd G statC sig of None \ None | Some statM - \ (class_rec (G,dynC) empty + \ (class_rec G dynC empty (\C c subcls_mthds. subcls_mthds ++ @@ -1481,7 +1481,7 @@ definition fields :: "prog \ qtname \ ((vname \ qtname) \ field) list" where "fields G C - \ class_rec (G,C) [] (\C c ts. map (\(n,t). ((n,C),t)) (cfields c) @ ts)" + \ class_rec G C [] (\C c ts. map (\(n,t). ((n,C),t)) (cfields c) @ ts)" text {* @{term "fields G C"} list of fields of a class, including all the fields of the superclasses (private, inherited and hidden ones) not only the accessible ones @@ -1805,7 +1805,7 @@ (\_ dynM. G,sig \ dynM overrides statM \ dynM = statM) (methd G C)" let "?class_rec C" = - "(class_rec (G, C) empty + "(class_rec G C empty (\C c subcls_mthds. subcls_mthds ++ (?filter C)))" from statM Subcls ws subclseq_dynC_statC have dynmethd_dynC_def: @@ -2270,7 +2270,7 @@ section "calculation of the superclasses of a class" definition superclasses :: "prog \ qtname \ qtname set" where - "superclasses G C \ class_rec (G,C) {} + "superclasses G C \ class_rec G C {} (\ C c superclss. (if C=Object then {} else insert (super c) superclss))" diff -r 118cda173627 -r 5d88ffdb290c src/HOL/Bali/WellForm.thy --- a/src/HOL/Bali/WellForm.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/Bali/WellForm.thy Tue Mar 02 15:39:15 2010 +0100 @@ -730,13 +730,15 @@ \ \is_static im \ accmodi im = Public" proof - assume asm: "wf_prog G" "is_iface G I" "im \ imethds G I sig" + + note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard] have "wf_prog G \ (\ i im. iface G I = Some i \ im \ imethds G I sig \ \is_static im \ accmodi im = Public)" (is "?P G I") - proof (rule iface_rec.induct,intro allI impI) + proof (induct G I rule: iface_rec_induct', intro allI impI) fix G I i im - assume hyp: "\ J i. J \ set (isuperIfs i) \ ws_prog G \ iface G I = Some i - \ ?P G J" + assume hyp: "\ i J. iface G I = Some i \ ws_prog G \ J \ set (isuperIfs i) + \ ?P G J" assume wf: "wf_prog G" and if_I: "iface G I = Some i" and im: "im \ imethds G I sig" show "\is_static im \ accmodi im = Public" @@ -1345,14 +1347,16 @@ qed qed +lemmas class_rec_induct' = class_rec.induct[of "%x y z w. P x y", standard] + lemma declclass_widen[rule_format]: "wf_prog G \ (\c m. class G C = Some c \ methd G C sig = Some m \ G\C \\<^sub>C declclass m)" (is "?P G C") -proof (rule class_rec.induct,intro allI impI) +proof (induct G C rule: class_rec_induct', intro allI impI) fix G C c m - assume Hyp: "\c. C \ Object \ ws_prog G \ class G C = Some c - \ ?P G (super c)" + assume Hyp: "\c. class G C = Some c \ ws_prog G \ C \ Object + \ ?P G (super c)" assume wf: "wf_prog G" and cls_C: "class G C = Some c" and m: "methd G C sig = Some m" show "G\C\\<^sub>C declclass m" @@ -1976,27 +1980,6 @@ qed qed -(* Tactical version *) -(* -lemma declclassD[rule_format]: - "wf_prog G \ - (\ c d m. class G C = Some c \ methd G C sig = Some m \ - class G (declclass m) = Some d - \ table_of (methods d) sig = Some (mthd m))" -apply (rule class_rec.induct) -apply (rule impI) -apply (rule allI)+ -apply (rule impI) -apply (case_tac "C=Object") -apply (force simp add: methd_rec) - -apply (subst methd_rec) -apply (blast dest: wf_ws_prog)+ -apply (case_tac "table_of (map (\(s, m). (s, C, m)) (methods c)) sig") -apply (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) -done -*) - lemma dynmethd_Object: assumes statM: "methd G Object sig = Some statM" and private: "accmodi statM = Private" and @@ -2355,9 +2338,9 @@ have "wf_prog G \ (\ c m. class G C = Some c \ methd G C sig = Some m \ methd G (declclass m) sig = Some m)" (is "?P G C") - proof (rule class_rec.induct,intro allI impI) + proof (induct G C rule: class_rec_induct', intro allI impI) fix G C c m - assume hyp: "\c. C \ Object \ ws_prog G \ class G C = Some c \ + assume hyp: "\c. class G C = Some c \ ws_prog G \ C \ Object \ ?P G (super c)" assume wf: "wf_prog G" and cls_C: "class G C = Some c" and m: "methd G C sig = Some m" diff -r 118cda173627 -r 5d88ffdb290c src/HOL/Induct/Tree.thy --- a/src/HOL/Induct/Tree.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/Induct/Tree.thy Tue Mar 02 15:39:15 2010 +0100 @@ -68,7 +68,7 @@ subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*} -text{*To define recdef style functions we need an ordering on the Brouwer +text{*To use the function package we need an ordering on the Brouwer ordinals. Start with a predecessor relation and form its transitive closure. *} diff -r 118cda173627 -r 5d88ffdb290c src/HOL/Lambda/ParRed.thy --- a/src/HOL/Lambda/ParRed.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/Lambda/ParRed.thy Tue Mar 02 15:39:15 2010 +0100 @@ -85,14 +85,14 @@ subsection {* Complete developments *} -consts +fun "cd" :: "dB => dB" -recdef "cd" "measure size" +where "cd (Var n) = Var n" - "cd (Var n \ t) = Var n \ cd t" - "cd ((s1 \ s2) \ t) = cd (s1 \ s2) \ cd t" - "cd (Abs u \ t) = (cd u)[cd t/0]" - "cd (Abs s) = Abs (cd s)" +| "cd (Var n \ t) = Var n \ cd t" +| "cd ((s1 \ s2) \ t) = cd (s1 \ s2) \ cd t" +| "cd (Abs u \ t) = (cd u)[cd t/0]" +| "cd (Abs s) = Abs (cd s)" lemma par_beta_cd: "s => t \ t => cd s" apply (induct s arbitrary: t rule: cd.induct) diff -r 118cda173627 -r 5d88ffdb290c src/HOL/Library/Word.thy --- a/src/HOL/Library/Word.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/Library/Word.thy Tue Mar 02 15:39:15 2010 +0100 @@ -311,11 +311,11 @@ lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w" by (rule bit_list_induct [of _ w],simp_all) -consts +fun nat_to_bv_helper :: "nat => bit list => bit list" -recdef nat_to_bv_helper "measure (\n. n)" - "nat_to_bv_helper n = (%bs. (if n = 0 then bs - else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \ else \)#bs)))" +where + "nat_to_bv_helper n bs = (if n = 0 then bs + else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \ else \)#bs))" definition nat_to_bv :: "nat => bit list" where diff -r 118cda173627 -r 5d88ffdb290c src/HOL/MicroJava/BV/Effect.thy --- a/src/HOL/MicroJava/BV/Effect.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/MicroJava/BV/Effect.thy Tue Mar 02 15:39:15 2010 +0100 @@ -34,33 +34,34 @@ | "succs Throw pc = [pc]" text "Effect of instruction on the state type:" -consts -eff' :: "instr \ jvm_prog \ state_type \ state_type" -recdef eff' "{}" -"eff' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)" -"eff' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])" -"eff' (LitPush v, G, (ST, LT)) = (the (typeof (\v. None) v) # ST, LT)" -"eff' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)" -"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)" -"eff' (New C, G, (ST,LT)) = (Class C # ST, LT)" -"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)" -"eff' (Pop, G, (ts#ST,LT)) = (ST,LT)" -"eff' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)" -"eff' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)" -"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)" -"eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)" +fun eff' :: "instr \ jvm_prog \ state_type \ state_type" +where +"eff' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)" | +"eff' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])" | +"eff' (LitPush v, G, (ST, LT)) = (the (typeof (\v. None) v) # ST, LT)" | +"eff' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)" | +"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)" | +"eff' (New C, G, (ST,LT)) = (Class C # ST, LT)" | +"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)" | +"eff' (Pop, G, (ts#ST,LT)) = (ST,LT)" | +"eff' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)" | +"eff' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)" | +"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)" | +"eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)" | "eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) - = (PrimT Integer#ST,LT)" -"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)" -"eff' (Goto b, G, s) = s" + = (PrimT Integer#ST,LT)" | +"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)" | +"eff' (Goto b, G, s) = s" | -- "Return has no successor instruction in the same method" -"eff' (Return, G, s) = s" +"eff' (Return, G, s) = s" | -- "Throw always terminates abruptly" -"eff' (Throw, G, s) = s" +"eff' (Throw, G, s) = s" | "eff' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" + + primrec match_any :: "jvm_prog \ p_count \ exception_table \ cname list" where "match_any G pc [] = []" | "match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e; @@ -77,16 +78,16 @@ "match G X pc et = (if \e \ set et. match_exception_entry G (Xcpt X) pc e then [Xcpt X] else [])" by (induct et) auto -consts +fun xcpt_names :: "instr \ jvm_prog \ p_count \ exception_table \ cname list" -recdef xcpt_names "{}" +where "xcpt_names (Getfield F C, G, pc, et) = match G NullPointer pc et" - "xcpt_names (Putfield F C, G, pc, et) = match G NullPointer pc et" - "xcpt_names (New C, G, pc, et) = match G OutOfMemory pc et" - "xcpt_names (Checkcast C, G, pc, et) = match G ClassCast pc et" - "xcpt_names (Throw, G, pc, et) = match_any G pc et" - "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" - "xcpt_names (i, G, pc, et) = []" +| "xcpt_names (Putfield F C, G, pc, et) = match G NullPointer pc et" +| "xcpt_names (New C, G, pc, et) = match G OutOfMemory pc et" +| "xcpt_names (Checkcast C, G, pc, et) = match G ClassCast pc et" +| "xcpt_names (Throw, G, pc, et) = match_any G pc et" +| "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" +| "xcpt_names (i, G, pc, et) = []" definition xcpt_eff :: "instr \ jvm_prog \ p_count \ state_type option \ exception_table \ succ_type" where @@ -118,53 +119,53 @@ text "Conditions under which eff is applicable:" -consts + +fun app' :: "instr \ jvm_prog \ p_count \ nat \ ty \ state_type \ bool" - -recdef app' "{}" +where "app' (Load idx, G, pc, maxs, rT, s) = - (idx < length (snd s) \ (snd s) ! idx \ Err \ length (fst s) < maxs)" + (idx < length (snd s) \ (snd s) ! idx \ Err \ length (fst s) < maxs)" | "app' (Store idx, G, pc, maxs, rT, (ts#ST, LT)) = - (idx < length LT)" + (idx < length LT)" | "app' (LitPush v, G, pc, maxs, rT, s) = - (length (fst s) < maxs \ typeof (\t. None) v \ None)" + (length (fst s) < maxs \ typeof (\t. None) v \ None)" | "app' (Getfield F C, G, pc, maxs, rT, (oT#ST, LT)) = (is_class G C \ field (G,C) F \ None \ fst (the (field (G,C) F)) = C \ - G \ oT \ (Class C))" + G \ oT \ (Class C))" | "app' (Putfield F C, G, pc, maxs, rT, (vT#oT#ST, LT)) = (is_class G C \ field (G,C) F \ None \ fst (the (field (G,C) F)) = C \ - G \ oT \ (Class C) \ G \ vT \ (snd (the (field (G,C) F))))" + G \ oT \ (Class C) \ G \ vT \ (snd (the (field (G,C) F))))" | "app' (New C, G, pc, maxs, rT, s) = - (is_class G C \ length (fst s) < maxs)" + (is_class G C \ length (fst s) < maxs)" | "app' (Checkcast C, G, pc, maxs, rT, (RefT rt#ST,LT)) = - (is_class G C)" + (is_class G C)" | "app' (Pop, G, pc, maxs, rT, (ts#ST,LT)) = - True" + True" | "app' (Dup, G, pc, maxs, rT, (ts#ST,LT)) = - (1+length ST < maxs)" + (1+length ST < maxs)" | "app' (Dup_x1, G, pc, maxs, rT, (ts1#ts2#ST,LT)) = - (2+length ST < maxs)" + (2+length ST < maxs)" | "app' (Dup_x2, G, pc, maxs, rT, (ts1#ts2#ts3#ST,LT)) = - (3+length ST < maxs)" + (3+length ST < maxs)" | "app' (Swap, G, pc, maxs, rT, (ts1#ts2#ST,LT)) = - True" + True" | "app' (IAdd, G, pc, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT)) = - True" + True" | "app' (Ifcmpeq b, G, pc, maxs, rT, (ts#ts'#ST,LT)) = - (0 \ int pc + b \ (isPrimT ts \ ts' = ts \ isRefT ts \ isRefT ts'))" + (0 \ int pc + b \ (isPrimT ts \ ts' = ts \ isRefT ts \ isRefT ts'))" | "app' (Goto b, G, pc, maxs, rT, s) = - (0 \ int pc + b)" + (0 \ int pc + b)" | "app' (Return, G, pc, maxs, rT, (T#ST,LT)) = - (G \ T \ rT)" + (G \ T \ rT)" | "app' (Throw, G, pc, maxs, rT, (T#ST,LT)) = - isRefT T" + isRefT T" | "app' (Invoke C mn fpTs, G, pc, maxs, rT, s) = (length fpTs < length (fst s) \ (let apTs = rev (take (length fpTs) (fst s)); X = hd (drop (length fpTs) (fst s)) in G \ X \ Class C \ is_class G C \ method (G,C) (mn,fpTs) \ None \ - list_all2 (\x y. G \ x \ y) apTs fpTs))" + list_all2 (\x y. G \ x \ y) apTs fpTs))" | "app' (i,G, pc,maxs,rT,s) = False" @@ -208,7 +209,7 @@ qed auto lemma 2: "\(2 < length a) \ a = [] \ (\ l. a = [l]) \ (\ l l'. a = [l,l'])" -proof -; +proof - assume "\(2 < length a)" hence "length a < (Suc (Suc (Suc 0)))" by simp hence * : "length a = 0 \ length a = Suc 0 \ length a = Suc (Suc 0)" @@ -268,7 +269,7 @@ "(app (Checkcast C) G maxs rT pc et (Some s)) = (\rT ST LT. s = (RefT rT#ST,LT) \ is_class G C \ (\x \ set (match G ClassCast pc et). is_class G x))" - by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto) + by (cases s, cases "fst s", simp) (cases "hd (fst s)", auto) lemma appPop[simp]: "(app Pop G maxs rT pc et (Some s)) = (\ts ST LT. s = (ts#ST,LT))" @@ -359,7 +360,7 @@ assume app: "?app (a,b)" hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \ length fpTs < length a" (is "?a \ ?l") - by (auto simp add: app_def) + by auto hence "?a \ 0 < length (drop (length fpTs) a)" (is "?a \ ?l") by auto hence "?a \ ?l \ length (rev (take (length fpTs) a)) = length fpTs" @@ -374,7 +375,7 @@ hence "\apTs X ST. a = rev apTs @ X # ST \ length apTs = length fpTs" by blast with app - show ?thesis by (unfold app_def, clarsimp) blast + show ?thesis by clarsimp blast qed with Pair have "?app s \ ?P s" by (simp only:) diff -r 118cda173627 -r 5d88ffdb290c src/HOL/MicroJava/JVM/JVMExec.thy --- a/src/HOL/MicroJava/JVM/JVMExec.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Tue Mar 02 15:39:15 2010 +0100 @@ -8,21 +8,19 @@ theory JVMExec imports JVMExecInstr JVMExceptions begin -consts +fun exec :: "jvm_prog \ jvm_state => jvm_state option" - - --- "exec is not recursive. recdef is just used for pattern matching" -recdef exec "{}" +-- "exec is not recursive. fun is just used for pattern matching" +where "exec (G, xp, hp, []) = None" - "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = +| "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = (let i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc; (xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs in Some (find_handler G xcpt' hp' frs'))" - "exec (G, Some xp, hp, frs) = None" +| "exec (G, Some xp, hp, frs) = None" definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" diff -r 118cda173627 -r 5d88ffdb290c src/HOL/Old_Number_Theory/EulerFermat.thy --- a/src/HOL/Old_Number_Theory/EulerFermat.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Tue Mar 02 15:39:15 2010 +0100 @@ -25,20 +25,18 @@ | insert: "A \ RsetR m ==> zgcd a m = 1 ==> \a'. a' \ A --> \ zcong a a' m ==> insert a A \ RsetR m" -consts - BnorRset :: "int * int => int set" - -recdef BnorRset - "measure ((\(a, m). nat a) :: int * int => nat)" - "BnorRset (a, m) = +fun + BnorRset :: "int \ int => int set" +where + "BnorRset a m = (if 0 < a then - let na = BnorRset (a - 1, m) + let na = BnorRset (a - 1) m in (if zgcd a m = 1 then insert a na else na) else {})" definition norRRset :: "int => int set" where - "norRRset m = BnorRset (m - 1, m)" + "norRRset m = BnorRset (m - 1) m" definition noXRRset :: "int => int => int set" where @@ -74,28 +72,27 @@ lemma BnorRset_induct: assumes "!!a m. P {} a m" - and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m - ==> P (BnorRset(a,m)) a m" - shows "P (BnorRset(u,v)) u v" + and "!!a m :: int. 0 < a ==> P (BnorRset (a - 1) m) (a - 1) m + ==> P (BnorRset a m) a m" + shows "P (BnorRset u v) u v" apply (rule BnorRset.induct) - apply safe - apply (case_tac [2] "0 < a") - apply (rule_tac [2] prems) + apply (case_tac "0 < a") + apply (rule_tac assms) apply simp_all - apply (simp_all add: BnorRset.simps prems) + apply (simp_all add: BnorRset.simps assms) done -lemma Bnor_mem_zle [rule_format]: "b \ BnorRset (a, m) \ b \ a" +lemma Bnor_mem_zle [rule_format]: "b \ BnorRset a m \ b \ a" apply (induct a m rule: BnorRset_induct) apply simp apply (subst BnorRset.simps) apply (unfold Let_def, auto) done -lemma Bnor_mem_zle_swap: "a < b ==> b \ BnorRset (a, m)" +lemma Bnor_mem_zle_swap: "a < b ==> b \ BnorRset a m" by (auto dest: Bnor_mem_zle) -lemma Bnor_mem_zg [rule_format]: "b \ BnorRset (a, m) --> 0 < b" +lemma Bnor_mem_zg [rule_format]: "b \ BnorRset a m --> 0 < b" apply (induct a m rule: BnorRset_induct) prefer 2 apply (subst BnorRset.simps) @@ -103,7 +100,7 @@ done lemma Bnor_mem_if [rule_format]: - "zgcd b m = 1 --> 0 < b --> b \ a --> b \ BnorRset (a, m)" + "zgcd b m = 1 --> 0 < b --> b \ a --> b \ BnorRset a m" apply (induct a m rule: BnorRset.induct, auto) apply (subst BnorRset.simps) defer @@ -111,7 +108,7 @@ apply (unfold Let_def, auto) done -lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \ RsetR m" +lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset a m \ RsetR m" apply (induct a m rule: BnorRset_induct, simp) apply (subst BnorRset.simps) apply (unfold Let_def, auto) @@ -124,7 +121,7 @@ apply (rule_tac [5] Bnor_mem_zg, auto) done -lemma Bnor_fin: "finite (BnorRset (a, m))" +lemma Bnor_fin: "finite (BnorRset a m)" apply (induct a m rule: BnorRset_induct) prefer 2 apply (subst BnorRset.simps) @@ -258,8 +255,8 @@ by (unfold inj_on_def, auto) lemma Bnor_prod_power [rule_format]: - "x \ 0 ==> a < m --> \((\a. a * x) ` BnorRset (a, m)) = - \(BnorRset(a, m)) * x^card (BnorRset (a, m))" + "x \ 0 ==> a < m --> \((\a. a * x) ` BnorRset a m) = + \(BnorRset a m) * x^card (BnorRset a m)" apply (induct a m rule: BnorRset_induct) prefer 2 apply (simplesubst BnorRset.simps) --{*multiple redexes*} @@ -284,7 +281,7 @@ done lemma Bnor_prod_zgcd [rule_format]: - "a < m --> zgcd (\(BnorRset(a, m))) m = 1" + "a < m --> zgcd (\(BnorRset a m)) m = 1" apply (induct a m rule: BnorRset_induct) prefer 2 apply (subst BnorRset.simps) @@ -299,13 +296,13 @@ apply (case_tac "x = 0") apply (case_tac [2] "m = 1") apply (rule_tac [3] iffD1) - apply (rule_tac [3] k = "\(BnorRset(m - 1, m))" + apply (rule_tac [3] k = "\(BnorRset (m - 1) m)" in zcong_cancel2) prefer 5 apply (subst Bnor_prod_power [symmetric]) apply (rule_tac [7] Bnor_prod_zgcd, simp_all) apply (rule bijzcong_zcong_prod) - apply (fold norRRset_def noXRRset_def) + apply (fold norRRset_def, fold noXRRset_def) apply (subst RRset2norRR_eq_norR [symmetric]) apply (rule_tac [3] inj_func_bijR, auto) apply (unfold zcongm_def) @@ -319,12 +316,12 @@ done lemma Bnor_prime: - "\ zprime p; a < p \ \ card (BnorRset (a, p)) = nat a" + "\ zprime p; a < p \ \ card (BnorRset a p) = nat a" apply (induct a p rule: BnorRset.induct) apply (subst BnorRset.simps) apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime) - apply (subgoal_tac "finite (BnorRset (a - 1,m))") - apply (subgoal_tac "a ~: BnorRset (a - 1,m)") + apply (subgoal_tac "finite (BnorRset (a - 1) m)") + apply (subgoal_tac "a ~: BnorRset (a - 1) m") apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1) apply (frule Bnor_mem_zle, arith) apply (frule Bnor_fin) diff -r 118cda173627 -r 5d88ffdb290c src/HOL/Old_Number_Theory/IntFact.thy --- a/src/HOL/Old_Number_Theory/IntFact.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/Old_Number_Theory/IntFact.thy Tue Mar 02 15:39:15 2010 +0100 @@ -14,14 +14,14 @@ \bigskip *} -consts +fun zfact :: "int => int" - d22set :: "int => int set" - -recdef zfact "measure ((\n. nat n) :: int => nat)" +where "zfact n = (if n \ 0 then 1 else n * zfact (n - 1))" -recdef d22set "measure ((\a. nat a) :: int => nat)" +fun + d22set :: "int => int set" +where "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})" @@ -38,12 +38,10 @@ and "!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a" shows "P (d22set u) u" apply (rule d22set.induct) - apply safe - prefer 2 - apply (case_tac "1 < a") - apply (rule_tac prems) - apply (simp_all (no_asm_simp)) - apply (simp_all (no_asm_simp) add: d22set.simps prems) + apply (case_tac "1 < a") + apply (rule_tac assms) + apply (simp_all (no_asm_simp)) + apply (simp_all (no_asm_simp) add: d22set.simps assms) done lemma d22set_g_1 [rule_format]: "b \ d22set a --> 1 < b" @@ -66,7 +64,8 @@ lemma d22set_mem: "1 < b \ b \ a \ b \ d22set a" apply (induct a rule: d22set.induct) apply auto - apply (simp_all add: d22set.simps) + apply (subst d22set.simps) + apply (case_tac "b < a", auto) done lemma d22set_fin: "finite (d22set a)" @@ -81,8 +80,6 @@ lemma d22set_prod_zfact: "\(d22set a) = zfact a" apply (induct a rule: d22set.induct) - apply safe - apply (simp add: d22set.simps zfact.simps) apply (subst d22set.simps) apply (subst zfact.simps) apply (case_tac "1 < a") diff -r 118cda173627 -r 5d88ffdb290c src/HOL/Old_Number_Theory/IntPrimes.thy --- a/src/HOL/Old_Number_Theory/IntPrimes.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Tue Mar 02 15:39:15 2010 +0100 @@ -19,17 +19,14 @@ subsection {* Definitions *} -consts - xzgcda :: "int * int * int * int * int * int * int * int => int * int * int" - -recdef xzgcda - "measure ((\(m, n, r', r, s', s, t', t). nat r) - :: int * int * int * int *int * int * int * int => nat)" - "xzgcda (m, n, r', r, s', s, t', t) = +fun + xzgcda :: "int \ int \ int \ int \ int \ int \ int \ int => (int * int * int)" +where + "xzgcda m n r' r s' s t' t = (if r \ 0 then (r', s', t') - else xzgcda (m, n, r, r' mod r, - s, s' - (r' div r) * s, - t, t' - (r' div r) * t))" + else xzgcda m n r (r' mod r) + s (s' - (r' div r) * s) + t (t' - (r' div r) * t))" definition zprime :: "int \ bool" where @@ -37,7 +34,7 @@ definition xzgcd :: "int => int => int * int * int" where - "xzgcd m n = xzgcda (m, n, m, n, 1, 0, 0, 1)" + "xzgcd m n = xzgcda m n m n 1 0 0 1" definition zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))") where @@ -307,9 +304,8 @@ lemma xzgcd_correct_aux1: "zgcd r' r = k --> 0 < r --> - (\sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))" - apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and - z = s and aa = t' and ab = t in xzgcda.induct) + (\sn tn. xzgcda m n r' r s' s t' t = (k, sn, tn))" + apply (induct m n r' r s' s t' t rule: xzgcda.induct) apply (subst zgcd_eq) apply (subst xzgcda.simps, auto) apply (case_tac "r' mod r = 0") @@ -321,17 +317,16 @@ done lemma xzgcd_correct_aux2: - "(\sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r --> + "(\sn tn. xzgcda m n r' r s' s t' t = (k, sn, tn)) --> 0 < r --> zgcd r' r = k" - apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and - z = s and aa = t' and ab = t in xzgcda.induct) + apply (induct m n r' r s' s t' t rule: xzgcda.induct) apply (subst zgcd_eq) apply (subst xzgcda.simps) apply (auto simp add: linorder_not_le) apply (case_tac "r' mod r = 0") prefer 2 apply (frule_tac a = "r'" in pos_mod_sign, auto) - apply (metis Pair_eq simps zle_refl) + apply (metis Pair_eq xzgcda.simps zle_refl) done lemma xzgcd_correct: @@ -362,10 +357,9 @@ by (rule iffD2 [OF order_less_le conjI]) lemma xzgcda_linear [rule_format]: - "0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) --> + "0 < r --> xzgcda m n r' r s' s t' t = (rn, sn, tn) --> r' = s' * m + t' * n --> r = s * m + t * n --> rn = sn * m + tn * n" - apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and - z = s and aa = t' and ab = t in xzgcda.induct) + apply (induct m n r' r s' s t' t rule: xzgcda.induct) apply (subst xzgcda.simps) apply (simp (no_asm)) apply (rule impI)+ diff -r 118cda173627 -r 5d88ffdb290c src/HOL/Old_Number_Theory/WilsonRuss.thy --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Tue Mar 02 15:39:15 2010 +0100 @@ -17,14 +17,12 @@ inv :: "int => int => int" where "inv p a = (a^(nat (p - 2))) mod p" -consts - wset :: "int * int => int set" - -recdef wset - "measure ((\(a, p). nat a) :: int * int => nat)" - "wset (a, p) = +fun + wset :: "int \ int => int set" +where + "wset a p = (if 1 < a then - let ws = wset (a - 1, p) + let ws = wset (a - 1) p in (if a \ ws then ws else insert a (insert (inv p a) ws)) else {})" @@ -163,35 +161,33 @@ lemma wset_induct: assumes "!!a p. P {} a p" and "!!a p. 1 < (a::int) \ - P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p" - shows "P (wset (u, v)) u v" - apply (rule wset.induct, safe) - prefer 2 - apply (case_tac "1 < a") - apply (rule prems) - apply simp_all - apply (simp_all add: wset.simps prems) + P (wset (a - 1) p) (a - 1) p ==> P (wset a p) a p" + shows "P (wset u v) u v" + apply (rule wset.induct) + apply (case_tac "1 < a") + apply (rule assms) + apply (simp_all add: wset.simps assms) done lemma wset_mem_imp_or [rule_format]: - "1 < a \ b \ wset (a - 1, p) - ==> b \ wset (a, p) --> b = a \ b = inv p a" + "1 < a \ b \ wset (a - 1) p + ==> b \ wset a p --> b = a \ b = inv p a" apply (subst wset.simps) apply (unfold Let_def, simp) done -lemma wset_mem_mem [simp]: "1 < a ==> a \ wset (a, p)" +lemma wset_mem_mem [simp]: "1 < a ==> a \ wset a p" apply (subst wset.simps) apply (unfold Let_def, simp) done -lemma wset_subset: "1 < a \ b \ wset (a - 1, p) ==> b \ wset (a, p)" +lemma wset_subset: "1 < a \ b \ wset (a - 1) p ==> b \ wset a p" apply (subst wset.simps) apply (unfold Let_def, auto) done lemma wset_g_1 [rule_format]: - "zprime p --> a < p - 1 --> b \ wset (a, p) --> 1 < b" + "zprime p --> a < p - 1 --> b \ wset a p --> 1 < b" apply (induct a p rule: wset_induct, auto) apply (case_tac "b = a") apply (case_tac [2] "b = inv p a") @@ -203,7 +199,7 @@ done lemma wset_less [rule_format]: - "zprime p --> a < p - 1 --> b \ wset (a, p) --> b < p - 1" + "zprime p --> a < p - 1 --> b \ wset a p --> b < p - 1" apply (induct a p rule: wset_induct, auto) apply (case_tac "b = a") apply (case_tac [2] "b = inv p a") @@ -216,7 +212,7 @@ lemma wset_mem [rule_format]: "zprime p --> - a < p - 1 --> 1 < b --> b \ a --> b \ wset (a, p)" + a < p - 1 --> 1 < b --> b \ a --> b \ wset a p" apply (induct a p rule: wset.induct, auto) apply (rule_tac wset_subset) apply (simp (no_asm_simp)) @@ -224,8 +220,8 @@ done lemma wset_mem_inv_mem [rule_format]: - "zprime p --> 5 \ p --> a < p - 1 --> b \ wset (a, p) - --> inv p b \ wset (a, p)" + "zprime p --> 5 \ p --> a < p - 1 --> b \ wset a p + --> inv p b \ wset a p" apply (induct a p rule: wset_induct, auto) apply (case_tac "b = a") apply (subst wset.simps) @@ -240,13 +236,13 @@ lemma wset_inv_mem_mem: "zprime p \ 5 \ p \ a < p - 1 \ 1 < b \ b < p - 1 - \ inv p b \ wset (a, p) \ b \ wset (a, p)" + \ inv p b \ wset a p \ b \ wset a p" apply (rule_tac s = "inv p (inv p b)" and t = b in subst) apply (rule_tac [2] wset_mem_inv_mem) apply (rule inv_inv, simp_all) done -lemma wset_fin: "finite (wset (a, p))" +lemma wset_fin: "finite (wset a p)" apply (induct a p rule: wset_induct) prefer 2 apply (subst wset.simps) @@ -255,27 +251,27 @@ lemma wset_zcong_prod_1 [rule_format]: "zprime p --> - 5 \ p --> a < p - 1 --> [(\x\wset(a, p). x) = 1] (mod p)" + 5 \ p --> a < p - 1 --> [(\x\wset a p. x) = 1] (mod p)" apply (induct a p rule: wset_induct) prefer 2 apply (subst wset.simps) - apply (unfold Let_def, auto) + apply (auto, unfold Let_def, auto) apply (subst setprod_insert) apply (tactic {* stac (thm "setprod_insert") 3 *}) apply (subgoal_tac [5] - "zcong (a * inv p a * (\x\ wset(a - 1, p). x)) (1 * 1) p") + "zcong (a * inv p a * (\x\wset (a - 1) p. x)) (1 * 1) p") prefer 5 apply (simp add: zmult_assoc) apply (rule_tac [5] zcong_zmult) apply (rule_tac [5] inv_is_inv) apply (tactic "clarify_tac @{claset} 4") - apply (subgoal_tac [4] "a \ wset (a - 1, p)") + apply (subgoal_tac [4] "a \ wset (a - 1) p") apply (rule_tac [5] wset_inv_mem_mem) apply (simp_all add: wset_fin) apply (rule inv_distinct, auto) done -lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2, p)" +lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2) p" apply safe apply (erule wset_mem) apply (rule_tac [2] d22set_g_1) diff -r 118cda173627 -r 5d88ffdb290c src/HOL/RealPow.thy --- a/src/HOL/RealPow.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/RealPow.thy Tue Mar 02 15:39:15 2010 +0100 @@ -113,9 +113,6 @@ lemma real_le_add_half_cancel: "(x + y/2 \ (y::real)) = (x \ y /2)" by auto -lemma real_minus_half_eq [simp]: "(x::real) - x/2 = x/2" -by auto - lemma real_mult_inverse_cancel: "[|(0::real) < x; 0 < x1; x1 * y < x * u |] ==> inverse x * y < inverse x1 * u" diff -r 118cda173627 -r 5d88ffdb290c src/HOL/ZF/Games.thy --- a/src/HOL/ZF/Games.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/ZF/Games.thy Tue Mar 02 15:39:15 2010 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/ZF/Games.thy +(* Title: HOL/ZF/MainZF.thy/Games.thy Author: Steven Obua An application of HOLZF: Partizan Games. See "Partizan Games in @@ -347,13 +347,12 @@ right_option_def[symmetric] left_option_def[symmetric]) done -consts +function neg_game :: "game \ game" - -recdef neg_game "option_of" - "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))" - -declare neg_game.simps[simp del] +where + [simp del]: "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))" +by auto +termination by (relation "option_of") auto lemma "neg_game (neg_game g) = g" apply (induct g rule: neg_game.induct) @@ -365,17 +364,16 @@ apply (auto simp add: zet_ext_eq zimage_iff) done -consts +function ge_game :: "(game * game) \ bool" - -recdef ge_game "(gprod_2_1 option_of)" - "ge_game (G, H) = (\ x. if zin x (right_options G) then ( +where + [simp del]: "ge_game (G, H) = (\ x. if zin x (right_options G) then ( if zin x (left_options H) then \ (ge_game (H, x) \ (ge_game (x, G))) else \ (ge_game (H, x))) else (if zin x (left_options H) then \ (ge_game (x, G)) else True))" -(hints simp: gprod_2_1_def) - -declare ge_game.simps [simp del] +by auto +termination by (relation "(gprod_2_1 option_of)") + (simp, auto simp: gprod_2_1_def) lemma ge_game_eq: "ge_game (G, H) = (\ x. (zin x (right_options G) \ \ ge_game (H, x)) \ (zin x (left_options H) \ \ ge_game (x, G)))" apply (subst ge_game.simps[where G=G and H=H]) @@ -506,19 +504,18 @@ definition zero_game :: game where "zero_game \ Game zempty zempty" -consts - plus_game :: "game * game \ game" +function + plus_game :: "game \ game \ game" +where + [simp del]: "plus_game G H = Game (zunion (zimage (\ g. plus_game g H) (left_options G)) + (zimage (\ h. plus_game G h) (left_options H))) + (zunion (zimage (\ g. plus_game g H) (right_options G)) + (zimage (\ h. plus_game G h) (right_options H)))" +by auto +termination by (relation "gprod_2_2 option_of") + (simp, auto simp: gprod_2_2_def) -recdef plus_game "gprod_2_2 option_of" - "plus_game (G, H) = Game (zunion (zimage (\ g. plus_game (g, H)) (left_options G)) - (zimage (\ h. plus_game (G, h)) (left_options H))) - (zunion (zimage (\ g. plus_game (g, H)) (right_options G)) - (zimage (\ h. plus_game (G, h)) (right_options H)))" -(hints simp add: gprod_2_2_def) - -declare plus_game.simps[simp del] - -lemma plus_game_comm: "plus_game (G, H) = plus_game (H, G)" +lemma plus_game_comm: "plus_game G H = plus_game H G" proof (induct G H rule: plus_game.induct) case (1 G H) show ?case @@ -541,11 +538,11 @@ lemma right_zero_game[simp]: "right_options (zero_game) = zempty" by (simp add: zero_game_def) -lemma plus_game_zero_right[simp]: "plus_game (G, zero_game) = G" +lemma plus_game_zero_right[simp]: "plus_game G zero_game = G" proof - { fix G H - have "H = zero_game \ plus_game (G, H) = G " + have "H = zero_game \ plus_game G H = G " proof (induct G H rule: plus_game.induct, rule impI) case (goal1 G H) note induct_hyp = prems[simplified goal1, simplified] and prems @@ -553,7 +550,7 @@ apply (simp only: plus_game.simps[where G=G and H=H]) apply (simp add: game_ext_eq prems) apply (auto simp add: - zimage_cong[where f = "\ g. plus_game (g, zero_game)" and g = "id"] + zimage_cong[where f = "\ g. plus_game g zero_game" and g = "id"] induct_hyp) done qed @@ -561,7 +558,7 @@ then show ?thesis by auto qed -lemma plus_game_zero_left: "plus_game (zero_game, G) = G" +lemma plus_game_zero_left: "plus_game zero_game G = G" by (simp add: plus_game_comm) lemma left_imp_options[simp]: "zin opt (left_options g) \ zin opt (options g)" @@ -571,11 +568,11 @@ by (simp add: options_def zunion) lemma left_options_plus: - "left_options (plus_game (u, v)) = zunion (zimage (\g. plus_game (g, v)) (left_options u)) (zimage (\h. plus_game (u, h)) (left_options v))" + "left_options (plus_game u v) = zunion (zimage (\g. plus_game g v) (left_options u)) (zimage (\h. plus_game u h) (left_options v))" by (subst plus_game.simps, simp) lemma right_options_plus: - "right_options (plus_game (u, v)) = zunion (zimage (\g. plus_game (g, v)) (right_options u)) (zimage (\h. plus_game (u, h)) (right_options v))" + "right_options (plus_game u v) = zunion (zimage (\g. plus_game g v) (right_options u)) (zimage (\h. plus_game u h) (right_options v))" by (subst plus_game.simps, simp) lemma left_options_neg: "left_options (neg_game u) = zimage neg_game (right_options u)" @@ -584,32 +581,32 @@ lemma right_options_neg: "right_options (neg_game u) = zimage neg_game (left_options u)" by (subst neg_game.simps, simp) -lemma plus_game_assoc: "plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))" +lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)" proof - { fix a - have "\ F G H. a = [F, G, H] \ plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))" + have "\ F G H. a = [F, G, H] \ plus_game (plus_game F G) H = plus_game F (plus_game G H)" proof (induct a rule: induct_game, (rule impI | rule allI)+) case (goal1 x F G H) - let ?L = "plus_game (plus_game (F, G), H)" - let ?R = "plus_game (F, plus_game (G, H))" + let ?L = "plus_game (plus_game F G) H" + let ?R = "plus_game F (plus_game G H)" note options_plus = left_options_plus right_options_plus { fix opt note hyp = goal1(1)[simplified goal1(2), rule_format] - have F: "zin opt (options F) \ plus_game (plus_game (opt, G), H) = plus_game (opt, plus_game (G, H))" + have F: "zin opt (options F) \ plus_game (plus_game opt G) H = plus_game opt (plus_game G H)" by (blast intro: hyp lprod_3_3) - have G: "zin opt (options G) \ plus_game (plus_game (F, opt), H) = plus_game (F, plus_game (opt, H))" + have G: "zin opt (options G) \ plus_game (plus_game F opt) H = plus_game F (plus_game opt H)" by (blast intro: hyp lprod_3_4) - have H: "zin opt (options H) \ plus_game (plus_game (F, G), opt) = plus_game (F, plus_game (G, opt))" + have H: "zin opt (options H) \ plus_game (plus_game F G) opt = plus_game F (plus_game G opt)" by (blast intro: hyp lprod_3_5) note F and G and H } note induct_hyp = this have "left_options ?L = left_options ?R \ right_options ?L = right_options ?R" by (auto simp add: - plus_game.simps[where G="plus_game (F,G)" and H=H] - plus_game.simps[where G="F" and H="plus_game (G,H)"] + plus_game.simps[where G="plus_game F G" and H=H] + plus_game.simps[where G="F" and H="plus_game G H"] zet_ext_eq zunion zimage_iff options_plus induct_hyp left_imp_options right_imp_options) then show ?case @@ -619,7 +616,7 @@ then show ?thesis by auto qed -lemma neg_plus_game: "neg_game (plus_game (G, H)) = plus_game(neg_game G, neg_game H)" +lemma neg_plus_game: "neg_game (plus_game G H) = plus_game (neg_game G) (neg_game H)" proof (induct G H rule: plus_game.induct) case (1 G H) note opt_ops = @@ -627,26 +624,26 @@ left_options_neg right_options_neg show ?case by (auto simp add: opt_ops - neg_game.simps[of "plus_game (G,H)"] + neg_game.simps[of "plus_game G H"] plus_game.simps[of "neg_game G" "neg_game H"] Game_ext zet_ext_eq zunion zimage_iff prems) qed -lemma eq_game_plus_inverse: "eq_game (plus_game (x, neg_game x)) zero_game" +lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game" proof (induct x rule: wf_induct[OF wf_option_of]) case (goal1 x) { fix y assume "zin y (options x)" - then have "eq_game (plus_game (y, neg_game y)) zero_game" + then have "eq_game (plus_game y (neg_game y)) zero_game" by (auto simp add: prems) } note ihyp = this { fix y assume y: "zin y (right_options x)" - have "\ (ge_game (zero_game, plus_game (y, neg_game x)))" + have "\ (ge_game (zero_game, plus_game y (neg_game x)))" apply (subst ge_game.simps, simp) - apply (rule exI[where x="plus_game (y, neg_game y)"]) + apply (rule exI[where x="plus_game y (neg_game y)"]) apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def]) apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: prems) done @@ -655,9 +652,9 @@ { fix y assume y: "zin y (left_options x)" - have "\ (ge_game (zero_game, plus_game (x, neg_game y)))" + have "\ (ge_game (zero_game, plus_game x (neg_game y)))" apply (subst ge_game.simps, simp) - apply (rule exI[where x="plus_game (y, neg_game y)"]) + apply (rule exI[where x="plus_game y (neg_game y)"]) apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def]) apply (auto simp add: left_options_plus zunion zimage_iff intro: prems) done @@ -666,9 +663,9 @@ { fix y assume y: "zin y (left_options x)" - have "\ (ge_game (plus_game (y, neg_game x), zero_game))" + have "\ (ge_game (plus_game y (neg_game x), zero_game))" apply (subst ge_game.simps, simp) - apply (rule exI[where x="plus_game (y, neg_game y)"]) + apply (rule exI[where x="plus_game y (neg_game y)"]) apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def]) apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: prems) done @@ -677,9 +674,9 @@ { fix y assume y: "zin y (right_options x)" - have "\ (ge_game (plus_game (x, neg_game y), zero_game))" + have "\ (ge_game (plus_game x (neg_game y), zero_game))" apply (subst ge_game.simps, simp) - apply (rule exI[where x="plus_game (y, neg_game y)"]) + apply (rule exI[where x="plus_game y (neg_game y)"]) apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def]) apply (auto simp add: right_options_plus zunion zimage_iff intro: prems) done @@ -687,28 +684,28 @@ note case4 = this show ?case apply (simp add: eq_game_def) - apply (simp add: ge_game.simps[of "plus_game (x, neg_game x)" "zero_game"]) - apply (simp add: ge_game.simps[of "zero_game" "plus_game (x, neg_game x)"]) + apply (simp add: ge_game.simps[of "plus_game x (neg_game x)" "zero_game"]) + apply (simp add: ge_game.simps[of "zero_game" "plus_game x (neg_game x)"]) apply (simp add: right_options_plus left_options_plus right_options_neg left_options_neg zunion zimage_iff) apply (auto simp add: case1 case2 case3 case4) done qed -lemma ge_plus_game_left: "ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))" +lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)" proof - { fix a - have "\ x y z. a = [x,y,z] \ ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))" + have "\ x y z. a = [x,y,z] \ ge_game (y,z) = ge_game (plus_game x y, plus_game x z)" proof (induct a rule: induct_game, (rule impI | rule allI)+) case (goal1 a x y z) note induct_hyp = goal1(1)[rule_format, simplified goal1(2)] { - assume hyp: "ge_game(plus_game (x, y), plus_game (x, z))" + assume hyp: "ge_game(plus_game x y, plus_game x z)" have "ge_game (y, z)" proof - { fix yr assume yr: "zin yr (right_options y)" - from hyp have "\ (ge_game (plus_game (x, z), plus_game (x, yr)))" - by (auto simp add: ge_game_eq[of "plus_game (x,y)" "plus_game(x,z)"] + from hyp have "\ (ge_game (plus_game x z, plus_game x yr))" + by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"] right_options_plus zunion zimage_iff intro: yr) then have "\ (ge_game (z, yr))" apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"]) @@ -718,8 +715,8 @@ note yr = this { fix zl assume zl: "zin zl (left_options z)" - from hyp have "\ (ge_game (plus_game (x, zl), plus_game (x, y)))" - by (auto simp add: ge_game_eq[of "plus_game (x,y)" "plus_game(x,z)"] + from hyp have "\ (ge_game (plus_game x zl, plus_game x y))" + by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"] left_options_plus zunion zimage_iff intro: zl) then have "\ (ge_game (zl, y))" apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"]) @@ -739,11 +736,11 @@ { fix x' assume x': "zin x' (right_options x)" - assume hyp: "ge_game (plus_game (x, z), plus_game (x', y))" - then have n: "\ (ge_game (plus_game (x', y), plus_game (x', z)))" - by (auto simp add: ge_game_eq[of "plus_game (x,z)" "plus_game (x', y)"] + assume hyp: "ge_game (plus_game x z, plus_game x' y)" + then have n: "\ (ge_game (plus_game x' y, plus_game x' z))" + by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"] right_options_plus zunion zimage_iff intro: x') - have t: "ge_game (plus_game (x', y), plus_game (x', z))" + have t: "ge_game (plus_game x' y, plus_game x' z)" apply (subst induct_hyp[symmetric]) apply (auto intro: lprod_3_3 x' yz) done @@ -753,11 +750,11 @@ { fix x' assume x': "zin x' (left_options x)" - assume hyp: "ge_game (plus_game (x', z), plus_game (x, y))" - then have n: "\ (ge_game (plus_game (x', y), plus_game (x', z)))" - by (auto simp add: ge_game_eq[of "plus_game (x',z)" "plus_game (x, y)"] + assume hyp: "ge_game (plus_game x' z, plus_game x y)" + then have n: "\ (ge_game (plus_game x' y, plus_game x' z))" + by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"] left_options_plus zunion zimage_iff intro: x') - have t: "ge_game (plus_game (x', y), plus_game (x', z))" + have t: "ge_game (plus_game x' y, plus_game x' z)" apply (subst induct_hyp[symmetric]) apply (auto intro: lprod_3_3 x' yz) done @@ -767,7 +764,7 @@ { fix y' assume y': "zin y' (right_options y)" - assume hyp: "ge_game (plus_game(x, z), plus_game (x, y'))" + assume hyp: "ge_game (plus_game x z, plus_game x y')" then have "ge_game(z, y')" apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"]) apply (auto simp add: hyp lprod_3_6 y') @@ -780,7 +777,7 @@ { fix z' assume z': "zin z' (left_options z)" - assume hyp: "ge_game (plus_game(x, z'), plus_game (x, y))" + assume hyp: "ge_game (plus_game x z', plus_game x y)" then have "ge_game(z', y)" apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"]) apply (auto simp add: hyp lprod_3_7 z') @@ -790,7 +787,7 @@ with z' have "False" by (auto simp add: ge_game_leftright_refl) } note case4 = this - have "ge_game(plus_game (x, y), plus_game (x, z))" + have "ge_game(plus_game x y, plus_game x z)" apply (subst ge_game_eq) apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff) apply (auto intro: case1 case2 case3 case4) @@ -804,7 +801,7 @@ then show ?thesis by blast qed -lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game (y, x), plus_game (z, x))" +lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game y x, plus_game z x)" by (simp add: ge_plus_game_left plus_game_comm) lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)" @@ -865,7 +862,7 @@ Pg_minus_def: "- G = contents (\ g \ Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})" definition - Pg_plus_def: "G + H = contents (\ g \ Rep_Pg G. \ h \ Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game (g,h)})})" + Pg_plus_def: "G + H = contents (\ g \ Rep_Pg G. \ h \ Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})" definition Pg_diff_def: "G - H = G + (- (H::Pg))" @@ -891,14 +888,14 @@ apply (simp add: eq_game_rel_def) done -lemma char_Pg_plus[simp]: "Abs_Pg (eq_game_rel `` {g}) + Abs_Pg (eq_game_rel `` {h}) = Abs_Pg (eq_game_rel `` {plus_game (g, h)})" +lemma char_Pg_plus[simp]: "Abs_Pg (eq_game_rel `` {g}) + Abs_Pg (eq_game_rel `` {h}) = Abs_Pg (eq_game_rel `` {plus_game g h})" proof - - have "(\ g h. {Abs_Pg (eq_game_rel `` {plus_game (g, h)})}) respects2 eq_game_rel" + have "(\ g h. {Abs_Pg (eq_game_rel `` {plus_game g h})}) respects2 eq_game_rel" apply (simp add: congruent2_def) apply (auto simp add: eq_game_rel_def eq_game_def) - apply (rule_tac y="plus_game (y1, z2)" in ge_game_trans) + apply (rule_tac y="plus_game y1 z2" in ge_game_trans) apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+ - apply (rule_tac y="plus_game (z1, y2)" in ge_game_trans) + apply (rule_tac y="plus_game z1 y2" in ge_game_trans) apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+ done then show ?thesis diff -r 118cda173627 -r 5d88ffdb290c src/HOL/ZF/Zet.thy --- a/src/HOL/ZF/Zet.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/ZF/Zet.thy Tue Mar 02 15:39:15 2010 +0100 @@ -196,7 +196,7 @@ lemma zimage_id[simp]: "zimage id A = A" by (simp add: zet_ext_eq zimage_iff) -lemma zimage_cong[recdef_cong]: "\ M = N; !! x. zin x N \ f x = g x \ \ zimage f M = zimage g N" +lemma zimage_cong[recdef_cong, fundef_cong]: "\ M = N; !! x. zin x N \ f x = g x \ \ zimage f M = zimage g N" by (auto simp add: zet_ext_eq zimage_iff) end diff -r 118cda173627 -r 5d88ffdb290c src/HOL/ex/Gauge_Integration.thy --- a/src/HOL/ex/Gauge_Integration.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOL/ex/Gauge_Integration.thy Tue Mar 02 15:39:15 2010 +0100 @@ -28,7 +28,7 @@ definition gauge :: "[real set, real => real] => bool" where - [code del]:"gauge E g = (\x\E. 0 < g(x))" + [code del]: "gauge E g = (\x\E. 0 < g(x))" subsection {* Gauge-fine divisions *} @@ -63,14 +63,20 @@ apply (drule fine_imp_le, simp) done -lemma empty_fine_imp_eq: "\fine \ (a, b) D; D = []\ \ a = b" -by (induct set: fine, simp_all) +lemma fine_Nil_iff: "fine \ (a, b) [] \ a = b" +by (auto elim: fine.cases intro: fine.intros) -lemma fine_eq: "fine \ (a, b) D \ a = b \ D = []" -apply (cases "D = []") -apply (drule (1) empty_fine_imp_eq, simp) -apply (drule (1) nonempty_fine_imp_less, simp) -done +lemma fine_same_iff: "fine \ (a, a) D \ D = []" +proof + assume "fine \ (a, a) D" thus "D = []" + by (metis nonempty_fine_imp_less less_irrefl) +next + assume "D = []" thus "fine \ (a, a) D" + by (simp add: fine_Nil) +qed + +lemma empty_fine_imp_eq: "\fine \ (a, b) D; D = []\ \ a = b" +by (simp add: fine_Nil_iff) lemma mem_fine: "\fine \ (a, b) D; (u, x, v) \ set D\ \ u < v \ u \ x \ x \ v" @@ -174,7 +180,7 @@ lemma fine_\_expand: assumes "fine \ (a,b) D" - and "\ x. \ a \ x ; x \ b \ \ \ x \ \' x" + and "\x. a \ x \ x \ b \ \ x \ \' x" shows "fine \' (a,b) D" using assms proof induct case 1 show ?case by (rule fine_Nil) @@ -258,6 +264,22 @@ (\D. fine \ (a,b) D --> \rsum D f - k\ < e)))" +lemma Integral_eq: + "Integral (a, b) f k \ + (\e>0. \\. gauge {a..b} \ \ (\D. fine \ (a,b) D \ \rsum D f - k\ < e))" +unfolding Integral_def by simp + +lemma IntegralI: + assumes "\e. 0 < e \ + \\. gauge {a..b} \ \ (\D. fine \ (a, b) D \ \rsum D f - k\ < e)" + shows "Integral (a, b) f k" +using assms unfolding Integral_def by auto + +lemma IntegralE: + assumes "Integral (a, b) f k" and "0 < e" + obtains \ where "gauge {a..b} \" and "\D. fine \ (a, b) D \ \rsum D f - k\ < e" +using assms unfolding Integral_def by auto + lemma Integral_def2: "Integral = (%(a,b) f k. \e>0. (\\. gauge {a..b} \ & (\D. fine \ (a,b) D --> @@ -272,60 +294,69 @@ text{*The integral is unique if it exists*} lemma Integral_unique: - "[| a \ b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2" -apply (simp add: Integral_def) -apply (drule_tac x = "\k1 - k2\ /2" in spec)+ -apply auto -apply (drule gauge_min, assumption) -apply (drule_tac \ = "%x. min (\ x) (\' x)" - in fine_exists, assumption, auto) -apply (drule fine_min) -apply (drule spec)+ -apply auto -apply (subgoal_tac "\(rsum D f - k2) - (rsum D f - k1)\ < \k1 - k2\") -apply arith -apply (drule add_strict_mono, assumption) -apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] - mult_less_cancel_right) + assumes le: "a \ b" + assumes 1: "Integral (a, b) f k1" + assumes 2: "Integral (a, b) f k2" + shows "k1 = k2" +proof (rule ccontr) + assume "k1 \ k2" + hence e: "0 < \k1 - k2\ / 2" by simp + obtain d1 where "gauge {a..b} d1" and + d1: "\D. fine d1 (a, b) D \ \rsum D f - k1\ < \k1 - k2\ / 2" + using 1 e by (rule IntegralE) + obtain d2 where "gauge {a..b} d2" and + d2: "\D. fine d2 (a, b) D \ \rsum D f - k2\ < \k1 - k2\ / 2" + using 2 e by (rule IntegralE) + have "gauge {a..b} (\x. min (d1 x) (d2 x))" + using `gauge {a..b} d1` and `gauge {a..b} d2` + by (rule gauge_min) + then obtain D where "fine (\x. min (d1 x) (d2 x)) (a, b) D" + using fine_exists [OF le] by fast + hence "fine d1 (a, b) D" and "fine d2 (a, b) D" + by (auto dest: fine_min) + hence "\rsum D f - k1\ < \k1 - k2\ / 2" and "\rsum D f - k2\ < \k1 - k2\ / 2" + using d1 d2 by simp_all + hence "\rsum D f - k1\ + \rsum D f - k2\ < \k1 - k2\ / 2 + \k1 - k2\ / 2" + by (rule add_strict_mono) + thus False by auto +qed + +lemma Integral_zero: "Integral(a,a) f 0" +apply (rule IntegralI) +apply (rule_tac x = "\x. 1" in exI) +apply (simp add: fine_same_iff gauge_def) done -lemma Integral_zero [simp]: "Integral(a,a) f 0" -apply (auto simp add: Integral_def) -apply (rule_tac x = "%x. 1" in exI) -apply (auto dest: fine_eq simp add: gauge_def rsum_def) +lemma Integral_same_iff [simp]: "Integral (a, a) f k \ k = 0" + by (auto intro: Integral_zero Integral_unique) + +lemma Integral_zero_fun: "Integral (a,b) (\x. 0) 0" +apply (rule IntegralI) +apply (rule_tac x="\x. 1" in exI, simp add: gauge_def) done lemma fine_rsum_const: "fine \ (a,b) D \ rsum D (\x. c) = (c * (b - a))" unfolding rsum_def by (induct set: fine, auto simp add: algebra_simps) -lemma Integral_eq_diff_bounds: "a \ b ==> Integral(a,b) (%x. 1) (b - a)" +lemma Integral_mult_const: "a \ b \ Integral(a,b) (\x. c) (c * (b - a))" apply (cases "a = b", simp) -apply (simp add: Integral_def, clarify) -apply (rule_tac x = "%x. b - a" in exI) +apply (rule IntegralI) +apply (rule_tac x = "\x. b - a" in exI) apply (rule conjI, simp add: gauge_def) apply (clarify) apply (subst fine_rsum_const, assumption, simp) done -lemma Integral_mult_const: "a \ b ==> Integral(a,b) (%x. c) (c*(b - a))" -apply (cases "a = b", simp) -apply (simp add: Integral_def, clarify) -apply (rule_tac x = "%x. b - a" in exI) -apply (rule conjI, simp add: gauge_def) -apply (clarify) -apply (subst fine_rsum_const, assumption, simp) -done +lemma Integral_eq_diff_bounds: "a \ b \ Integral(a,b) (\x. 1) (b - a)" + using Integral_mult_const [of a b 1] by simp lemma Integral_mult: "[| a \ b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)" -apply (auto simp add: order_le_less - dest: Integral_unique [OF order_refl Integral_zero]) -apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc) -apply (case_tac "c = 0", force) -apply (drule_tac x = "e/abs c" in spec) -apply (simp add: divide_pos_pos) -apply clarify +apply (auto simp add: order_le_less) +apply (cases "c = 0", simp add: Integral_zero_fun) +apply (rule IntegralI) +apply (erule_tac e="e / \c\" in IntegralE, simp add: divide_pos_pos) apply (rule_tac x="\" in exI, clarify) apply (drule_tac x="D" in spec, clarify) apply (simp add: pos_less_divide_eq abs_mult [symmetric] @@ -337,22 +368,20 @@ assumes "Integral (b, c) f x2" assumes "a \ b" and "b \ c" shows "Integral (a, c) f (x1 + x2)" -proof (cases "a < b \ b < c", simp only: Integral_def split_conv, rule allI, rule impI) +proof (cases "a < b \ b < c", rule IntegralI) fix \ :: real assume "0 < \" hence "0 < \ / 2" by auto assume "a < b \ b < c" hence "a < b" and "b < c" by auto - from `Integral (a, b) f x1`[simplified Integral_def split_conv, - rule_format, OF `0 < \/2`] obtain \1 where \1_gauge: "gauge {a..b} \1" - and I1: "\ D. fine \1 (a,b) D \ \ rsum D f - x1 \ < (\ / 2)" by auto + and I1: "\ D. fine \1 (a,b) D \ \ rsum D f - x1 \ < (\ / 2)" + using IntegralE [OF `Integral (a, b) f x1` `0 < \/2`] by auto - from `Integral (b, c) f x2`[simplified Integral_def split_conv, - rule_format, OF `0 < \/2`] obtain \2 where \2_gauge: "gauge {b..c} \2" - and I2: "\ D. fine \2 (b,c) D \ \ rsum D f - x2 \ < (\ / 2)" by auto + and I2: "\ D. fine \2 (b,c) D \ \ rsum D f - x2 \ < (\ / 2)" + using IntegralE [OF `Integral (b, c) f x2` `0 < \/2`] by auto def \ \ "\ x. if x < b then min (\1 x) (b - x) else if x = b then min (\1 b) (\2 b) @@ -360,6 +389,7 @@ have "gauge {a..c} \" using \1_gauge \2_gauge unfolding \_def gauge_def by auto + moreover { fix D :: "(real \ real \ real) list" assume fine: "fine \ (a,c) D" @@ -462,12 +492,12 @@ thus ?thesis proof (rule disjE) assume "a = b" hence "x1 = 0" - using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto - thus ?thesis using `a = b` `Integral (b, c) f x2` by auto + using `Integral (a, b) f x1` by simp + thus ?thesis using `a = b` `Integral (b, c) f x2` by simp next assume "b = c" hence "x2 = 0" - using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto - thus ?thesis using `b = c` `Integral (a, b) f x1` by auto + using `Integral (b, c) f x2` by simp + thus ?thesis using `b = c` `Integral (a, b) f x1` by simp qed qed @@ -486,7 +516,7 @@ apply (rule_tac z1 = "\inverse (z - x)\" in real_mult_le_cancel_iff2 [THEN iffD1]) apply simp -apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric] +apply (simp del: abs_inverse add: abs_mult [symmetric] mult_assoc [symmetric]) apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) = (f z - f x) / (z - x) - f' x") @@ -543,31 +573,51 @@ qed lemma fundamental_theorem_of_calculus: - "\ a \ b; \x. a \ x & x \ b --> DERIV f x :> f'(x) \ - \ Integral(a,b) f' (f(b) - f(a))" - apply (drule order_le_imp_less_or_eq, auto) - apply (auto simp add: Integral_def2) - apply (drule_tac e = "e / (b - a)" in lemma_straddle) - apply (simp add: divide_pos_pos) - apply clarify - apply (rule_tac x="g" in exI, clarify) - apply (clarsimp simp add: rsum_def) - apply (frule fine_listsum_eq_diff [where f=f]) - apply (erule subst) - apply (subst listsum_subtractf [symmetric]) - apply (rule listsum_abs [THEN order_trans]) - apply (subst map_map [unfolded o_def]) - apply (subgoal_tac "e = (\(u, x, v)\D. (e / (b - a)) * (v - u))") - apply (erule ssubst) - apply (simp add: abs_minus_commute) - apply (rule listsum_mono) - apply (clarify, rename_tac u x v) - apply ((drule spec)+, erule mp) - apply (simp add: mem_fine mem_fine2 mem_fine3) - apply (frule fine_listsum_eq_diff [where f="\x. x"]) - apply (simp only: split_def) - apply (subst listsum_const_mult) - apply simp -done + assumes "a \ b" + assumes f': "\x. a \ x \ x \ b \ DERIV f x :> f'(x)" + shows "Integral (a, b) f' (f(b) - f(a))" +proof (cases "a = b") + assume "a = b" thus ?thesis by simp +next + assume "a \ b" with `a \ b` have "a < b" by simp + show ?thesis + proof (simp add: Integral_def2, clarify) + fix e :: real assume "0 < e" + with `a < b` have "0 < e / (b - a)" by (simp add: divide_pos_pos) + + from lemma_straddle [OF f' this] + obtain \ where "gauge {a..b} \" + and \: "\x u v. \a \ u; u \ x; x \ v; v \ b; v - u < \ x\ \ + \f v - f u - f' x * (v - u)\ \ e * (v - u) / (b - a)" by auto + + have "\D. fine \ (a, b) D \ \rsum D f' - (f b - f a)\ \ e" + proof (clarify) + fix D assume D: "fine \ (a, b) D" + hence "(\(u, x, v)\D. f v - f u) = f b - f a" + by (rule fine_listsum_eq_diff) + hence "\rsum D f' - (f b - f a)\ = \rsum D f' - (\(u, x, v)\D. f v - f u)\" + by simp + also have "\ = \(\(u, x, v)\D. f v - f u) - rsum D f'\" + by (rule abs_minus_commute) + also have "\ = \\(u, x, v)\D. (f v - f u) - f' x * (v - u)\" + by (simp only: rsum_def listsum_subtractf split_def) + also have "\ \ (\(u, x, v)\D. \(f v - f u) - f' x * (v - u)\)" + by (rule ord_le_eq_trans [OF listsum_abs], simp add: o_def split_def) + also have "\ \ (\(u, x, v)\D. (e / (b - a)) * (v - u))" + apply (rule listsum_mono, clarify, rename_tac u x v) + using D apply (simp add: \ mem_fine mem_fine2 mem_fine3) + done + also have "\ = e" + using fine_listsum_eq_diff [OF D, where f="\x. x"] + unfolding split_def listsum_const_mult + using `a < b` by simp + finally show "\rsum D f' - (f b - f a)\ \ e" . + qed + + with `gauge {a..b} \` + show "\\. gauge {a..b} \ \ (\D. fine \ (a, b) D \ \rsum D f' - (f b - f a)\ \ e)" + by auto + qed +qed end diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Domain.thy Tue Mar 02 15:39:15 2010 +0100 @@ -9,6 +9,7 @@ uses ("Tools/cont_consts.ML") ("Tools/cont_proc.ML") + ("Tools/Domain/domain_constructors.ML") ("Tools/Domain/domain_library.ML") ("Tools/Domain/domain_syntax.ML") ("Tools/Domain/domain_axioms.ML") @@ -86,7 +87,10 @@ lemma rep_defined_iff: "(rep\x = \) = (x = \)" by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms) -lemma (in iso) compact_abs_rev: "compact (abs\x) \ compact x" +lemma casedist_rule: "rep\x = \ \ P \ x = \ \ P" + by (simp add: rep_defined_iff) + +lemma compact_abs_rev: "compact (abs\x) \ compact x" proof (unfold compact_def) assume "adm (\y. \ abs\x \ y)" with cont_Rep_CFun2 @@ -228,11 +232,51 @@ lemmas con_eq_iff_rules = sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules +lemmas sel_strict_rules = + cfcomp2 sscase1 sfst_strict ssnd_strict fup1 + +lemma sel_app_extra_rules: + "sscase\ID\\\(sinr\x) = \" + "sscase\ID\\\(sinl\x) = x" + "sscase\\\ID\(sinl\x) = \" + "sscase\\\ID\(sinr\x) = x" + "fup\ID\(up\x) = x" +by (cases "x = \", simp, simp)+ + +lemmas sel_app_rules = + sel_strict_rules sel_app_extra_rules + ssnd_spair sfst_spair up_defined spair_defined + +lemmas sel_defined_iff_rules = + cfcomp2 sfst_defined_iff ssnd_defined_iff + +lemmas take_con_rules = + ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict + sprod_map_spair' sprod_map_strict u_map_up u_map_strict + +lemma lub_ID_take_lemma: + assumes "chain t" and "(\n. t n) = ID" + assumes "\n. t n\x = t n\y" shows "x = y" +proof - + have "(\n. t n\x) = (\n. t n\y)" + using assms(3) by simp + then have "(\n. t n)\x = (\n. t n)\y" + using assms(1) by (simp add: lub_distribs) + then show "x = y" + using assms(2) by simp +qed + +lemma lub_ID_reach: + assumes "chain t" and "(\n. t n) = ID" + shows "(\n. t n\x) = x" +using assms by (simp add: lub_distribs) + use "Tools/cont_consts.ML" use "Tools/cont_proc.ML" use "Tools/Domain/domain_library.ML" use "Tools/Domain/domain_syntax.ML" use "Tools/Domain/domain_axioms.ML" +use "Tools/Domain/domain_constructors.ML" use "Tools/Domain/domain_theorems.ML" use "Tools/Domain/domain_extender.ML" diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Fixrec.thy Tue Mar 02 15:39:15 2010 +0100 @@ -265,7 +265,7 @@ *} translations - "x" <= "_match Fixrec.return (_variable x)" + "x" <= "_match (CONST Fixrec.return) (_variable x)" subsection {* Pattern combinators for data constructors *} diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/HOLCF.thy Tue Mar 02 15:39:15 2010 +0100 @@ -6,8 +6,10 @@ theory HOLCF imports - Domain ConvexPD Algebraic Universal Sum_Cpo Main - Representable + Main + Domain + Powerdomains + Sum_Cpo uses "holcf_logic.ML" "Tools/adm_tac.ML" diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 02 15:39:15 2010 +0100 @@ -902,15 +902,10 @@ shows "s1< (\i. X i) = (\i. Y i)" by (simp only: expand_fun_eq [symmetric]) +lemma lub_eq: + "(\i. X i = Y i) \ (\i. X i) = (\i. Y i)" + by simp + text {* more results about mono and = of lubs of chains *} lemma lub_mono2: diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Powerdomains.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Powerdomains.thy Tue Mar 02 15:39:15 2010 +0100 @@ -0,0 +1,313 @@ +(* Title: HOLCF/Powerdomains.thy + Author: Brian Huffman +*) + +header {* Powerdomains *} + +theory Powerdomains +imports Representable ConvexPD +begin + +subsection {* Powerdomains are representable *} + +text "Upper powerdomain of a representable type is representable." + +instantiation upper_pd :: (rep) rep +begin + +definition emb_upper_pd_def: "emb = udom_emb oo upper_map\emb" +definition prj_upper_pd_def: "prj = upper_map\prj oo udom_prj" + +instance + apply (intro_classes, unfold emb_upper_pd_def prj_upper_pd_def) + apply (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj ep_pair_udom) +done + +end + +text "Lower powerdomain of a representable type is representable." + +instantiation lower_pd :: (rep) rep +begin + +definition emb_lower_pd_def: "emb = udom_emb oo lower_map\emb" +definition prj_lower_pd_def: "prj = lower_map\prj oo udom_prj" + +instance + apply (intro_classes, unfold emb_lower_pd_def prj_lower_pd_def) + apply (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj ep_pair_udom) +done + +end + +text "Convex powerdomain of a representable type is representable." + +instantiation convex_pd :: (rep) rep +begin + +definition emb_convex_pd_def: "emb = udom_emb oo convex_map\emb" +definition prj_convex_pd_def: "prj = convex_map\prj oo udom_prj" + +instance + apply (intro_classes, unfold emb_convex_pd_def prj_convex_pd_def) + apply (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj ep_pair_udom) +done + +end + +subsection {* Finite deflation lemmas *} + +text "TODO: move these lemmas somewhere else" + +lemma finite_compact_range_imp_finite_range: + fixes d :: "'a::profinite \ 'b::cpo" + assumes "finite ((\x. d\x) ` {x. compact x})" + shows "finite (range (\x. d\x))" +proof (rule finite_subset [OF _ prems]) + { + fix x :: 'a + have "range (\i. d\(approx i\x)) \ (\x. d\x) ` {x. compact x}" + by auto + hence "finite (range (\i. d\(approx i\x)))" + using prems by (rule finite_subset) + hence "finite_chain (\i. d\(approx i\x))" + by (simp add: finite_range_imp_finch) + hence "\i. (\i. d\(approx i\x)) = d\(approx i\x)" + by (simp add: finite_chain_def maxinch_is_thelub) + hence "\i. d\x = d\(approx i\x)" + by (simp add: lub_distribs) + hence "d\x \ (\x. d\x) ` {x. compact x}" + by auto + } + thus "range (\x. d\x) \ (\x. d\x) ` {x. compact x}" + by clarsimp +qed + +lemma finite_deflation_upper_map: + assumes "finite_deflation d" shows "finite_deflation (upper_map\d)" +proof (intro finite_deflation.intro finite_deflation_axioms.intro) + interpret d: finite_deflation d by fact + have "deflation d" by fact + thus "deflation (upper_map\d)" by (rule deflation_upper_map) + have "finite (range (\x. d\x))" by (rule d.finite_range) + hence "finite (Rep_compact_basis -` range (\x. d\x))" + by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) + hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp + hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" + by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) + hence "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp + hence "finite ((\xs. upper_map\d\xs) ` range upper_principal)" + apply (rule finite_subset [COMP swap_prems_rl]) + apply (clarsimp, rename_tac t) + apply (induct_tac t rule: pd_basis_induct) + apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit) + apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDUnit) + apply (rule image_eqI) + apply (erule sym) + apply simp + apply (rule exI) + apply (rule Abs_compact_basis_inverse [symmetric]) + apply (simp add: d.compact) + apply (simp only: upper_plus_principal [symmetric] upper_map_plus) + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDPlus) + done + moreover have "{xs::'a upper_pd. compact xs} = range upper_principal" + by (auto dest: upper_pd.compact_imp_principal) + ultimately have "finite ((\xs. upper_map\d\xs) ` {xs::'a upper_pd. compact xs})" + by simp + hence "finite (range (\xs. upper_map\d\xs))" + by (rule finite_compact_range_imp_finite_range) + thus "finite {xs. upper_map\d\xs = xs}" + by (rule finite_range_imp_finite_fixes) +qed + +lemma finite_deflation_lower_map: + assumes "finite_deflation d" shows "finite_deflation (lower_map\d)" +proof (intro finite_deflation.intro finite_deflation_axioms.intro) + interpret d: finite_deflation d by fact + have "deflation d" by fact + thus "deflation (lower_map\d)" by (rule deflation_lower_map) + have "finite (range (\x. d\x))" by (rule d.finite_range) + hence "finite (Rep_compact_basis -` range (\x. d\x))" + by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) + hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp + hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" + by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) + hence "finite (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp + hence "finite ((\xs. lower_map\d\xs) ` range lower_principal)" + apply (rule finite_subset [COMP swap_prems_rl]) + apply (clarsimp, rename_tac t) + apply (induct_tac t rule: pd_basis_induct) + apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit) + apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDUnit) + apply (rule image_eqI) + apply (erule sym) + apply simp + apply (rule exI) + apply (rule Abs_compact_basis_inverse [symmetric]) + apply (simp add: d.compact) + apply (simp only: lower_plus_principal [symmetric] lower_map_plus) + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDPlus) + done + moreover have "{xs::'a lower_pd. compact xs} = range lower_principal" + by (auto dest: lower_pd.compact_imp_principal) + ultimately have "finite ((\xs. lower_map\d\xs) ` {xs::'a lower_pd. compact xs})" + by simp + hence "finite (range (\xs. lower_map\d\xs))" + by (rule finite_compact_range_imp_finite_range) + thus "finite {xs. lower_map\d\xs = xs}" + by (rule finite_range_imp_finite_fixes) +qed + +lemma finite_deflation_convex_map: + assumes "finite_deflation d" shows "finite_deflation (convex_map\d)" +proof (intro finite_deflation.intro finite_deflation_axioms.intro) + interpret d: finite_deflation d by fact + have "deflation d" by fact + thus "deflation (convex_map\d)" by (rule deflation_convex_map) + have "finite (range (\x. d\x))" by (rule d.finite_range) + hence "finite (Rep_compact_basis -` range (\x. d\x))" + by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) + hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp + hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" + by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) + hence "finite (convex_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp + hence "finite ((\xs. convex_map\d\xs) ` range convex_principal)" + apply (rule finite_subset [COMP swap_prems_rl]) + apply (clarsimp, rename_tac t) + apply (induct_tac t rule: pd_basis_induct) + apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit) + apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDUnit) + apply (rule image_eqI) + apply (erule sym) + apply simp + apply (rule exI) + apply (rule Abs_compact_basis_inverse [symmetric]) + apply (simp add: d.compact) + apply (simp only: convex_plus_principal [symmetric] convex_map_plus) + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDPlus) + done + moreover have "{xs::'a convex_pd. compact xs} = range convex_principal" + by (auto dest: convex_pd.compact_imp_principal) + ultimately have "finite ((\xs. convex_map\d\xs) ` {xs::'a convex_pd. compact xs})" + by simp + hence "finite (range (\xs. convex_map\d\xs))" + by (rule finite_compact_range_imp_finite_range) + thus "finite {xs. convex_map\d\xs = xs}" + by (rule finite_range_imp_finite_fixes) +qed + +subsection {* Deflation combinators *} + +definition "upper_defl = TypeRep_fun1 upper_map" +definition "lower_defl = TypeRep_fun1 lower_map" +definition "convex_defl = TypeRep_fun1 convex_map" + +lemma cast_upper_defl: + "cast\(upper_defl\A) = udom_emb oo upper_map\(cast\A) oo udom_prj" +unfolding upper_defl_def +apply (rule cast_TypeRep_fun1) +apply (erule finite_deflation_upper_map) +done + +lemma cast_lower_defl: + "cast\(lower_defl\A) = udom_emb oo lower_map\(cast\A) oo udom_prj" +unfolding lower_defl_def +apply (rule cast_TypeRep_fun1) +apply (erule finite_deflation_lower_map) +done + +lemma cast_convex_defl: + "cast\(convex_defl\A) = udom_emb oo convex_map\(cast\A) oo udom_prj" +unfolding convex_defl_def +apply (rule cast_TypeRep_fun1) +apply (erule finite_deflation_convex_map) +done + +lemma REP_upper: "REP('a upper_pd) = upper_defl\REP('a)" +apply (rule cast_eq_imp_eq, rule ext_cfun) +apply (simp add: cast_REP cast_upper_defl) +apply (simp add: prj_upper_pd_def) +apply (simp add: emb_upper_pd_def) +apply (simp add: upper_map_map cfcomp1) +done + +lemma REP_lower: "REP('a lower_pd) = lower_defl\REP('a)" +apply (rule cast_eq_imp_eq, rule ext_cfun) +apply (simp add: cast_REP cast_lower_defl) +apply (simp add: prj_lower_pd_def) +apply (simp add: emb_lower_pd_def) +apply (simp add: lower_map_map cfcomp1) +done + +lemma REP_convex: "REP('a convex_pd) = convex_defl\REP('a)" +apply (rule cast_eq_imp_eq, rule ext_cfun) +apply (simp add: cast_REP cast_convex_defl) +apply (simp add: prj_convex_pd_def) +apply (simp add: emb_convex_pd_def) +apply (simp add: convex_map_map cfcomp1) +done + +lemma isodefl_upper: + "isodefl d t \ isodefl (upper_map\d) (upper_defl\t)" +apply (rule isodeflI) +apply (simp add: cast_upper_defl cast_isodefl) +apply (simp add: emb_upper_pd_def prj_upper_pd_def) +apply (simp add: upper_map_map) +done + +lemma isodefl_lower: + "isodefl d t \ isodefl (lower_map\d) (lower_defl\t)" +apply (rule isodeflI) +apply (simp add: cast_lower_defl cast_isodefl) +apply (simp add: emb_lower_pd_def prj_lower_pd_def) +apply (simp add: lower_map_map) +done + +lemma isodefl_convex: + "isodefl d t \ isodefl (convex_map\d) (convex_defl\t)" +apply (rule isodeflI) +apply (simp add: cast_convex_defl cast_isodefl) +apply (simp add: emb_convex_pd_def prj_convex_pd_def) +apply (simp add: convex_map_map) +done + +subsection {* Domain package setup for powerdomains *} + +setup {* + fold Domain_Isomorphism.add_type_constructor + [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}, + @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}, + @{thm deflation_upper_map}), + + (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}, + @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}, + @{thm deflation_lower_map}), + + (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map}, + @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID}, + @{thm deflation_convex_map})] +*} + +end diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Representable.thy Tue Mar 02 15:39:15 2010 +0100 @@ -5,9 +5,10 @@ header {* Representable Types *} theory Representable -imports Algebraic Universal Ssum Sprod One ConvexPD Fixrec +imports Algebraic Universal Ssum Sprod One Fixrec uses ("Tools/repdef.ML") + ("Tools/holcf_library.ML") ("Tools/Domain/domain_isomorphism.ML") begin @@ -179,6 +180,33 @@ shows "abs\(rep\x) = x" unfolding abs_def rep_def by (simp add: REP [symmetric]) +lemma deflation_abs_rep: + fixes abs and rep and d + assumes abs_iso: "\x. rep\(abs\x) = x" + assumes rep_iso: "\y. abs\(rep\y) = y" + shows "deflation d \ deflation (abs oo d oo rep)" +by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms) + +lemma deflation_chain_min: + assumes chain: "chain d" + assumes defl: "\i. deflation (d i)" + shows "d i\(d j\x) = d (min i j)\x" +proof (rule linorder_le_cases) + assume "i \ j" + with chain have "d i \ d j" by (rule chain_mono) + then have "d i\(d j\x) = d i\x" + by (rule deflation_below_comp1 [OF defl defl]) + moreover from `i \ j` have "min i j = i" by simp + ultimately show ?thesis by simp +next + assume "j \ i" + with chain have "d j \ d i" by (rule chain_mono) + then have "d i\(d j\x) = d j\x" + by (rule deflation_below_comp2 [OF defl defl]) + moreover from `j \ i` have "min i j = j" by simp + ultimately show ?thesis by simp +qed + subsection {* Proving a subtype is representable *} @@ -460,214 +488,6 @@ end -text "Upper powerdomain of a representable type is representable." - -instantiation upper_pd :: (rep) rep -begin - -definition emb_upper_pd_def: "emb = udom_emb oo upper_map\emb" -definition prj_upper_pd_def: "prj = upper_map\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_upper_pd_def prj_upper_pd_def) - apply (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj ep_pair_udom) -done - -end - -text "Lower powerdomain of a representable type is representable." - -instantiation lower_pd :: (rep) rep -begin - -definition emb_lower_pd_def: "emb = udom_emb oo lower_map\emb" -definition prj_lower_pd_def: "prj = lower_map\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_lower_pd_def prj_lower_pd_def) - apply (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj ep_pair_udom) -done - -end - -text "Convex powerdomain of a representable type is representable." - -instantiation convex_pd :: (rep) rep -begin - -definition emb_convex_pd_def: "emb = udom_emb oo convex_map\emb" -definition prj_convex_pd_def: "prj = convex_map\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_convex_pd_def prj_convex_pd_def) - apply (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj ep_pair_udom) -done - -end - -subsection {* Finite deflation lemmas *} - -text "TODO: move these lemmas somewhere else" - -lemma finite_compact_range_imp_finite_range: - fixes d :: "'a::profinite \ 'b::cpo" - assumes "finite ((\x. d\x) ` {x. compact x})" - shows "finite (range (\x. d\x))" -proof (rule finite_subset [OF _ prems]) - { - fix x :: 'a - have "range (\i. d\(approx i\x)) \ (\x. d\x) ` {x. compact x}" - by auto - hence "finite (range (\i. d\(approx i\x)))" - using prems by (rule finite_subset) - hence "finite_chain (\i. d\(approx i\x))" - by (simp add: finite_range_imp_finch) - hence "\i. (\i. d\(approx i\x)) = d\(approx i\x)" - by (simp add: finite_chain_def maxinch_is_thelub) - hence "\i. d\x = d\(approx i\x)" - by (simp add: lub_distribs) - hence "d\x \ (\x. d\x) ` {x. compact x}" - by auto - } - thus "range (\x. d\x) \ (\x. d\x) ` {x. compact x}" - by clarsimp -qed - -lemma finite_deflation_upper_map: - assumes "finite_deflation d" shows "finite_deflation (upper_map\d)" -proof (intro finite_deflation.intro finite_deflation_axioms.intro) - interpret d: finite_deflation d by fact - have "deflation d" by fact - thus "deflation (upper_map\d)" by (rule deflation_upper_map) - have "finite (range (\x. d\x))" by (rule d.finite_range) - hence "finite (Rep_compact_basis -` range (\x. d\x))" - by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) - hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp - hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" - by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) - hence "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp - hence "finite ((\xs. upper_map\d\xs) ` range upper_principal)" - apply (rule finite_subset [COMP swap_prems_rl]) - apply (clarsimp, rename_tac t) - apply (induct_tac t rule: pd_basis_induct) - apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit) - apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDUnit) - apply (rule image_eqI) - apply (erule sym) - apply simp - apply (rule exI) - apply (rule Abs_compact_basis_inverse [symmetric]) - apply (simp add: d.compact) - apply (simp only: upper_plus_principal [symmetric] upper_map_plus) - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDPlus) - done - moreover have "{xs::'a upper_pd. compact xs} = range upper_principal" - by (auto dest: upper_pd.compact_imp_principal) - ultimately have "finite ((\xs. upper_map\d\xs) ` {xs::'a upper_pd. compact xs})" - by simp - hence "finite (range (\xs. upper_map\d\xs))" - by (rule finite_compact_range_imp_finite_range) - thus "finite {xs. upper_map\d\xs = xs}" - by (rule finite_range_imp_finite_fixes) -qed - -lemma finite_deflation_lower_map: - assumes "finite_deflation d" shows "finite_deflation (lower_map\d)" -proof (intro finite_deflation.intro finite_deflation_axioms.intro) - interpret d: finite_deflation d by fact - have "deflation d" by fact - thus "deflation (lower_map\d)" by (rule deflation_lower_map) - have "finite (range (\x. d\x))" by (rule d.finite_range) - hence "finite (Rep_compact_basis -` range (\x. d\x))" - by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) - hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp - hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" - by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) - hence "finite (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp - hence "finite ((\xs. lower_map\d\xs) ` range lower_principal)" - apply (rule finite_subset [COMP swap_prems_rl]) - apply (clarsimp, rename_tac t) - apply (induct_tac t rule: pd_basis_induct) - apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit) - apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDUnit) - apply (rule image_eqI) - apply (erule sym) - apply simp - apply (rule exI) - apply (rule Abs_compact_basis_inverse [symmetric]) - apply (simp add: d.compact) - apply (simp only: lower_plus_principal [symmetric] lower_map_plus) - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDPlus) - done - moreover have "{xs::'a lower_pd. compact xs} = range lower_principal" - by (auto dest: lower_pd.compact_imp_principal) - ultimately have "finite ((\xs. lower_map\d\xs) ` {xs::'a lower_pd. compact xs})" - by simp - hence "finite (range (\xs. lower_map\d\xs))" - by (rule finite_compact_range_imp_finite_range) - thus "finite {xs. lower_map\d\xs = xs}" - by (rule finite_range_imp_finite_fixes) -qed - -lemma finite_deflation_convex_map: - assumes "finite_deflation d" shows "finite_deflation (convex_map\d)" -proof (intro finite_deflation.intro finite_deflation_axioms.intro) - interpret d: finite_deflation d by fact - have "deflation d" by fact - thus "deflation (convex_map\d)" by (rule deflation_convex_map) - have "finite (range (\x. d\x))" by (rule d.finite_range) - hence "finite (Rep_compact_basis -` range (\x. d\x))" - by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) - hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp - hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" - by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) - hence "finite (convex_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp - hence "finite ((\xs. convex_map\d\xs) ` range convex_principal)" - apply (rule finite_subset [COMP swap_prems_rl]) - apply (clarsimp, rename_tac t) - apply (induct_tac t rule: pd_basis_induct) - apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit) - apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDUnit) - apply (rule image_eqI) - apply (erule sym) - apply simp - apply (rule exI) - apply (rule Abs_compact_basis_inverse [symmetric]) - apply (simp add: d.compact) - apply (simp only: convex_plus_principal [symmetric] convex_map_plus) - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDPlus) - done - moreover have "{xs::'a convex_pd. compact xs} = range convex_principal" - by (auto dest: convex_pd.compact_imp_principal) - ultimately have "finite ((\xs. convex_map\d\xs) ` {xs::'a convex_pd. compact xs})" - by simp - hence "finite (range (\xs. convex_map\d\xs))" - by (rule finite_compact_range_imp_finite_range) - thus "finite {xs. convex_map\d\xs = xs}" - by (rule finite_range_imp_finite_fixes) -qed - subsection {* Type combinators *} definition @@ -697,9 +517,6 @@ definition "sprod_defl = TypeRep_fun2 sprod_map" definition "cprod_defl = TypeRep_fun2 cprod_map" definition "u_defl = TypeRep_fun1 u_map" -definition "upper_defl = TypeRep_fun1 upper_map" -definition "lower_defl = TypeRep_fun1 lower_map" -definition "convex_defl = TypeRep_fun1 convex_map" lemma Rep_fin_defl_mono: "a \ b \ Rep_fin_defl a \ Rep_fin_defl b" unfolding below_fin_defl_def . @@ -783,27 +600,6 @@ apply (erule finite_deflation_u_map) done -lemma cast_upper_defl: - "cast\(upper_defl\A) = udom_emb oo upper_map\(cast\A) oo udom_prj" -unfolding upper_defl_def -apply (rule cast_TypeRep_fun1) -apply (erule finite_deflation_upper_map) -done - -lemma cast_lower_defl: - "cast\(lower_defl\A) = udom_emb oo lower_map\(cast\A) oo udom_prj" -unfolding lower_defl_def -apply (rule cast_TypeRep_fun1) -apply (erule finite_deflation_lower_map) -done - -lemma cast_convex_defl: - "cast\(convex_defl\A) = udom_emb oo convex_map\(cast\A) oo udom_prj" -unfolding convex_defl_def -apply (rule cast_TypeRep_fun1) -apply (erule finite_deflation_convex_map) -done - text {* REP of type constructor = type combinator *} lemma REP_cfun: "REP('a \ 'b) = cfun_defl\REP('a)\REP('b)" @@ -814,7 +610,6 @@ apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom]) done - lemma REP_ssum: "REP('a \ 'b) = ssum_defl\REP('a)\REP('b)" apply (rule cast_eq_imp_eq, rule ext_cfun) apply (simp add: cast_REP cast_ssum_defl) @@ -847,39 +642,12 @@ apply (simp add: u_map_map cfcomp1) done -lemma REP_upper: "REP('a upper_pd) = upper_defl\REP('a)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_upper_defl) -apply (simp add: prj_upper_pd_def) -apply (simp add: emb_upper_pd_def) -apply (simp add: upper_map_map cfcomp1) -done - -lemma REP_lower: "REP('a lower_pd) = lower_defl\REP('a)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_lower_defl) -apply (simp add: prj_lower_pd_def) -apply (simp add: emb_lower_pd_def) -apply (simp add: lower_map_map cfcomp1) -done - -lemma REP_convex: "REP('a convex_pd) = convex_defl\REP('a)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_convex_defl) -apply (simp add: prj_convex_pd_def) -apply (simp add: emb_convex_pd_def) -apply (simp add: convex_map_map cfcomp1) -done - lemmas REP_simps = REP_cfun REP_ssum REP_sprod REP_cprod REP_up - REP_upper - REP_lower - REP_convex subsection {* Isomorphic deflations *} @@ -1007,59 +775,27 @@ apply (simp add: u_map_map) done -lemma isodefl_upper: - "isodefl d t \ isodefl (upper_map\d) (upper_defl\t)" -apply (rule isodeflI) -apply (simp add: cast_upper_defl cast_isodefl) -apply (simp add: emb_upper_pd_def prj_upper_pd_def) -apply (simp add: upper_map_map) -done - -lemma isodefl_lower: - "isodefl d t \ isodefl (lower_map\d) (lower_defl\t)" -apply (rule isodeflI) -apply (simp add: cast_lower_defl cast_isodefl) -apply (simp add: emb_lower_pd_def prj_lower_pd_def) -apply (simp add: lower_map_map) -done - -lemma isodefl_convex: - "isodefl d t \ isodefl (convex_map\d) (convex_defl\t)" -apply (rule isodeflI) -apply (simp add: cast_convex_defl cast_isodefl) -apply (simp add: emb_convex_pd_def prj_convex_pd_def) -apply (simp add: convex_map_map) -done - subsection {* Constructing Domain Isomorphisms *} +use "Tools/holcf_library.ML" use "Tools/Domain/domain_isomorphism.ML" setup {* fold Domain_Isomorphism.add_type_constructor - [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map}, - @{thm REP_cfun}, @{thm isodefl_cfun}, @{thm cfun_map_ID}), - - (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, - @{thm REP_ssum}, @{thm isodefl_ssum}, @{thm ssum_map_ID}), + [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun}, + @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}), - (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, - @{thm REP_sprod}, @{thm isodefl_sprod}, @{thm sprod_map_ID}), - - (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, - @{thm REP_cprod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}), + (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum}, + @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}), - (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, - @{thm REP_up}, @{thm isodefl_u}, @{thm u_map_ID}), - - (@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}, - @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}), + (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod}, + @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}), - (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}, - @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}), + (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod}, + @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}), - (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map}, - @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID})] + (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up}, + @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})] *} end diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Sprod.thy Tue Mar 02 15:39:15 2010 +0100 @@ -245,6 +245,10 @@ "x \ \ \ y \ \ \ sprod_map\f\g\(:x, y:) = (:f\x, g\y:)" by (simp add: sprod_map_def) +lemma sprod_map_spair': + "f\\ = \ \ g\\ = \ \ sprod_map\f\g\(:x, y:) = (:f\x, g\y:)" +by (cases "x = \ \ y = \") auto + lemma sprod_map_ID: "sprod_map\ID\ID = ID" unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun) diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Ssum.thy --- a/src/HOLCF/Ssum.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Ssum.thy Tue Mar 02 15:39:15 2010 +0100 @@ -226,6 +226,12 @@ lemma ssum_map_sinr [simp]: "x \ \ \ ssum_map\f\g\(sinr\x) = sinr\(g\x)" unfolding ssum_map_def by simp +lemma ssum_map_sinl': "f\\ = \ \ ssum_map\f\g\(sinl\x) = sinl\(f\x)" +by (cases "x = \") simp_all + +lemma ssum_map_sinr': "g\\ = \ \ ssum_map\f\g\(sinr\x) = sinr\(g\x)" +by (cases "x = \") simp_all + lemma ssum_map_ID: "ssum_map\ID\ID = ID" unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun) diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 15:39:15 2010 +0100 @@ -11,12 +11,14 @@ val calc_axioms : bool -> string Symtab.table -> - string -> Domain_Library.eq list -> int -> Domain_Library.eq -> + Domain_Library.eq list -> int -> Domain_Library.eq -> string * (string * term) list * (string * term) list val add_axioms : bool -> - bstring -> Domain_Library.eq list -> theory -> theory + ((string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list) list -> + Domain_Library.eq list -> theory -> theory end; @@ -49,7 +51,6 @@ fun calc_axioms (definitional : bool) (map_tab : string Symtab.table) - (comp_dname : string) (eqs : eq list) (n : int) (eqn as ((dname,_),cons) : eq) @@ -67,82 +68,8 @@ val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); - val when_def = ("when_def",%%:(dname^"_when") == - List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => - Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); - - val copy_def = - let fun r i = proj (Bound 0) eqs i; - in - ("copy_def", %%:(dname^"_copy") == /\ "f" - (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep)) - end; - -(* -- definitions concerning the constructors, discriminators and selectors - *) - - fun con_def m n (_,args) = let - fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x)); - fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); - fun inj y 1 _ = y - | inj y _ 0 = mk_sinl y - | inj y i j = mk_sinr (inj y (i-1) (j-1)); - in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end; - - val con_defs = mapn (fn n => fn (con, _, args) => - (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; - - val dis_defs = let - fun ddef (con,_,_) = (dis_name con ^"_def",%%:(dis_name con) == - list_ccomb(%%:(dname^"_when"),map - (fn (con',_,args) => (List.foldr /\# - (if con'=con then TT else FF) args)) cons)) - in map ddef cons end; - - val mat_defs = - let - fun mdef (con, _, _) = - let - val k = Bound 0 - val x = Bound 1 - fun one_con (con', _, args') = - if con'=con then k else List.foldr /\# mk_fail args' - val w = list_ccomb(%%:(dname^"_when"), map one_con cons) - val rhs = /\ "x" (/\ "k" (w ` x)) - in (mat_name con ^"_def", %%:(mat_name con) == rhs) end - in map mdef cons end; - - val pat_defs = - let - fun pdef (con, _, args) = - let - val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - val xs = map (bound_arg args) args; - val r = Bound (length args); - val rhs = case args of [] => mk_return HOLogic.unit - | _ => mk_ctuple_pat ps ` mk_ctuple xs; - fun one_con (con', _, args') = List.foldr /\# (if con'=con then rhs else mk_fail) args'; - in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == - list_ccomb(%%:(dname^"_when"), map one_con cons)) - end - in map pdef cons end; - - val sel_defs = let - fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == - list_ccomb(%%:(dname^"_when"),map - (fn (con', _, args) => if con'<>con then UU else - List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); - in map_filter I (maps (fn (con, _, args) => mapn (sdef con) 1 args) cons) end; - - (* ----- axiom and definitions concerning induction ------------------------- *) - val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n - `%x_name === %:x_name)); - val take_def = - ("take_def", - %%:(dname^"_take") == - mk_lam("n",proj - (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); val finite_def = ("finite_def", %%:(dname^"_finite") == @@ -150,10 +77,8 @@ mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); in (dnam, - (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]), - (if definitional then [when_def] else [when_def, copy_def]) @ - con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ - [take_def, finite_def]) + (if definitional then [] else [abs_iso_ax, rep_iso_ax]), + [finite_def]) end; (* let (calc_axioms) *) @@ -173,81 +98,75 @@ fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; -fun add_matchers (((dname,_),cons) : eq) thy = - let - val con_names = map first cons; - val mat_names = map mat_name con_names; - fun qualify n = Sign.full_name thy (Binding.name n); - val ms = map qualify con_names ~~ map qualify mat_names; - in Fixrec.add_matchers ms thy end; - -fun add_axioms definitional comp_dnam (eqs : eq list) thy' = +fun add_axioms definitional eqs' (eqs : eq list) thy' = let - val comp_dname = Sign.full_bname thy' comp_dnam; val dnames = map (fst o fst) eqs; val x_name = idx_name dnames "x"; - fun copy_app dname = %%:(dname^"_copy")`Bound 0; - val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == - /\ "f"(mk_ctuple (map copy_app dnames))); - - fun one_con (con, _, args) = - let - val nonrec_args = filter_out is_rec args; - val rec_args = filter is_rec args; - val recs_cnt = length rec_args; - val allargs = nonrec_args @ rec_args - @ map (upd_vname (fn s=> s^"'")) rec_args; - val allvns = map vname allargs; - fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; - val vns1 = map (vname_arg "" ) args; - val vns2 = map (vname_arg "'") args; - val allargs_cnt = length nonrec_args + 2*recs_cnt; - val rec_idxs = (recs_cnt-1) downto 0; - val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) - (allargs~~((allargs_cnt-1) downto 0))); - fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ - Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); - val capps = - List.foldr - mk_conj - (mk_conj( - Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), - Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) - (mapn rel_app 1 rec_args); - in - List.foldr - mk_ex - (Library.foldr mk_conj - (map (defined o Bound) nonlazy_idxs,capps)) allvns - end; - fun one_comp n (_,cons) = - mk_all (x_name(n+1), - mk_all (x_name(n+1)^"'", - mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0, - foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) - ::map one_con cons)))); - val bisim_def = - ("bisim_def", %%:(comp_dname^"_bisim") == - mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); fun add_one (dnam, axs, dfs) = Sign.add_path dnam - #> add_defs_infer dfs #> add_axioms_infer axs #> Sign.parent_path; val map_tab = Domain_Isomorphism.get_map_tab thy'; + val axs = mapn (calc_axioms definitional map_tab eqs) 0 eqs; + val thy = thy' |> fold add_one axs; - val thy = thy' - |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs); + fun get_iso_info ((dname, tyvars), cons') = + let + fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t + fun prod (_,args,_) = + case args of [] => oneT + | _ => foldr1 mk_sprodT (map opt_lazy args); + val ax_abs_iso = PureThy.get_thm thy (dname ^ ".abs_iso"); + val ax_rep_iso = PureThy.get_thm thy (dname ^ ".rep_iso"); + val lhsT = Type(dname,tyvars); + val rhsT = foldr1 mk_ssumT (map prod cons'); + val rep_const = Const(dname^"_rep", lhsT ->> rhsT); + val abs_const = Const(dname^"_abs", rhsT ->> lhsT); + in + { + absT = lhsT, + repT = rhsT, + abs_const = abs_const, + rep_const = rep_const, + abs_inverse = ax_abs_iso, + rep_inverse = ax_rep_iso + } + end; + val dom_binds = map (Binding.name o Long_Name.base_name) dnames; + val thy = + if definitional then thy + else snd (Domain_Isomorphism.define_take_functions + (dom_binds ~~ map get_iso_info eqs') thy); - val use_copy_def = length eqs>1 andalso not definitional; + fun add_one' (dnam, axs, dfs) = + Sign.add_path dnam + #> add_defs_infer dfs + #> Sign.parent_path; + val thy = fold add_one' axs thy; + + (* declare lub_take axioms *) + local + fun ax_lub_take dname = + let + val dnam : string = Long_Name.base_name dname; + val take_const = %%:(dname^"_take"); + val lub = %%: @{const_name lub}; + val image = %%: @{const_name image}; + val UNIV = @{term "UNIV :: nat set"}; + val lhs = lub $ (image $ take_const $ UNIV); + val ax = mk_trp (lhs === ID); + in + add_one (dnam, [("lub_take", ax)], []) + end + in + val thy = + if definitional then thy + else fold ax_lub_take dnames thy + end; in thy - |> Sign.add_path comp_dnam - |> add_defs_infer (bisim_def::(if use_copy_def then [copy_def] else [])) - |> Sign.parent_path - |> fold add_matchers eqs end; (* let (add_axioms) *) end; (* struct *) diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Tools/Domain/domain_constructors.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Tue Mar 02 15:39:15 2010 +0100 @@ -0,0 +1,1123 @@ +(* Title: HOLCF/Tools/domain/domain_constructors.ML + Author: Brian Huffman + +Defines constructor functions for a given domain isomorphism +and proves related theorems. +*) + +signature DOMAIN_CONSTRUCTORS = +sig + val add_domain_constructors : + string + -> (binding * (bool * binding option * typ) list * mixfix) list + -> Domain_Isomorphism.iso_info + -> theory + -> { con_consts : term list, + con_betas : thm list, + exhaust : thm, + casedist : thm, + con_compacts : thm list, + con_rews : thm list, + inverts : thm list, + injects : thm list, + dist_les : thm list, + dist_eqs : thm list, + cases : thm list, + sel_rews : thm list, + dis_rews : thm list, + match_rews : thm list, + pat_rews : thm list + } * theory; +end; + + +structure Domain_Constructors :> DOMAIN_CONSTRUCTORS = +struct + +open HOLCF_Library; +infixr 6 ->>; +infix -->>; + +(************************** miscellaneous functions ***************************) + +val simple_ss = + HOL_basic_ss addsimps simp_thms; + +val beta_ss = + HOL_basic_ss + addsimps simp_thms + addsimps [@{thm beta_cfun}] + addsimprocs [@{simproc cont_proc}]; + +fun define_consts + (specs : (binding * term * mixfix) list) + (thy : theory) + : (term list * thm list) * theory = + let + fun mk_decl (b, t, mx) = (b, fastype_of t, mx); + val decls = map mk_decl specs; + val thy = Cont_Consts.add_consts decls thy; + fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T); + val consts = map mk_const decls; + fun mk_def c (b, t, mx) = + (Binding.suffix_name "_def" b, Logic.mk_equals (c, t)); + val defs = map2 mk_def consts specs; + val (def_thms, thy) = + PureThy.add_defs false (map Thm.no_attributes defs) thy; + in + ((consts, def_thms), thy) + end; + +fun prove + (thy : theory) + (defs : thm list) + (goal : term) + (tacs : {prems: thm list, context: Proof.context} -> tactic list) + : thm = + let + fun tac {prems, context} = + rewrite_goals_tac defs THEN + EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context}) + in + Goal.prove_global thy [] [] goal tac + end; + +fun get_vars_avoiding + (taken : string list) + (args : (bool * typ) list) + : (term list * term list) = + let + val Ts = map snd args; + val ns = Name.variant_list taken (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); + in + (vs, nonlazy) + end; + +fun get_vars args = get_vars_avoiding [] args; + +(************** generating beta reduction rules from definitions **************) + +local + fun arglist (Const _ $ Abs (s, T, t)) = + let + val arg = Free (s, T); + val (args, body) = arglist (subst_bound (arg, t)); + in (arg :: args, body) end + | arglist t = ([], t); +in + fun beta_of_def thy def_thm = + let + val (con, lam) = Logic.dest_equals (concl_of def_thm); + val (args, rhs) = arglist lam; + val lhs = list_ccomb (con, args); + val goal = mk_equals (lhs, rhs); + val cs = ContProc.cont_thms lam; + val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs; + in + prove thy (def_thm::betas) goal (K [rtac reflexive_thm 1]) + end; +end; + +(******************************************************************************) +(************* definitions and theorems for constructor functions *************) +(******************************************************************************) + +fun add_constructors + (spec : (binding * (bool * typ) list * mixfix) list) + (abs_const : term) + (iso_locale : thm) + (thy : theory) + = + let + + (* get theorems about rep and abs *) + val abs_strict = iso_locale RS @{thm iso.abs_strict}; + + (* get types of type isomorphism *) + val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const); + + fun vars_of args = + let + val Ts = map snd args; + val ns = Datatype_Prop.make_tnames Ts; + in + map Free (ns ~~ Ts) + end; + + (* define constructor functions *) + val ((con_consts, con_defs), thy) = + let + fun one_arg (lazy, T) var = if lazy then mk_up var else var; + fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args)); + fun mk_abs t = abs_const ` t; + val rhss = map mk_abs (mk_sinjects (map one_con spec)); + fun mk_def (bind, args, mx) rhs = + (bind, big_lambdas (vars_of args) rhs, mx); + in + define_consts (map2 mk_def spec rhss) thy + end; + + (* prove beta reduction rules for constructors *) + val con_betas = map (beta_of_def thy) con_defs; + + (* replace bindings with terms in constructor spec *) + val spec' : (term * (bool * typ) list) list = + let fun one_con con (b, args, mx) = (con, args); + in map2 one_con con_consts spec end; + + (* prove exhaustiveness of constructors *) + local + fun arg2typ n (true, T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo}))) + | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo})); + fun args2typ n [] = (n, oneT) + | args2typ n [arg] = arg2typ n arg + | args2typ n (arg::args) = + let + val (n1, t1) = arg2typ n arg; + val (n2, t2) = args2typ n1 args + in (n2, mk_sprodT (t1, t2)) end; + fun cons2typ n [] = (n, oneT) + | cons2typ n [con] = args2typ n (snd con) + | cons2typ n (con::cons) = + let + val (n1, t1) = args2typ n (snd con); + val (n2, t2) = cons2typ n1 cons + in (n2, mk_ssumT (t1, t2)) end; + val ct = ctyp_of thy (snd (cons2typ 1 spec')); + val thm1 = instantiate' [SOME ct] [] @{thm exh_start}; + val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1; + val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2; + + val x = Free ("x", lhsT); + fun one_con (con, args) = + let + val (vs, nonlazy) = get_vars_avoiding ["x"] args; + val eqn = mk_eq (x, list_ccomb (con, vs)); + val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy); + in Library.foldr mk_ex (vs, conj) end; + val goal = mk_trp (foldr1 mk_disj (mk_undef x :: map one_con spec')); + (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *) + val tacs = [ + rtac (iso_locale RS @{thm iso.casedist_rule}) 1, + rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})], + rtac thm3 1]; + in + val exhaust = prove thy con_betas goal (K tacs); + val casedist = + (exhaust RS @{thm exh_casedist0}) + |> rewrite_rule @{thms exh_casedists} + |> Drule.export_without_context; + end; + + (* prove compactness rules for constructors *) + val con_compacts = + let + val rules = @{thms compact_sinl compact_sinr compact_spair + compact_up compact_ONE}; + val tacs = + [rtac (iso_locale RS @{thm iso.compact_abs}) 1, + REPEAT (resolve_tac rules 1 ORELSE atac 1)]; + fun con_compact (con, args) = + let + val vs = vars_of args; + val con_app = list_ccomb (con, vs); + val concl = mk_trp (mk_compact con_app); + val assms = map (mk_trp o mk_compact) vs; + val goal = Logic.list_implies (assms, concl); + in + prove thy con_betas goal (K tacs) + end; + in + map con_compact spec' + end; + + (* prove strictness rules for constructors *) + local + fun con_strict (con, args) = + let + val rules = abs_strict :: @{thms con_strict_rules}; + val (vs, nonlazy) = get_vars args; + fun one_strict v' = + let + val UU = mk_bottom (fastype_of v'); + val vs' = map (fn v => if v = v' then UU else v) vs; + val goal = mk_trp (mk_undef (list_ccomb (con, vs'))); + val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; + in prove thy con_betas goal (K tacs) end; + in map one_strict nonlazy end; + + fun con_defin (con, args) = + let + fun iff_disj (t, []) = HOLogic.mk_not t + | iff_disj (t, ts) = mk_eq (t, foldr1 HOLogic.mk_disj ts); + val (vs, nonlazy) = get_vars args; + val lhs = mk_undef (list_ccomb (con, vs)); + val rhss = map mk_undef nonlazy; + val goal = mk_trp (iff_disj (lhs, rhss)); + val rule1 = iso_locale RS @{thm iso.abs_defined_iff}; + val rules = rule1 :: @{thms con_defined_iff_rules}; + val tacs = [simp_tac (HOL_ss addsimps rules) 1]; + in prove thy con_betas goal (K tacs) end; + in + val con_stricts = maps con_strict spec'; + val con_defins = map con_defin spec'; + val con_rews = con_stricts @ con_defins; + end; + + (* prove injectiveness of constructors *) + local + fun pgterm rel (con, args) = + let + fun prime (Free (n, T)) = Free (n^"'", T) + | prime t = t; + val (xs, nonlazy) = get_vars args; + val ys = map prime xs; + val lhs = rel (list_ccomb (con, xs), list_ccomb (con, ys)); + val rhs = foldr1 mk_conj (ListPair.map rel (xs, ys)); + val concl = mk_trp (mk_eq (lhs, rhs)); + val zs = case args of [_] => [] | _ => nonlazy; + val assms = map (mk_trp o mk_defined) zs; + val goal = Logic.list_implies (assms, concl); + in prove thy con_betas goal end; + val cons' = filter (fn (_, args) => not (null args)) spec'; + in + val inverts = + let + val abs_below = iso_locale RS @{thm iso.abs_below}; + val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below}; + val rules2 = @{thms up_defined spair_defined ONE_defined} + val rules = rules1 @ rules2; + val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]; + in map (fn c => pgterm mk_below c (K tacs)) cons' end; + val injects = + let + val abs_eq = iso_locale RS @{thm iso.abs_eq}; + val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq}; + val rules2 = @{thms up_defined spair_defined ONE_defined} + val rules = rules1 @ rules2; + val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]; + in map (fn c => pgterm mk_eq c (K tacs)) cons' end; + end; + + (* prove distinctness of constructors *) + local + fun map_dist (f : 'a -> 'a -> 'b) (xs : 'a list) : 'b list = + flat (map_index (fn (i, x) => map (f x) (nth_drop i xs)) xs); + fun prime (Free (n, T)) = Free (n^"'", T) + | prime t = t; + fun iff_disj (t, []) = mk_not t + | iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts); + fun iff_disj2 (t, [], us) = mk_not t + | iff_disj2 (t, ts, []) = mk_not t + | iff_disj2 (t, ts, us) = + mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us)); + fun dist_le (con1, args1) (con2, args2) = + let + val (vs1, zs1) = get_vars args1; + val (vs2, zs2) = get_vars args2 |> pairself (map prime); + val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2)); + val rhss = map mk_undef zs1; + val goal = mk_trp (iff_disj (lhs, rhss)); + val rule1 = iso_locale RS @{thm iso.abs_below}; + val rules = rule1 :: @{thms con_below_iff_rules}; + val tacs = [simp_tac (HOL_ss addsimps rules) 1]; + in prove thy con_betas goal (K tacs) end; + fun dist_eq (con1, args1) (con2, args2) = + let + val (vs1, zs1) = get_vars args1; + val (vs2, zs2) = get_vars args2 |> pairself (map prime); + val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2)); + val rhss1 = map mk_undef zs1; + val rhss2 = map mk_undef zs2; + val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2)); + val rule1 = iso_locale RS @{thm iso.abs_eq}; + val rules = rule1 :: @{thms con_eq_iff_rules}; + val tacs = [simp_tac (HOL_ss addsimps rules) 1]; + in prove thy con_betas goal (K tacs) end; + in + val dist_les = map_dist dist_le spec'; + val dist_eqs = map_dist dist_eq spec'; + end; + + val result = + { + con_consts = con_consts, + con_betas = con_betas, + exhaust = exhaust, + casedist = casedist, + con_compacts = con_compacts, + con_rews = con_rews, + inverts = inverts, + injects = injects, + dist_les = dist_les, + dist_eqs = dist_eqs + }; + in + (result, thy) + end; + +(******************************************************************************) +(**************** definition and theorems for case combinator *****************) +(******************************************************************************) + +fun add_case_combinator + (spec : (term * (bool * typ) list) list) + (lhsT : typ) + (dname : string) + (con_betas : thm list) + (casedist : thm) + (iso_locale : thm) + (rep_const : term) + (thy : theory) + : ((typ -> term) * thm list) * theory = + let + + (* TODO: move these to holcf_library.ML *) + fun one_when_const T = Const (@{const_name one_when}, T ->> oneT ->> T); + fun mk_one_when t = one_when_const (fastype_of t) ` t; + fun mk_sscase (t, u) = + let + val (T, V) = dest_cfunT (fastype_of t); + val (U, V) = dest_cfunT (fastype_of u); + in sscase_const (T, U, V) ` t ` u end; + fun strictify_const T = Const (@{const_name strictify}, T ->> T); + fun mk_strictify t = strictify_const (fastype_of t) ` t; + fun ssplit_const (T, U, V) = + Const (@{const_name ssplit}, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V); + fun mk_ssplit t = + let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t)); + in ssplit_const (T, U, V) ` t end; + fun lambda_stuple [] t = mk_one_when t + | lambda_stuple [x] t = mk_strictify (big_lambda x t) + | lambda_stuple [x,y] t = mk_ssplit (big_lambdas [x, y] t) + | lambda_stuple (x::xs) t = mk_ssplit (big_lambda x (lambda_stuple xs t)); + + (* eta contraction for simplifying definitions *) + fun cont_eta_contract (Const(@{const_name Abs_CFun},TT) $ Abs(a,T,body)) = + (case cont_eta_contract body of + body' as (Const(@{const_name Abs_CFun},Ta) $ f $ Bound 0) => + if not (0 mem loose_bnos f) then incr_boundvars ~1 f + else Const(@{const_name Abs_CFun},TT) $ Abs(a,T,body') + | body' => Const(@{const_name Abs_CFun},TT) $ Abs(a,T,body')) + | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t + | cont_eta_contract t = t; + + (* prove rep/abs rules *) + val rep_strict = iso_locale RS @{thm iso.rep_strict}; + val abs_inverse = iso_locale RS @{thm iso.abs_iso}; + + (* calculate function arguments of case combinator *) + val tns = map (fst o dest_TFree) (snd (dest_Type lhsT)); + val resultT = TFree (Name.variant tns "'t", @{sort pcpo}); + fun fTs T = map (fn (_, args) => map snd args -->> T) spec; + val fns = Datatype_Prop.indexify_names (map (K "f") spec); + val fs = map Free (fns ~~ fTs resultT); + fun caseT T = fTs T -->> (lhsT ->> T); + + (* definition of case combinator *) + local + val case_bind = Binding.name (dname ^ "_when"); + fun one_con f (_, args) = + let + fun argT (lazy, T) = if lazy then mk_upT T else T; + fun down (lazy, T) v = if lazy then from_up T ` v else v; + val Ts = map argT args; + val ns = Name.variant_list fns (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val xs = map2 down args vs; + in + cont_eta_contract (lambda_stuple vs (list_ccomb (f, xs))) + end; + val body = foldr1 mk_sscase (map2 one_con fs spec); + val rhs = big_lambdas fs (mk_cfcomp (body, rep_const)); + val ((case_consts, case_defs), thy) = + define_consts [(case_bind, rhs, NoSyn)] thy; + val case_name = Sign.full_name thy case_bind; + in + val case_def = hd case_defs; + fun case_const T = Const (case_name, caseT T); + val case_app = list_ccomb (case_const resultT, fs); + val thy = thy; + end; + + (* define syntax for case combinator *) + (* TODO: re-implement case syntax using a parse translation *) + local + open Syntax + fun syntax c = Syntax.mark_const (fst (dest_Const c)); + fun xconst c = Long_Name.base_name (fst (dest_Const c)); + fun c_ast authentic con = + Constant (if authentic then syntax con else xconst con); + fun showint n = string_of_int (n+1); + fun expvar n = Variable ("e" ^ showint n); + fun argvar n (m, _) = Variable ("a" ^ showint n ^ "_" ^ showint m); + fun argvars n args = map_index (argvar n) args; + fun app s (l, r) = mk_appl (Constant s) [l, r]; + val cabs = app "_cabs"; + val capp = app @{const_syntax Rep_CFun}; + val capps = Library.foldl capp + fun con1 authentic n (con,args) = + Library.foldl capp (c_ast authentic con, argvars n args); + fun case1 authentic (n, c) = + app "_case1" (con1 authentic n c, expvar n); + fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args); + fun when1 n (m, c) = + if n = m then arg1 (n, c) else (Constant @{const_syntax UU}); + val case_constant = Constant (syntax (case_const dummyT)); + fun case_trans authentic = + ParsePrintRule + (app "_case_syntax" + (Variable "x", + foldr1 (app "_case2") (map_index (case1 authentic) spec)), + capp (capps (case_constant, map_index arg1 spec), Variable "x")); + fun one_abscon_trans authentic (n, c) = + ParsePrintRule + (cabs (con1 authentic n c, expvar n), + capps (case_constant, map_index (when1 n) spec)); + fun abscon_trans authentic = + map_index (one_abscon_trans authentic) spec; + val trans_rules : ast Syntax.trrule list = + case_trans false :: case_trans true :: + abscon_trans false @ abscon_trans true; + in + val thy = Sign.add_trrules_i trans_rules thy; + end; + + (* prove beta reduction rule for case combinator *) + val case_beta = beta_of_def thy case_def; + + (* prove strictness of case combinator *) + val case_strict = + let + val defs = case_beta :: map mk_meta_eq [rep_strict, @{thm cfcomp2}]; + val goal = mk_trp (mk_strict case_app); + val rules = @{thms sscase1 ssplit1 strictify1 one_when1}; + val tacs = [resolve_tac rules 1]; + in prove thy defs goal (K tacs) end; + + (* prove rewrites for case combinator *) + local + fun one_case (con, args) f = + let + val (vs, nonlazy) = get_vars args; + val assms = map (mk_trp o mk_defined) nonlazy; + val lhs = case_app ` list_ccomb (con, vs); + val rhs = list_ccomb (f, vs); + val concl = mk_trp (mk_eq (lhs, rhs)); + val goal = Logic.list_implies (assms, concl); + val defs = case_beta :: con_betas; + val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1}; + val rules2 = @{thms con_defined_iff_rules}; + val rules3 = @{thms cfcomp2 one_when2}; + val rules = abs_inverse :: rules1 @ rules2 @ rules3; + val tacs = [asm_simp_tac (beta_ss addsimps rules) 1]; + in prove thy defs goal (K tacs) end; + in + val case_apps = map2 one_case spec fs; + end + + in + ((case_const, case_strict :: case_apps), thy) + end + +(******************************************************************************) +(************** definitions and theorems for selector functions ***************) +(******************************************************************************) + +fun add_selectors + (spec : (term * (bool * binding option * typ) list) list) + (rep_const : term) + (abs_inv : thm) + (rep_strict : thm) + (rep_strict_iff : thm) + (con_betas : thm list) + (thy : theory) + : thm list * theory = + let + + (* define selector functions *) + val ((sel_consts, sel_defs), thy) = + let + fun rangeT s = snd (dest_cfunT (fastype_of s)); + fun mk_outl s = mk_cfcomp (from_sinl (dest_ssumT (rangeT s)), s); + fun mk_outr s = mk_cfcomp (from_sinr (dest_ssumT (rangeT s)), s); + fun mk_sfst s = mk_cfcomp (sfst_const (dest_sprodT (rangeT s)), s); + fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s); + fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s); + + fun sels_of_arg s (lazy, NONE, T) = [] + | sels_of_arg s (lazy, SOME b, T) = + [(b, if lazy then mk_down s else s, NoSyn)]; + fun sels_of_args s [] = [] + | sels_of_args s (v :: []) = sels_of_arg s v + | sels_of_args s (v :: vs) = + sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs; + fun sels_of_cons s [] = [] + | sels_of_cons s ((con, args) :: []) = sels_of_args s args + | sels_of_cons s ((con, args) :: cs) = + sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs; + val sel_eqns : (binding * term * mixfix) list = + sels_of_cons rep_const spec; + in + define_consts sel_eqns thy + end + + (* replace bindings with terms in constructor spec *) + val spec2 : (term * (bool * term option * typ) list) list = + let + fun prep_arg (lazy, NONE, T) sels = ((lazy, NONE, T), sels) + | prep_arg (lazy, SOME _, T) sels = + ((lazy, SOME (hd sels), T), tl sels); + fun prep_con (con, args) sels = + apfst (pair con) (fold_map prep_arg args sels); + in + fst (fold_map prep_con spec sel_consts) + end; + + (* prove selector strictness rules *) + val sel_stricts : thm list = + let + val rules = rep_strict :: @{thms sel_strict_rules}; + val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; + fun sel_strict sel = + let + val goal = mk_trp (mk_strict sel); + in + prove thy sel_defs goal (K tacs) + end + in + map sel_strict sel_consts + end + + (* prove selector application rules *) + val sel_apps : thm list = + let + val defs = con_betas @ sel_defs; + val rules = abs_inv :: @{thms sel_app_rules}; + val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]; + fun sel_apps_of (i, (con, args)) = + let + val Ts : typ list = map #3 args; + val ns : string list = Datatype_Prop.make_tnames Ts; + val vs : term list = map Free (ns ~~ Ts); + val con_app : term = list_ccomb (con, vs); + val vs' : (bool * term) list = map #1 args ~~ vs; + fun one_same (n, sel, T) = + let + val xs = map snd (filter_out fst (nth_drop n vs')); + val assms = map (mk_trp o mk_defined) xs; + val concl = mk_trp (mk_eq (sel ` con_app, nth vs n)); + val goal = Logic.list_implies (assms, concl); + in + prove thy defs goal (K tacs) + end; + fun one_diff (n, sel, T) = + let + val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T)); + in + prove thy defs goal (K tacs) + end; + fun one_con (j, (_, args')) : thm list = + let + fun prep (i, (lazy, NONE, T)) = NONE + | prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T); + val sels : (int * term * typ) list = + map_filter prep (map_index I args'); + in + if i = j + then map one_same sels + else map one_diff sels + end + in + flat (map_index one_con spec2) + end + in + flat (map_index sel_apps_of spec2) + end + + (* prove selector definedness rules *) + val sel_defins : thm list = + let + val rules = rep_strict_iff :: @{thms sel_defined_iff_rules}; + val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; + fun sel_defin sel = + let + val (T, U) = dest_cfunT (fastype_of sel); + val x = Free ("x", T); + val lhs = mk_eq (sel ` x, mk_bottom U); + val rhs = mk_eq (x, mk_bottom T); + val goal = mk_trp (mk_eq (lhs, rhs)); + in + prove thy sel_defs goal (K tacs) + end + fun one_arg (false, SOME sel, T) = SOME (sel_defin sel) + | one_arg _ = NONE; + in + case spec2 of + [(con, args)] => map_filter one_arg args + | _ => [] + end; + + in + (sel_stricts @ sel_defins @ sel_apps, thy) + end + +(******************************************************************************) +(************ definitions and theorems for discriminator functions ************) +(******************************************************************************) + +fun add_discriminators + (bindings : binding list) + (spec : (term * (bool * typ) list) list) + (lhsT : typ) + (casedist : thm) + (case_const : typ -> term) + (case_rews : thm list) + (thy : theory) = + let + + fun vars_of args = + let + val Ts = map snd args; + val ns = Datatype_Prop.make_tnames Ts; + in + map Free (ns ~~ Ts) + end; + + (* define discriminator functions *) + local + fun dis_fun i (j, (con, args)) = + let + val (vs, nonlazy) = get_vars args; + val tr = if i = j then @{term TT} else @{term FF}; + in + big_lambdas vs tr + end; + fun dis_eqn (i, bind) : binding * term * mixfix = + let + val dis_bind = Binding.prefix_name "is_" bind; + val rhs = list_ccomb (case_const trT, map_index (dis_fun i) spec); + in + (dis_bind, rhs, NoSyn) + end; + in + val ((dis_consts, dis_defs), thy) = + define_consts (map_index dis_eqn bindings) thy + end; + + (* prove discriminator strictness rules *) + local + fun dis_strict dis = + let val goal = mk_trp (mk_strict dis); + in prove thy dis_defs goal (K [rtac (hd case_rews) 1]) end; + in + val dis_stricts = map dis_strict dis_consts; + end; + + (* prove discriminator/constructor rules *) + local + fun dis_app (i, dis) (j, (con, args)) = + let + val (vs, nonlazy) = get_vars args; + val lhs = dis ` list_ccomb (con, vs); + val rhs = if i = j then @{term TT} else @{term FF}; + val assms = map (mk_trp o mk_defined) nonlazy; + val concl = mk_trp (mk_eq (lhs, rhs)); + val goal = Logic.list_implies (assms, concl); + val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]; + in prove thy dis_defs goal (K tacs) end; + fun one_dis (i, dis) = + map_index (dis_app (i, dis)) spec; + in + val dis_apps = flat (map_index one_dis dis_consts); + end; + + (* prove discriminator definedness rules *) + local + fun dis_defin dis = + let + val x = Free ("x", lhsT); + val simps = dis_apps @ @{thms dist_eq_tr}; + val tacs = + [rtac @{thm iffI} 1, + asm_simp_tac (HOL_basic_ss addsimps dis_stricts) 2, + rtac casedist 1, atac 1, + DETERM_UNTIL_SOLVED (CHANGED + (asm_full_simp_tac (simple_ss addsimps simps) 1))]; + val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x)); + in prove thy [] goal (K tacs) end; + in + val dis_defins = map dis_defin dis_consts; + end; + + in + (dis_stricts @ dis_defins @ dis_apps, thy) + end; + +(******************************************************************************) +(*************** definitions and theorems for match combinators ***************) +(******************************************************************************) + +fun add_match_combinators + (bindings : binding list) + (spec : (term * (bool * typ) list) list) + (lhsT : typ) + (casedist : thm) + (case_const : typ -> term) + (case_rews : thm list) + (thy : theory) = + let + + (* get a fresh type variable for the result type *) + val resultT : typ = + let + val ts : string list = map (fst o dest_TFree) (snd (dest_Type lhsT)); + val t : string = Name.variant ts "'t"; + in TFree (t, @{sort pcpo}) end; + + (* define match combinators *) + local + val x = Free ("x", lhsT); + fun k args = Free ("k", map snd args -->> mk_matchT resultT); + val fail = mk_fail resultT; + fun mat_fun i (j, (con, args)) = + let + val (vs, nonlazy) = get_vars_avoiding ["x","k"] args; + in + if i = j then k args else big_lambdas vs fail + end; + fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix = + let + val mat_bind = Binding.prefix_name "match_" bind; + val funs = map_index (mat_fun i) spec + val body = list_ccomb (case_const (mk_matchT resultT), funs); + val rhs = big_lambda x (big_lambda (k args) (body ` x)); + in + (mat_bind, rhs, NoSyn) + end; + in + val ((match_consts, match_defs), thy) = + define_consts (map_index mat_eqn (bindings ~~ spec)) thy + end; + + (* register match combinators with fixrec package *) + local + val con_names = map (fst o dest_Const o fst) spec; + val mat_names = map (fst o dest_Const) match_consts; + in + val thy = Fixrec.add_matchers (con_names ~~ mat_names) thy; + end; + + (* prove strictness of match combinators *) + local + fun match_strict mat = + let + val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat)); + val k = Free ("k", U); + val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V)); + val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]; + in prove thy match_defs goal (K tacs) end; + in + val match_stricts = map match_strict match_consts; + end; + + (* prove match/constructor rules *) + local + val fail = mk_fail resultT; + fun match_app (i, mat) (j, (con, args)) = + let + val (vs, nonlazy) = get_vars_avoiding ["k"] args; + val (_, (kT, _)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat)); + val k = Free ("k", kT); + val lhs = mat ` list_ccomb (con, vs) ` k; + val rhs = if i = j then list_ccomb (k, vs) else fail; + val assms = map (mk_trp o mk_defined) nonlazy; + val concl = mk_trp (mk_eq (lhs, rhs)); + val goal = Logic.list_implies (assms, concl); + val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]; + in prove thy match_defs goal (K tacs) end; + fun one_match (i, mat) = + map_index (match_app (i, mat)) spec; + in + val match_apps = flat (map_index one_match match_consts); + end; + + in + (match_stricts @ match_apps, thy) + end; + +(******************************************************************************) +(************** definitions and theorems for pattern combinators **************) +(******************************************************************************) + +fun add_pattern_combinators + (bindings : binding list) + (spec : (term * (bool * typ) list) list) + (lhsT : typ) + (casedist : thm) + (case_const : typ -> term) + (case_rews : thm list) + (thy : theory) = + let + + (* utility functions *) + fun mk_pair_pat (p1, p2) = + let + val T1 = fastype_of p1; + val T2 = fastype_of p2; + val (U1, V1) = apsnd dest_matchT (dest_cfunT T1); + val (U2, V2) = apsnd dest_matchT (dest_cfunT T2); + val pat_typ = [T1, T2] ---> + (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2))); + val pat_const = Const (@{const_name cpair_pat}, pat_typ); + in + pat_const $ p1 $ p2 + end; + fun mk_tuple_pat [] = return_const HOLogic.unitT + | mk_tuple_pat ps = foldr1 mk_pair_pat ps; + fun branch_const (T,U,V) = + Const (@{const_name branch}, + (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V); + + (* define pattern combinators *) + local + val tns = map (fst o dest_TFree) (snd (dest_Type lhsT)); + + fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix = + let + val pat_bind = Binding.suffix_name "_pat" bind; + val Ts = map snd args; + val Vs = + (map (K "'t") args) + |> Datatype_Prop.indexify_names + |> Name.variant_list tns + |> map (fn t => TFree (t, @{sort pcpo})); + val patNs = Datatype_Prop.indexify_names (map (K "pat") args); + val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs; + val pats = map Free (patNs ~~ patTs); + val fail = mk_fail (mk_tupleT Vs); + val (vs, nonlazy) = get_vars_avoiding patNs args; + val rhs = big_lambdas vs (mk_tuple_pat pats ` mk_tuple vs); + fun one_fun (j, (_, args')) = + let + val (vs', nonlazy) = get_vars_avoiding patNs args'; + in if i = j then rhs else big_lambdas vs' fail end; + val funs = map_index one_fun spec; + val body = list_ccomb (case_const (mk_matchT (mk_tupleT Vs)), funs); + in + (pat_bind, lambdas pats body, NoSyn) + end; + in + val ((pat_consts, pat_defs), thy) = + define_consts (map_index pat_eqn (bindings ~~ spec)) thy + end; + + (* syntax translations for pattern combinators *) + local + open Syntax + fun syntax c = Syntax.mark_const (fst (dest_Const c)); + fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r]; + val capp = app @{const_syntax Rep_CFun}; + val capps = Library.foldl capp + + fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"]; + fun app_pat x = Syntax.mk_appl (Constant "_pat") [x]; + fun args_list [] = Constant "_noargs" + | args_list xs = foldr1 (app "_args") xs; + fun one_case_trans (pat, (con, args)) = + let + val cname = Constant (syntax con); + val pname = Constant (syntax pat); + val ns = 1 upto length args; + val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; + val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; + val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; + in + [ParseRule (app_pat (capps (cname, xs)), + mk_appl pname (map app_pat xs)), + ParseRule (app_var (capps (cname, xs)), + app_var (args_list xs)), + PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)), + app "_match" (mk_appl pname ps, args_list vs))] + end; + val trans_rules : Syntax.ast Syntax.trrule list = + maps one_case_trans (pat_consts ~~ spec); + in + val thy = Sign.add_trrules_i trans_rules thy; + end; + + (* prove strictness and reduction rules of pattern combinators *) + local + val tns = map (fst o dest_TFree) (snd (dest_Type lhsT)); + val rn = Name.variant tns "'r"; + val R = TFree (rn, @{sort pcpo}); + fun pat_lhs (pat, args) = + let + val Ts = map snd args; + val Vs = + (map (K "'t") args) + |> Datatype_Prop.indexify_names + |> Name.variant_list (rn::tns) + |> map (fn t => TFree (t, @{sort pcpo})); + val patNs = Datatype_Prop.indexify_names (map (K "pat") args); + val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs; + val pats = map Free (patNs ~~ patTs); + val k = Free ("rhs", mk_tupleT Vs ->> R); + val branch1 = branch_const (lhsT, mk_tupleT Vs, R); + val fun1 = (branch1 $ list_comb (pat, pats)) ` k; + val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R); + val fun2 = (branch2 $ mk_tuple_pat pats) ` k; + val taken = "rhs" :: patNs; + in (fun1, fun2, taken) end; + fun pat_strict (pat, (con, args)) = + let + val (fun1, fun2, taken) = pat_lhs (pat, args); + val defs = @{thm branch_def} :: pat_defs; + val goal = mk_trp (mk_strict fun1); + val rules = @{thm Fixrec.bind_strict} :: case_rews; + val tacs = [simp_tac (beta_ss addsimps rules) 1]; + in prove thy defs goal (K tacs) end; + fun pat_apps (i, (pat, (con, args))) = + let + val (fun1, fun2, taken) = pat_lhs (pat, args); + fun pat_app (j, (con', args')) = + let + val (vs, nonlazy) = get_vars_avoiding taken args'; + val con_app = list_ccomb (con', vs); + val assms = map (mk_trp o mk_defined) nonlazy; + val rhs = if i = j then fun2 ` mk_tuple vs else mk_fail R; + val concl = mk_trp (mk_eq (fun1 ` con_app, rhs)); + val goal = Logic.list_implies (assms, concl); + val defs = @{thm branch_def} :: pat_defs; + val rules = @{thms bind_fail left_unit} @ case_rews; + val tacs = [asm_simp_tac (beta_ss addsimps rules) 1]; + in prove thy defs goal (K tacs) end; + in map_index pat_app spec end; + in + val pat_stricts = map pat_strict (pat_consts ~~ spec); + val pat_apps = flat (map_index pat_apps (pat_consts ~~ spec)); + end; + + in + (pat_stricts @ pat_apps, thy) + end + +(******************************************************************************) +(******************************* main function ********************************) +(******************************************************************************) + +fun add_domain_constructors + (dname : string) + (spec : (binding * (bool * binding option * typ) list * mixfix) list) + (iso_info : Domain_Isomorphism.iso_info) + (thy : theory) = + let + + (* retrieve facts about rep/abs *) + val lhsT = #absT iso_info; + val {rep_const, abs_const, ...} = iso_info; + val abs_iso_thm = #abs_inverse iso_info; + val rep_iso_thm = #rep_inverse iso_info; + val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm]; + val rep_strict = iso_locale RS @{thm iso.rep_strict}; + val abs_strict = iso_locale RS @{thm iso.abs_strict}; + val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff}; + val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff}; + + (* qualify constants and theorems with domain name *) + val thy = Sign.add_path dname thy; + + (* define constructor functions *) + val (con_result, thy) = + let + fun prep_arg (lazy, sel, T) = (lazy, T); + fun prep_con (b, args, mx) = (b, map prep_arg args, mx); + val con_spec = map prep_con spec; + in + add_constructors con_spec abs_const iso_locale thy + end; + val {con_consts, con_betas, casedist, ...} = con_result; + + (* define case combinator *) + val ((case_const : typ -> term, cases : thm list), thy) = + let + fun prep_arg (lazy, sel, T) = (lazy, T); + fun prep_con c (b, args, mx) = (c, map prep_arg args); + val case_spec = map2 prep_con con_consts spec; + in + add_case_combinator case_spec lhsT dname + con_betas casedist iso_locale rep_const thy + end; + + (* define and prove theorems for selector functions *) + val (sel_thms : thm list, thy : theory) = + let + val sel_spec : (term * (bool * binding option * typ) list) list = + map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec; + in + add_selectors sel_spec rep_const + abs_iso_thm rep_strict rep_defined_iff con_betas thy + end; + + (* define and prove theorems for discriminator functions *) + val (dis_thms : thm list, thy : theory) = + let + val bindings = map #1 spec; + fun prep_arg (lazy, sel, T) = (lazy, T); + fun prep_con c (b, args, mx) = (c, map prep_arg args); + val dis_spec = map2 prep_con con_consts spec; + in + add_discriminators bindings dis_spec lhsT + casedist case_const cases thy + end + + (* define and prove theorems for match combinators *) + val (match_thms : thm list, thy : theory) = + let + val bindings = map #1 spec; + fun prep_arg (lazy, sel, T) = (lazy, T); + fun prep_con c (b, args, mx) = (c, map prep_arg args); + val mat_spec = map2 prep_con con_consts spec; + in + add_match_combinators bindings mat_spec lhsT + casedist case_const cases thy + end + + (* define and prove theorems for pattern combinators *) + val (pat_thms : thm list, thy : theory) = + let + val bindings = map #1 spec; + fun prep_arg (lazy, sel, T) = (lazy, T); + fun prep_con c (b, args, mx) = (c, map prep_arg args); + val pat_spec = map2 prep_con con_consts spec; + in + add_pattern_combinators bindings pat_spec lhsT + casedist case_const cases thy + end + + (* restore original signature path *) + val thy = Sign.parent_path thy; + + val result = + { con_consts = con_consts, + con_betas = con_betas, + exhaust = #exhaust con_result, + casedist = casedist, + con_compacts = #con_compacts con_result, + con_rews = #con_rews con_result, + inverts = #inverts con_result, + injects = #injects con_result, + dist_les = #dist_les con_result, + dist_eqs = #dist_eqs con_result, + cases = cases, + sel_rews = sel_thms, + dis_rews = dis_thms, + match_rews = match_thms, + pat_rews = pat_thms }; + in + (result, thy) + end; + +end; diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 15:39:15 2010 +0100 @@ -150,29 +150,26 @@ val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = check_and_sort_domain false dtnvs' cons'' thy''; - val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs'; + val thy' = thy'' |> Domain_Syntax.add_syntax false eqs'; val dts = map (Type o fst) eqs'; val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss; - fun typid (Type (id,_)) = - let val c = hd (Symbol.explode (Long_Name.base_name id)) - in if Symbol.is_letter c then c else "t" end - | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) - | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); fun one_con (con,args,mx) = (Binding.name_of con, (* FIXME preverse binding (!?) *) mx, ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), Option.map Binding.name_of sel,vn)) - (args,(mk_var_names(map (typid o third) args))) + (args, Datatype_Prop.make_tnames (map third args)) ) : cons; val eqs : eq list = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; - val thy = thy' |> Domain_Axioms.add_axioms false comp_dnam eqs; + val thy = thy' |> Domain_Axioms.add_axioms false eqs' eqs; val ((rewss, take_rews), theorems_thy) = thy - |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs + |> fold_map (fn (eq, (x,cs)) => + Domain_Theorems.theorems (eq, eqs) (Type x, cs)) + (eqs ~~ eqs') ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); in theorems_thy @@ -220,35 +217,32 @@ if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); - val thy'' = thy''' |> + val (iso_infos, thy'') = thy''' |> Domain_Isomorphism.domain_isomorphism (map (fn ((vs, dname, mx, _), eq) => (map fst vs, dname, mx, mk_eq_typ eq, NONE)) (eqs''' ~~ eqs')) - val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs'; + val thy' = thy'' |> Domain_Syntax.add_syntax true eqs'; val dts = map (Type o fst) eqs'; val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss; - fun typid (Type (id,_)) = - let val c = hd (Symbol.explode (Long_Name.base_name id)) - in if Symbol.is_letter c then c else "t" end - | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) - | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); fun one_con (con,args,mx) = (Binding.name_of con, (* FIXME preverse binding (!?) *) mx, ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), Option.map Binding.name_of sel,vn)) - (args,(mk_var_names(map (typid o third) args))) + (args, Datatype_Prop.make_tnames (map third args)) ) : cons; val eqs : eq list = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; - val thy = thy' |> Domain_Axioms.add_axioms true comp_dnam eqs; + val thy = thy' |> Domain_Axioms.add_axioms true eqs' eqs; val ((rewss, take_rews), theorems_thy) = thy - |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs + |> fold_map (fn (eq, (x,cs)) => + Domain_Theorems.theorems (eq, eqs) (Type x, cs)) + (eqs ~~ eqs') ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); in theorems_thy diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 15:39:15 2010 +0100 @@ -6,16 +6,34 @@ signature DOMAIN_ISOMORPHISM = sig - val domain_isomorphism: + type iso_info = + { + repT : typ, + absT : typ, + rep_const : term, + abs_const : term, + rep_inverse : thm, + abs_inverse : thm + } + val domain_isomorphism : (string list * binding * mixfix * typ * (binding * binding) option) list - -> theory -> theory - val domain_isomorphism_cmd: + -> theory -> iso_info list * theory + val domain_isomorphism_cmd : (string list * binding * mixfix * string * (binding * binding) option) list -> theory -> theory - val add_type_constructor: - (string * term * string * thm * thm * thm) -> theory -> theory - val get_map_tab: + val add_type_constructor : + (string * term * string * thm * thm * thm * thm) -> theory -> theory + val get_map_tab : theory -> string Symtab.table + val define_take_functions : + (binding * iso_info) list -> theory -> + { take_consts : term list, + take_defs : thm list, + chain_take_thms : thm list, + take_0_thms : thm list, + take_Suc_thms : thm list, + deflation_take_thms : thm list + } * theory; end; structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM = @@ -49,133 +67,49 @@ fun merge data = Symtab.merge (K true) data; ); -structure RepData = Theory_Data -( - type T = thm list; - val empty = []; - val extend = I; - val merge = Thm.merge_thms; -); - -structure IsodeflData = Theory_Data -( +structure Thm_List : THEORY_DATA_ARGS = +struct type T = thm list; val empty = []; val extend = I; val merge = Thm.merge_thms; -); +end; + +structure RepData = Theory_Data (Thm_List); -structure MapIdData = Theory_Data -( - type T = thm list; - val empty = []; - val extend = I; - val merge = Thm.merge_thms; -); +structure IsodeflData = Theory_Data (Thm_List); + +structure MapIdData = Theory_Data (Thm_List); + +structure DeflMapData = Theory_Data (Thm_List); fun add_type_constructor - (tname, defl_const, map_name, REP_thm, isodefl_thm, map_ID_thm) = + (tname, defl_const, map_name, REP_thm, + isodefl_thm, map_ID_thm, defl_map_thm) = DeflData.map (Symtab.insert (K true) (tname, defl_const)) #> MapData.map (Symtab.insert (K true) (tname, map_name)) #> RepData.map (Thm.add_thm REP_thm) #> IsodeflData.map (Thm.add_thm isodefl_thm) - #> MapIdData.map (Thm.add_thm map_ID_thm); + #> MapIdData.map (Thm.add_thm map_ID_thm) + #> DeflMapData.map (Thm.add_thm defl_map_thm); val get_map_tab = MapData.get; (******************************************************************************) -(******************************* building types *******************************) +(************************** building types and terms **************************) (******************************************************************************) -(* ->> is taken from holcf_logic.ML *) -fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]); - -infixr 6 ->>; val (op ->>) = cfunT; +open HOLCF_Library; -fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) - | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); - -fun tupleT [] = HOLogic.unitT - | tupleT [T] = T - | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts); +infixr 6 ->>; +infix -->>; val deflT = @{typ "udom alg_defl"}; fun mapT (T as Type (_, Ts)) = - Library.foldr cfunT (map (fn T => T ->> T) Ts, T ->> T); - -(******************************************************************************) -(******************************* building terms *******************************) -(******************************************************************************) - -(* builds the expression (v1,v2,..,vn) *) -fun mk_tuple [] = HOLogic.unit -| mk_tuple (t::[]) = t -| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts); - -(* builds the expression (%(v1,v2,..,vn). rhs) *) -fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs - | lambda_tuple (v::[]) rhs = Term.lambda v rhs - | lambda_tuple (v::vs) rhs = - HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)); - -(* continuous application and abstraction *) - -fun capply_const (S, T) = - Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T)); - -fun cabs_const (S, T) = - Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T)); - -fun mk_cabs t = - let val T = Term.fastype_of t - in cabs_const (Term.domain_type T, Term.range_type T) $ t end - -(* builds the expression (LAM v. rhs) *) -fun big_lambda v rhs = - cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs; - -(* builds the expression (LAM v1 v2 .. vn. rhs) *) -fun big_lambdas [] rhs = rhs - | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); - -fun mk_capply (t, u) = - let val (S, T) = - case Term.fastype_of t of - Type(@{type_name "->"}, [S, T]) => (S, T) - | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); - in capply_const (S, T) $ t $ u end; - -(* miscellaneous term constructions *) - -val mk_trp = HOLogic.mk_Trueprop; - -val mk_fst = HOLogic.mk_fst; -val mk_snd = HOLogic.mk_snd; - -fun mk_cont t = - let val T = Term.fastype_of t - in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end; - -fun mk_fix t = - let val (T, _) = dest_cfunT (Term.fastype_of t) - in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end; - -fun ID_const T = Const (@{const_name ID}, cfunT (T, T)); - -fun cfcomp_const (T, U, V) = - Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V)); - -fun mk_cfcomp (f, g) = - let - val (U, V) = dest_cfunT (Term.fastype_of f); - val (T, U') = dest_cfunT (Term.fastype_of g); - in - if U = U' - then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g) - else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) - end; + (map (fn T => T ->> T) Ts) -->> (T ->> T) + | mapT T = T ->> T; fun mk_Rep_of T = Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T; @@ -185,12 +119,49 @@ fun isodefl_const T = Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT); +fun mk_deflation t = + Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t; + +fun mk_lub t = + let + val T = Term.range_type (Term.fastype_of t); + val lub_const = Const (@{const_name lub}, (T --> boolT) --> T); + val UNIV_const = @{term "UNIV :: nat set"}; + val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT; + val image_const = Const (@{const_name image}, image_type); + in + lub_const $ (image_const $ t $ UNIV_const) + end; + (* splits a cterm into the right and lefthand sides of equality *) fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); (******************************************************************************) +(****************************** isomorphism info ******************************) +(******************************************************************************) + +type iso_info = + { + absT : typ, + repT : typ, + abs_const : term, + rep_const : term, + abs_inverse : thm, + rep_inverse : thm + } + +fun deflation_abs_rep (info : iso_info) : thm = + let + val abs_iso = #abs_inverse info; + val rep_iso = #rep_inverse info; + val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]; + in + Drule.export_without_context thm + end + +(******************************************************************************) (*************** fixed-point definitions and unfolding theorems ***************) (******************************************************************************) @@ -204,7 +175,8 @@ val fixpoint = mk_fix (mk_cabs functional); (* project components of fixpoint *) - fun mk_projs (x::[]) t = [(x, t)] + fun mk_projs [] t = [] + | mk_projs (x::[]) t = [(x, t)] | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); val projs = mk_projs lhss fixpoint; @@ -272,7 +244,7 @@ | defl_of (TVar _) = error ("defl_of_typ: TVar") | defl_of (T as Type (c, Ts)) = case Symtab.lookup tab c of - SOME t => Library.foldl mk_capply (t, map defl_of Ts) + SOME t => list_ccomb (t, map defl_of Ts) | NONE => if is_closed_typ T then mk_Rep_of T else error ("defl_of_typ: type variable under unsupported type constructor " ^ c); @@ -288,15 +260,252 @@ | map_of (T as TVar _) = error ("map_of_typ: TVar") | map_of (T as Type (c, Ts)) = case Symtab.lookup tab c of - SOME t => Library.foldl mk_capply (Const (t, mapT T), map map_of Ts) + SOME t => list_ccomb (Const (t, mapT T), map map_of Ts) | NONE => if is_closed_typ T - then ID_const T + then mk_ID T else error ("map_of_typ: type variable under unsupported type constructor " ^ c); in map_of T end; (******************************************************************************) -(* prepare datatype specifications *) +(********************* declaring definitions and theorems *********************) +(******************************************************************************) + +fun define_const + (bind : binding, rhs : term) + (thy : theory) + : (term * thm) * theory = + let + val typ = Term.fastype_of rhs; + val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy; + val eqn = Logic.mk_equals (const, rhs); + val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn); + val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy; + in + ((const, def_thm), thy) + end; + +fun add_qualified_thm name (path, thm) thy = + thy + |> Sign.add_path path + |> yield_singleton PureThy.add_thms + (Thm.no_attributes (Binding.name name, thm)) + ||> Sign.parent_path; + +(******************************************************************************) +(************************** defining take functions ***************************) +(******************************************************************************) + +fun define_take_functions + (spec : (binding * iso_info) list) + (thy : theory) = + let + + (* retrieve components of spec *) + val dom_binds = map fst spec; + val iso_infos = map snd spec; + val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos; + val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos; + val dnames = map Binding.name_of dom_binds; + + (* get table of map functions *) + val map_tab = MapData.get thy; + + fun mk_projs [] t = [] + | mk_projs (x::[]) t = [(x, t)] + | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); + + fun mk_cfcomp2 ((rep_const, abs_const), f) = + mk_cfcomp (abs_const, mk_cfcomp (f, rep_const)); + + (* defining map functions over dtyps *) + fun copy_of_dtyp recs (T, dt) = + if Datatype_Aux.is_rec_type dt + then copy_of_dtyp' recs (T, dt) + else mk_ID T + and copy_of_dtyp' recs (T, Datatype_Aux.DtRec i) = nth recs i + | copy_of_dtyp' recs (T, Datatype_Aux.DtTFree a) = mk_ID T + | copy_of_dtyp' recs (T, Datatype_Aux.DtType (c, ds)) = + case Symtab.lookup map_tab c of + SOME f => + list_ccomb + (Const (f, mapT T), + map (copy_of_dtyp recs) (snd (dest_Type T) ~~ ds)) + | NONE => + (warning ("copy_of_dtyp: unknown type constructor " ^ c); mk_ID T); + + (* define take functional *) + val new_dts : (string * string list) list = + map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns; + val copy_arg_type = mk_tupleT (map (fn (T, _) => T ->> T) dom_eqns); + val copy_arg = Free ("f", copy_arg_type); + val copy_args = map snd (mk_projs dom_binds copy_arg); + fun one_copy_rhs (rep_abs, (lhsT, rhsT)) = + let + val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT; + val body = copy_of_dtyp copy_args (rhsT, dtyp); + in + mk_cfcomp2 (rep_abs, body) + end; + val take_functional = + big_lambda copy_arg + (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns))); + val take_rhss = + let + val i = Free ("i", HOLogic.natT); + val rhs = mk_iterate (i, take_functional) + in + map (Term.lambda i o snd) (mk_projs dom_binds rhs) + end; + + (* define take constants *) + fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy = + let + val take_type = HOLogic.natT --> lhsT ->> lhsT; + val take_bind = Binding.suffix_name "_take" tbind; + val (take_const, thy) = + Sign.declare_const ((take_bind, take_type), NoSyn) thy; + val take_eqn = Logic.mk_equals (take_const, take_rhs); + val (take_def_thm, thy) = + thy + |> Sign.add_path (Binding.name_of tbind) + |> yield_singleton + (PureThy.add_defs false o map Thm.no_attributes) + (Binding.name "take_def", take_eqn) + ||> Sign.parent_path; + in ((take_const, take_def_thm), thy) end; + val ((take_consts, take_defs), thy) = thy + |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns) + |>> ListPair.unzip; + + (* prove chain_take lemmas *) + fun prove_chain_take (take_const, dname) thy = + let + val goal = mk_trp (mk_chain take_const); + val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd}; + val tac = simp_tac (HOL_basic_ss addsimps rules) 1; + val chain_take_thm = Goal.prove_global thy [] [] goal (K tac); + in + add_qualified_thm "chain_take" (dname, chain_take_thm) thy + end; + val (chain_take_thms, thy) = + fold_map prove_chain_take (take_consts ~~ dnames) thy; + + (* prove take_0 lemmas *) + fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy = + let + val lhs = take_const $ @{term "0::nat"}; + val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT)); + val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict}; + val tac = simp_tac (HOL_basic_ss addsimps rules) 1; + val take_0_thm = Goal.prove_global thy [] [] goal (K tac); + in + add_qualified_thm "take_0" (dname, take_0_thm) thy + end; + val (take_0_thms, thy) = + fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy; + + (* prove take_Suc lemmas *) + val i = Free ("i", natT); + val take_is = map (fn t => t $ i) take_consts; + fun prove_take_Suc + (((take_const, rep_abs), dname), (lhsT, rhsT)) thy = + let + val lhs = take_const $ (@{term Suc} $ i); + val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT; + val body = copy_of_dtyp take_is (rhsT, dtyp); + val rhs = mk_cfcomp2 (rep_abs, body); + val goal = mk_eqs (lhs, rhs); + val simps = @{thms iterate_Suc fst_conv snd_conv} + val rules = take_defs @ simps; + val tac = simp_tac (beta_ss addsimps rules) 1; + val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac); + in + add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy + end; + val (take_Suc_thms, thy) = + fold_map prove_take_Suc + (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy; + + (* prove deflation theorems for take functions *) + val deflation_abs_rep_thms = map deflation_abs_rep iso_infos; + val deflation_take_thm = + let + val i = Free ("i", natT); + fun mk_goal take_const = mk_deflation (take_const $ i); + val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)); + val adm_rules = + @{thms adm_conj adm_subst [OF _ adm_deflation] + cont2cont_fst cont2cont_snd cont_id}; + val bottom_rules = + take_0_thms @ @{thms deflation_UU simp_thms}; + val deflation_rules = + @{thms conjI deflation_ID} + @ deflation_abs_rep_thms + @ DeflMapData.get thy; + in + Goal.prove_global thy [] [] goal (fn _ => + EVERY + [rtac @{thm nat.induct} 1, + simp_tac (HOL_basic_ss addsimps bottom_rules) 1, + asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1, + REPEAT (etac @{thm conjE} 1 + ORELSE resolve_tac deflation_rules 1 + ORELSE atac 1)]) + end; + fun conjuncts [] thm = [] + | conjuncts (n::[]) thm = [(n, thm)] + | conjuncts (n::ns) thm = let + val thmL = thm RS @{thm conjunct1}; + val thmR = thm RS @{thm conjunct2}; + in (n, thmL):: conjuncts ns thmR end; + val (deflation_take_thms, thy) = + fold_map (add_qualified_thm "deflation_take") + (map (apsnd Drule.export_without_context) + (conjuncts dnames deflation_take_thm)) thy; + + (* prove strictness of take functions *) + fun prove_take_strict (take_const, dname) thy = + let + val goal = mk_trp (mk_strict (take_const $ Free ("i", natT))); + val tac = rtac @{thm deflation_strict} 1 + THEN resolve_tac deflation_take_thms 1; + val take_strict_thm = Goal.prove_global thy [] [] goal (K tac); + in + add_qualified_thm "take_strict" (dname, take_strict_thm) thy + end; + val (take_strict_thms, thy) = + fold_map prove_take_strict (take_consts ~~ dnames) thy; + + (* prove take/take rules *) + fun prove_take_take ((chain_take, deflation_take), dname) thy = + let + val take_take_thm = + @{thm deflation_chain_min} OF [chain_take, deflation_take]; + in + add_qualified_thm "take_take" (dname, take_take_thm) thy + end; + val (take_take_thms, thy) = + fold_map prove_take_take + (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy; + + val result = + { + take_consts = take_consts, + take_defs = take_defs, + chain_take_thms = chain_take_thms, + take_0_thms = take_0_thms, + take_Suc_thms = take_Suc_thms, + deflation_take_thms = deflation_take_thms + }; + + in + (result, thy) + end; + +(******************************************************************************) +(******************************* main function ********************************) +(******************************************************************************) fun read_typ thy str sorts = let @@ -320,7 +529,7 @@ (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list) (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list) (thy: theory) - : theory = + : iso_info list * theory = let val _ = Theory.requires thy "Representable" "domain isomorphisms"; @@ -345,7 +554,7 @@ val dom_eqns = map mk_dom_eqn doms; (* check for valid type parameters *) - val (tyvars, _, _, _, _)::_ = doms; + val (tyvars, _, _, _, _) = hd doms; val new_doms = map (fn (tvs, tname, mx, _, _) => let val full_tname = Sign.full_name tmp_thy tname in @@ -362,7 +571,7 @@ (* declare deflation combinator constants *) fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy = let - val defl_type = Library.foldr cfunT (map (K deflT) vs, deflT); + val defl_type = map (K deflT) vs -->> deflT; val defl_bind = Binding.suffix_name "_defl" tbind; in Sign.declare_const ((defl_bind, defl_type), NoSyn) thy @@ -390,7 +599,7 @@ let fun tfree a = TFree (a, the (AList.lookup (op =) sorts a)) val reps = map (mk_Rep_of o tfree) vs; - val defl = Library.foldl mk_capply (defl_const, reps); + val defl = list_ccomb (defl_const, reps); val ((_, _, _, {REP, ...}), thy) = Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy; in @@ -421,21 +630,12 @@ (* define rep/abs functions *) fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy = let - val rep_type = cfunT (lhsT, rhsT); - val abs_type = cfunT (rhsT, lhsT); val rep_bind = Binding.suffix_name "_rep" tbind; val abs_bind = Binding.suffix_name "_abs" tbind; - val (rep_bind, abs_bind) = the_default (rep_bind, abs_bind) morphs; - val (rep_const, thy) = thy |> - Sign.declare_const ((rep_bind, rep_type), NoSyn); - val (abs_const, thy) = thy |> - Sign.declare_const ((abs_bind, abs_type), NoSyn); - val rep_eqn = Logic.mk_equals (rep_const, coerce_const rep_type); - val abs_eqn = Logic.mk_equals (abs_const, coerce_const abs_type); - val ([rep_def, abs_def], thy) = thy |> - (PureThy.add_defs false o map Thm.no_attributes) - [(Binding.suffix_name "_rep_def" tbind, rep_eqn), - (Binding.suffix_name "_abs_def" tbind, abs_eqn)]; + val ((rep_const, rep_def), thy) = + define_const (rep_bind, coerce_const (lhsT ->> rhsT)) thy; + val ((abs_const, abs_def), thy) = + define_const (abs_bind, coerce_const (rhsT ->> lhsT)) thy; in (((rep_const, abs_const), (rep_def, abs_def)), thy) end; @@ -463,10 +663,27 @@ in (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy) end; - val ((iso_thms, isodefl_abs_rep_thms), thy) = thy + val ((iso_thms, isodefl_abs_rep_thms), thy) = + thy |> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs) |>> ListPair.unzip; + (* collect info about rep/abs *) + val iso_infos : iso_info list = + let + fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) = + { + repT = rhsT, + absT = lhsT, + rep_const = repC, + abs_const = absC, + rep_inverse = rep_iso, + abs_inverse = abs_iso + }; + in + map mk_info (dom_eqns ~~ rep_abs_consts ~~ iso_thms) + end + (* declare map functions *) fun declare_map_const (tbind, (lhsT, rhsT)) thy = let @@ -502,13 +719,14 @@ val isodefl_thm = let fun unprime a = Library.unprefix "'" a; - fun mk_d (TFree (a, _)) = Free ("d" ^ unprime a, deflT); - fun mk_f (T as TFree (a, _)) = Free ("f" ^ unprime a, T ->> T); + fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT); + fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T); fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T); - fun mk_goal ((map_const, defl_const), (T as Type (c, Ts), rhsT)) = + fun mk_goal ((map_const, defl_const), (T, rhsT)) = let - val map_term = Library.foldl mk_capply (map_const, map mk_f Ts); - val defl_term = Library.foldl mk_capply (defl_const, map mk_d Ts); + val (_, Ts) = dest_Type T; + val map_term = list_ccomb (map_const, map mk_f Ts); + val defl_term = list_ccomb (defl_const, map mk_d Ts); in isodefl_const T $ map_term $ defl_term end; val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns; val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns); @@ -554,8 +772,8 @@ (((map_const, (lhsT, _)), REP_thm), isodefl_thm) = let val Ts = snd (dest_Type lhsT); - val lhs = Library.foldl mk_capply (map_const, map ID_const Ts); - val goal = mk_eqs (lhs, ID_const lhsT); + val lhs = list_ccomb (map_const, map mk_ID Ts); + val goal = mk_eqs (lhs, mk_ID lhsT); val tac = EVERY [rtac @{thm isodefl_REP_imp_ID} 1, stac REP_thm 1, @@ -573,121 +791,110 @@ (map_ID_binds ~~ map_ID_thms); val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy; - (* define copy combinators *) - val new_dts = - map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns; - val copy_arg_type = tupleT (map (fn (T, _) => T ->> T) dom_eqns); - val copy_arg = Free ("f", copy_arg_type); - val copy_args = - let fun mk_copy_args [] t = [] - | mk_copy_args (_::[]) t = [t] - | mk_copy_args (_::xs) t = - mk_fst t :: mk_copy_args xs (mk_snd t); - in mk_copy_args doms copy_arg end; - fun copy_of_dtyp (T, dt) = - if Datatype_Aux.is_rec_type dt - then copy_of_dtyp' (T, dt) - else ID_const T - and copy_of_dtyp' (T, Datatype_Aux.DtRec i) = nth copy_args i - | copy_of_dtyp' (T, Datatype_Aux.DtTFree a) = ID_const T - | copy_of_dtyp' (T as Type (_, Ts), Datatype_Aux.DtType (c, ds)) = - case Symtab.lookup map_tab' c of - SOME f => - Library.foldl mk_capply - (Const (f, mapT T), map copy_of_dtyp (Ts ~~ ds)) - | NONE => - (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID_const T); - fun define_copy ((tbind, (rep_const, abs_const)), (lhsT, rhsT)) thy = + (* prove deflation theorems for map functions *) + val deflation_abs_rep_thms = map deflation_abs_rep iso_infos; + val deflation_map_thm = let - val copy_type = copy_arg_type ->> (lhsT ->> lhsT); - val copy_bind = Binding.suffix_name "_copy" tbind; - val (copy_const, thy) = thy |> - Sign.declare_const ((copy_bind, copy_type), NoSyn); - val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT; - val body = copy_of_dtyp (rhsT, dtyp); - val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)); - val rhs = big_lambda copy_arg comp; - val eqn = Logic.mk_equals (copy_const, rhs); - val ([copy_def], thy) = - thy - |> Sign.add_path (Binding.name_of tbind) - |> (PureThy.add_defs false o map Thm.no_attributes) - [(Binding.name "copy_def", eqn)] - ||> Sign.parent_path; - in ((copy_const, copy_def), thy) end; - val ((copy_consts, copy_defs), thy) = thy - |> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns) - |>> ListPair.unzip; + fun unprime a = Library.unprefix "'" a; + fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T); + fun mk_assm T = mk_trp (mk_deflation (mk_f T)); + fun mk_goal (map_const, (lhsT, rhsT)) = + let + val (_, Ts) = dest_Type lhsT; + val map_term = list_ccomb (map_const, map mk_f Ts); + in mk_deflation map_term end; + val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns; + val goals = map mk_goal (map_consts ~~ dom_eqns); + val goal = mk_trp (foldr1 HOLogic.mk_conj goals); + val start_thms = + @{thm split_def} :: map_apply_thms; + val adm_rules = + @{thms adm_conj adm_subst [OF _ adm_deflation] + cont2cont_fst cont2cont_snd cont_id}; + val bottom_rules = + @{thms fst_strict snd_strict deflation_UU simp_thms}; + val deflation_rules = + @{thms conjI deflation_ID} + @ deflation_abs_rep_thms + @ DeflMapData.get thy; + in + Goal.prove_global thy [] assms goal (fn {prems, ...} => + EVERY + [simp_tac (HOL_basic_ss addsimps start_thms) 1, + rtac @{thm fix_ind} 1, + REPEAT (resolve_tac adm_rules 1), + simp_tac (HOL_basic_ss addsimps bottom_rules) 1, + simp_tac beta_ss 1, + simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1, + REPEAT (etac @{thm conjE} 1), + REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)]) + end; + val deflation_map_binds = dom_binds |> + map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map"); + val (deflation_map_thms, thy) = thy |> + (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context)) + (conjuncts deflation_map_binds deflation_map_thm); + val thy = DeflMapData.map (fold Thm.add_thm deflation_map_thms) thy; - (* define combined copy combinator *) - val ((c_const, c_def_thms), thy) = - if length doms = 1 - then ((hd copy_consts, []), thy) - else - let - val c_type = copy_arg_type ->> copy_arg_type; - val c_name = space_implode "_" (map Binding.name_of dom_binds); - val c_bind = Binding.name (c_name ^ "_copy"); - val c_body = - mk_tuple (map (mk_capply o rpair copy_arg) copy_consts); - val c_rhs = big_lambda copy_arg c_body; - val (c_const, thy) = - Sign.declare_const ((c_bind, c_type), NoSyn) thy; - val c_eqn = Logic.mk_equals (c_const, c_rhs); - val (c_def_thms, thy) = - thy - |> Sign.add_path c_name - |> (PureThy.add_defs false o map Thm.no_attributes) - [(Binding.name "copy_def", c_eqn)] - ||> Sign.parent_path; - in ((c_const, c_def_thms), thy) end; + (* definitions and proofs related to take functions *) + val (take_info, thy) = + define_take_functions (dom_binds ~~ iso_infos) thy; + val {take_consts, take_defs, chain_take_thms, take_0_thms, + take_Suc_thms, deflation_take_thms} = take_info; - (* fixed-point lemma for combined copy combinator *) - val fix_copy_lemma = + (* least-upper-bound lemma for take functions *) + val lub_take_lemma = let - fun mk_map_ID (map_const, (Type (c, Ts), rhsT)) = - Library.foldl mk_capply (map_const, map ID_const Ts); + val lhs = mk_tuple (map mk_lub take_consts); + fun mk_map_ID (map_const, (lhsT, rhsT)) = + list_ccomb (map_const, map mk_ID (snd (dest_Type lhsT))); val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns)); - val goal = mk_eqs (mk_fix c_const, rhs); - val rules = - [@{thm pair_collapse}, @{thm split_def}] - @ map_apply_thms - @ c_def_thms @ copy_defs - @ MapIdData.get thy; - val tac = simp_tac (beta_ss addsimps rules) 1; + val goal = mk_trp (mk_eq (lhs, rhs)); + val start_rules = + @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms + @ @{thms pair_collapse split_def} + @ map_apply_thms @ MapIdData.get thy; + val rules0 = + @{thms iterate_0 Pair_strict} @ take_0_thms; + val rules1 = + @{thms iterate_Suc Pair_fst_snd_eq fst_conv snd_conv} + @ take_Suc_thms; + val tac = + EVERY + [simp_tac (HOL_basic_ss addsimps start_rules) 1, + simp_tac (HOL_basic_ss addsimps @{thms fix_def2}) 1, + rtac @{thm lub_eq} 1, + rtac @{thm nat.induct} 1, + simp_tac (HOL_basic_ss addsimps rules0) 1, + asm_full_simp_tac (beta_ss addsimps rules1) 1]; in Goal.prove_global thy [] [] goal (K tac) end; - (* prove reach lemmas *) - val reach_thm_projs = - let fun mk_projs (x::[]) t = [(x, t)] - | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); - in mk_projs dom_binds (mk_fix c_const) end; - fun prove_reach_thm (((bind, t), map_ID_thm), (lhsT, rhsT)) thy = + (* prove lub of take equals ID *) + fun prove_lub_take (((bind, take_const), map_ID_thm), (lhsT, rhsT)) thy = let - val x = Free ("x", lhsT); - val goal = mk_eqs (mk_capply (t, x), x); - val rules = - fix_copy_lemma :: map_ID_thm :: @{thms fst_conv snd_conv ID1}; - val tac = simp_tac (HOL_basic_ss addsimps rules) 1; - val reach_thm = Goal.prove_global thy [] [] goal (K tac); + val i = Free ("i", natT); + val goal = mk_eqs (mk_lub (lambda i (take_const $ i)), mk_ID lhsT); + val tac = + EVERY + [rtac @{thm trans} 1, rtac map_ID_thm 2, + cut_facts_tac [lub_take_lemma] 1, + REPEAT (etac @{thm Pair_inject} 1), atac 1]; + val lub_take_thm = Goal.prove_global thy [] [] goal (K tac); in - thy - |> Sign.add_path (Binding.name_of bind) - |> yield_singleton (PureThy.add_thms o map Thm.no_attributes) - (Binding.name "reach", reach_thm) - ||> Sign.parent_path + add_qualified_thm "lub_take" (Binding.name_of bind, lub_take_thm) thy end; - val (reach_thms, thy) = thy |> - fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns); + val (lub_take_thms, thy) = + fold_map prove_lub_take + (dom_binds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy; in - thy + (iso_infos, thy) end; val domain_isomorphism = gen_domain_isomorphism cert_typ; -val domain_isomorphism_cmd = gen_domain_isomorphism read_typ; +val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ; (******************************************************************************) (******************************** outer syntax ********************************) diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Tools/Domain/domain_library.ML --- a/src/HOLCF/Tools/Domain/domain_library.ML Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Tue Mar 02 15:39:15 2010 +0100 @@ -5,36 +5,6 @@ *) -(* ----- general support ---------------------------------------------------- *) - -fun mapn f n [] = [] - | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; - -fun foldr'' f (l,f2) = - let fun itr [] = raise Fail "foldr''" - | itr [a] = f2 a - | itr (a::l) = f(a, itr l) - in itr l end; - -fun map_cumulr f start xs = - List.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => - (y::ys,res2)) ([],start) xs; - -fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; -fun upd_first f (x,y,z) = (f x, y, z); -fun upd_second f (x,y,z) = ( x, f y, z); -fun upd_third f (x,y,z) = ( x, y, f z); - -fun atomize ctxt thm = - let - val r_inst = read_instantiate ctxt; - fun at thm = - case concl_of thm of - _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) - | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) - | _ => [thm]; - in map zero_var_indexes (at thm) end; - (* infix syntax *) infixr 5 -->; @@ -44,8 +14,6 @@ infix 0 ==; infix 1 ===; infix 1 ~=; -infix 1 <<; -infix 1 ~<<; infix 9 ` ; infix 9 `% ; @@ -56,19 +24,25 @@ signature DOMAIN_LIBRARY = sig + val first : 'a * 'b * 'c -> 'a + val second : 'a * 'b * 'c -> 'b + val third : 'a * 'b * 'c -> 'c + val upd_second : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c + val upd_third : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd + val mapn : (int -> 'a -> 'b) -> int -> 'a list -> 'b list + val atomize : Proof.context -> thm -> thm list + val Imposs : string -> 'a; val cpo_type : theory -> typ -> bool; val pcpo_type : theory -> typ -> bool; val string_of_typ : theory -> typ -> string; (* Creating HOLCF types *) - val mk_cfunT : typ * typ -> typ; val ->> : typ * typ -> typ; val mk_ssumT : typ * typ -> typ; val mk_sprodT : typ * typ -> typ; val mk_uT : typ -> typ; val oneT : typ; - val trT : typ; val mk_maybeT : typ -> typ; val mk_ctupleT : typ list -> typ; val mk_TFree : string -> typ; @@ -81,26 +55,17 @@ val `% : term * string -> term; val /\ : string -> term -> term; val UU : term; - val TT : term; - val FF : term; val ID : term; val oo : term * term -> term; - val mk_up : term -> term; - val mk_sinl : term -> term; - val mk_sinr : term -> term; - val mk_stuple : term list -> term; val mk_ctuple : term list -> term; val mk_fix : term -> term; val mk_iterate : term * term * term -> term; val mk_fail : term; val mk_return : term -> term; val list_ccomb : term * term list -> term; - (* - val con_app : string -> ('a * 'b * string) list -> term; - *) val con_app2 : string -> ('a -> term) -> 'a list -> term; + val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a val proj : term -> 'a list -> int -> term; - val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a; val mk_ctuple_pat : term list -> term; val mk_branch : term -> term; @@ -111,15 +76,11 @@ val mk_lam : string * term -> term; val mk_all : string * term -> term; val mk_ex : string * term -> term; - val mk_constrain : typ * term -> term; val mk_constrainall : string * typ * term -> term; val === : term * term -> term; - val << : term * term -> term; - val ~<< : term * term -> term; val strict : term -> term; val defined : term -> term; val mk_adm : term -> term; - val mk_compact : term -> term; val lift : ('a -> term) -> 'a list * term -> term; val lift_defined : ('a -> term) -> 'a list * term -> term; @@ -162,12 +123,38 @@ val dis_name : string -> string; val mat_name : string -> string; val pat_name : string -> string; - val mk_var_names : string list -> string list; end; structure Domain_Library :> DOMAIN_LIBRARY = struct +fun first (x,_,_) = x; +fun second (_,x,_) = x; +fun third (_,_,x) = x; + +fun upd_first f (x,y,z) = (f x, y, z); +fun upd_second f (x,y,z) = ( x, f y, z); +fun upd_third f (x,y,z) = ( x, y, f z); + +fun mapn f n [] = [] + | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; + +fun foldr'' f (l,f2) = + let fun itr [] = raise Fail "foldr''" + | itr [a] = f2 a + | itr (a::l) = f(a, itr l) + in itr l end; + +fun atomize ctxt thm = + let + val r_inst = read_instantiate ctxt; + fun at thm = + case concl_of thm of + _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) + | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) + | _ => [thm]; + in map zero_var_indexes (at thm) end; + exception Impossible of string; fun Imposs msg = raise Impossible ("Domain:"^msg); @@ -191,22 +178,6 @@ fun pat_name con = (extern_name con) ^ "_pat"; fun pat_name_ con = (strip_esc con) ^ "_pat"; -(* make distinct names out of the type list, - forbidding "o","n..","x..","f..","P.." as names *) -(* a number string is added if necessary *) -fun mk_var_names ids : string list = - let - fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s; - fun index_vnames(vn::vns,occupied) = - (case AList.lookup (op =) occupied vn of - NONE => if vn mem vns - then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied) - else vn :: index_vnames(vns, occupied) - | SOME(i) => (vn^(string_of_int (i+1))) - :: index_vnames(vns,(vn,i+1)::occupied)) - | index_vnames([],occupied) = []; - in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end; - fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo}); fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo}); fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg; @@ -270,7 +241,6 @@ fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]); fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]); val oneT = @{typ one}; -val trT = @{typ tr}; val op ->> = mk_cfunT; @@ -290,7 +260,6 @@ fun mk_lam (x,T) = Abs(x,dummyT,T); fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); fun mk_ex (x,P) = mk_exists (x,dummyT,P); -val mk_constrain = uncurry TypeInfer.constrain; fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P))); end @@ -301,29 +270,18 @@ infix 0 ==; fun S == T = %%:"==" $ S $ T; infix 1 ===; fun S === T = %%:"op =" $ S $ T; infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T); -infix 1 <<; fun S << T = %%: @{const_name Porder.below} $ S $ T; -infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T); infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x; infix 9 `% ; fun f`% s = f` %: s; infix 9 `%%; fun f`%%s = f` %%:s; fun mk_adm t = %%: @{const_name adm} $ t; -fun mk_compact t = %%: @{const_name compact} $ t; val ID = %%: @{const_name ID}; fun mk_strictify t = %%: @{const_name strictify}`t; -(*val csplitN = "Cprod.csplit";*) -(*val sfstN = "Sprod.sfst";*) -(*val ssndN = "Sprod.ssnd";*) fun mk_ssplit t = %%: @{const_name ssplit}`t; -fun mk_sinl t = %%: @{const_name sinl}`t; -fun mk_sinr t = %%: @{const_name sinr}`t; fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y; -fun mk_up t = %%: @{const_name up}`t; fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u; val ONE = @{term ONE}; -val TT = @{term TT}; -val FF = @{term FF}; fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z; fun mk_fix t = %%: @{const_name fix}`t; fun mk_return t = %%: @{const_name Fixrec.return}`t; @@ -354,8 +312,6 @@ fun spair (t,u) = %%: @{const_name spair}`t`u; fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) | mk_ctuple ts = foldr1 cpair ts; -fun mk_stuple [] = ONE - | mk_stuple ts = foldr1 spair ts; fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; fun mk_maybeT T = Type ("Fixrec.maybe",[T]); diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Tools/Domain/domain_syntax.ML --- a/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 15:39:15 2010 +0100 @@ -9,14 +9,12 @@ val calc_syntax: theory -> bool -> - typ -> (string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list -> - (binding * typ * mixfix) list * ast Syntax.trrule list + (binding * typ * mixfix) list val add_syntax: bool -> - string -> ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list -> theory -> theory @@ -31,19 +29,15 @@ fun calc_syntax thy (definitional : bool) - (dtypeprod : typ) ((dname : string, typevars : typ list), (cons': (binding * (bool * binding option * typ) list * mixfix) list)) - : (binding * typ * mixfix) list * ast Syntax.trrule list = + : (binding * typ * mixfix) list = let (* ----- constants concerning the isomorphism ------------------------------- *) local fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t fun prod (_,args,_) = case args of [] => oneT | _ => foldr1 mk_sprodT (map opt_lazy args); - fun freetvar s = let val tvar = mk_TFree s in - if tvar mem typevars then freetvar ("t"^s) else tvar end; - fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args); in val dtype = Type(dname,typevars); val dtype2 = foldr1 mk_ssumT (map prod cons'); @@ -51,160 +45,28 @@ fun dbind s = Binding.name (dnam ^ s); val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn); val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn); - val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); - val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn); end; -(* ----- constants concerning constructors, discriminators, and selectors --- *) - - local - val escape = let - fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs - else c::esc cs - | esc [] = [] - in implode o esc o Symbol.explode end; - - fun dis_name_ con = - Binding.name ("is_" ^ strip_esc (Binding.name_of con)); - fun mat_name_ con = - Binding.name ("match_" ^ strip_esc (Binding.name_of con)); - fun pat_name_ con = - Binding.name (strip_esc (Binding.name_of con) ^ "_pat"); - fun con (name,args,mx) = - (name, List.foldr (op ->>) dtype (map third args), mx); - fun dis (con,args,mx) = - (dis_name_ con, dtype->>trT, - Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri)); - (* strictly speaking, these constants have one argument, - but the mixfix (without arguments) is introduced only - to generate parse rules for non-alphanumeric names*) - fun freetvar s n = - let val tvar = mk_TFree (s ^ string_of_int n) - in if tvar mem typevars then freetvar ("t"^s) n else tvar end; - - fun mk_matT (a,bs,c) = - a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; - fun mat (con,args,mx) = - (mat_name_ con, - mk_matT(dtype, map third args, freetvar "t" 1), - Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri)); - fun sel1 (_,sel,typ) = - Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; - fun sel (con,args,mx) = map_filter sel1 args; - fun mk_patT (a,b) = a ->> mk_maybeT b; - fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n); - fun pat (con,args,mx) = - (pat_name_ con, - (mapn pat_arg_typ 1 args) - ---> - mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))), - Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); - in - val consts_con = map con cons'; - val consts_dis = map dis cons'; - val consts_mat = map mat cons'; - val consts_pat = map pat cons'; - val consts_sel = maps sel cons'; - end; - -(* ----- constants concerning induction ------------------------------------- *) - - val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn); val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn); -(* ----- case translation --------------------------------------------------- *) - - fun syntax b = Syntax.mark_const (Sign.full_bname thy b); + val optional_consts = + if definitional then [] else [const_rep, const_abs]; - local open Syntax in - local - fun c_ast authentic con = Constant ((authentic ? syntax) (Binding.name_of con)); - fun expvar n = Variable ("e" ^ string_of_int n); - fun argvar n m _ = Variable ("a" ^ string_of_int n ^ "_" ^ string_of_int m); - fun argvars n args = mapn (argvar n) 1 args; - fun app s (l, r) = mk_appl (Constant s) [l, r]; - val cabs = app "_cabs"; - val capp = app @{const_syntax Rep_CFun}; - fun con1 authentic n (con,args,mx) = - Library.foldl capp (c_ast authentic con, argvars n args); - fun case1 authentic n (con,args,mx) = - app "_case1" (con1 authentic n (con,args,mx), expvar n); - fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args); - fun when1 n m = if n = m then arg1 n else K (Constant @{const_syntax UU}); - - fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"]; - fun app_pat x = mk_appl (Constant "_pat") [x]; - fun args_list [] = Constant "_noargs" - | args_list xs = foldr1 (app "_args") xs; - in - fun case_trans authentic = - ParsePrintRule - (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn (case1 authentic) 1 cons')), - capp (Library.foldl capp - (Constant (syntax (dnam ^ "_when")), mapn arg1 1 cons'), Variable "x")); - - fun one_abscon_trans authentic n (con,mx,args) = - ParsePrintRule - (cabs (con1 authentic n (con,mx,args), expvar n), - Library.foldl capp (Constant (syntax (dnam ^ "_when")), mapn (when1 n) 1 cons')); - fun abscon_trans authentic = mapn (one_abscon_trans authentic) 1 cons'; - - fun one_case_trans authentic (con,args,mx) = - let - val cname = c_ast authentic con; - val pname = Constant (syntax (strip_esc (Binding.name_of con) ^ "_pat")); - val ns = 1 upto length args; - val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; - val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; - val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; - in - [ParseRule (app_pat (Library.foldl capp (cname, xs)), - mk_appl pname (map app_pat xs)), - ParseRule (app_var (Library.foldl capp (cname, xs)), - app_var (args_list xs)), - PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)), - app "_match" (mk_appl pname ps, args_list vs))] - end; - val Case_trans = maps (one_case_trans false) cons' @ maps (one_case_trans true) cons'; - end; - end; - val optional_consts = - if definitional then [] else [const_rep, const_abs, const_copy]; - - in (optional_consts @ [const_when] @ - consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @ - [const_take, const_finite], - (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans))) + in (optional_consts @ [const_finite]) end; (* let *) (* ----- putting all the syntax stuff together ------------------------------ *) fun add_syntax (definitional : bool) - (comp_dnam : string) (eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list) (thy'' : theory) = let - val dtypes = map (Type o fst) eqs'; - val boolT = HOLogic.boolT; - val funprod = - foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes); - val relprod = - foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes); - val const_copy = - (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn); - val const_bisim = - (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn); - val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = - map (calc_syntax thy'' definitional funprod) eqs'; + val ctt : (binding * typ * mixfix) list list = + map (calc_syntax thy'' definitional) eqs'; in thy'' - |> Cont_Consts.add_consts - (maps fst ctt @ - (if length eqs'>1 andalso not definitional - then [const_copy] else []) @ - [const_bisim]) - |> Sign.add_trrules_i (maps snd ctt) + |> Cont_Consts.add_consts (flat ctt) end; (* let *) end; (* struct *) diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Mar 02 15:39:15 2010 +0100 @@ -9,7 +9,11 @@ signature DOMAIN_THEOREMS = sig - val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory; + val theorems: + Domain_Library.eq * Domain_Library.eq list + -> typ * (binding * (bool * binding option * typ) list * mixfix) list + -> theory -> thm list * theory; + val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory; val quiet_mode: bool Unsynchronized.ref; val trace_domain: bool Unsynchronized.ref; @@ -28,20 +32,11 @@ val adm_all = @{thm adm_all}; val adm_conj = @{thm adm_conj}; val adm_subst = @{thm adm_subst}; -val antisym_less_inverse = @{thm below_antisym_inverse}; -val beta_cfun = @{thm beta_cfun}; -val cfun_arg_cong = @{thm cfun_arg_cong}; val ch2ch_fst = @{thm ch2ch_fst}; val ch2ch_snd = @{thm ch2ch_snd}; val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL}; val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR}; val chain_iterate = @{thm chain_iterate}; -val compact_ONE = @{thm compact_ONE}; -val compact_sinl = @{thm compact_sinl}; -val compact_sinr = @{thm compact_sinr}; -val compact_spair = @{thm compact_spair}; -val compact_up = @{thm compact_up}; -val contlub_cfun_arg = @{thm contlub_cfun_arg}; val contlub_cfun_fun = @{thm contlub_cfun_fun}; val contlub_fst = @{thm contlub_fst}; val contlub_snd = @{thm contlub_snd}; @@ -52,35 +47,10 @@ val cont2cont_snd = @{thm cont2cont_snd}; val cont2cont_Rep_CFun = @{thm cont2cont_Rep_CFun}; val fix_def2 = @{thm fix_def2}; -val injection_eq = @{thm injection_eq}; -val injection_less = @{thm injection_below}; val lub_equal = @{thm lub_equal}; -val monofun_cfun_arg = @{thm monofun_cfun_arg}; val retraction_strict = @{thm retraction_strict}; -val spair_eq = @{thm spair_eq}; -val spair_less = @{thm spair_below}; -val sscase1 = @{thm sscase1}; -val ssplit1 = @{thm ssplit1}; -val strictify1 = @{thm strictify1}; val wfix_ind = @{thm wfix_ind}; - -val iso_intro = @{thm iso.intro}; -val iso_abs_iso = @{thm iso.abs_iso}; -val iso_rep_iso = @{thm iso.rep_iso}; -val iso_abs_strict = @{thm iso.abs_strict}; -val iso_rep_strict = @{thm iso.rep_strict}; -val iso_abs_defin' = @{thm iso.abs_defin'}; -val iso_rep_defin' = @{thm iso.rep_defin'}; -val iso_abs_defined = @{thm iso.abs_defined}; -val iso_rep_defined = @{thm iso.rep_defined}; -val iso_compact_abs = @{thm iso.compact_abs}; -val iso_compact_rep = @{thm iso.compact_rep}; -val iso_iso_swap = @{thm iso.iso_swap}; - -val exh_start = @{thm exh_start}; -val ex_defined_iffs = @{thms ex_defined_iffs}; -val exh_casedist0 = @{thm exh_casedist0}; -val exh_casedists = @{thms exh_casedists}; +val iso_intro = @{thm iso.intro}; open Domain_Library; infixr 0 ===>; @@ -118,6 +88,9 @@ else cut_facts_tac prems 1 :: tacsf context; in pg'' thy defs t tacs end; +(* FIXME!!!!!!!!! *) +(* We should NEVER re-parse variable names as strings! *) +(* The names can conflict with existing constants or other syntax! *) fun case_UU_tac ctxt rews i v = InductTacs.case_tac ctxt (v^"=UU") i THEN asm_simp_tac (HOLCF_ss addsimps rews) i; @@ -130,13 +103,13 @@ val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp} -val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)} - -fun theorems (((dname, _), cons) : eq, eqs : eq list) thy = +fun theorems + (((dname, _), cons) : eq, eqs : eq list) + (dom_eqn : typ * (binding * (bool * binding option * typ) list * mixfix) list) + (thy : theory) = let val _ = message ("Proving isomorphism properties of domain "^dname^" ..."); -val pg = pg' thy; val map_tab = Domain_Isomorphism.get_map_tab thy; @@ -147,515 +120,97 @@ in val ax_abs_iso = ga "abs_iso" dname; val ax_rep_iso = ga "rep_iso" dname; - val ax_when_def = ga "when_def" dname; - fun get_def mk_name (con, _, _) = ga (mk_name con^"_def") dname; - val axs_con_def = map (get_def extern_name) cons; - val axs_dis_def = map (get_def dis_name) cons; - val axs_mat_def = map (get_def mat_name) cons; - val axs_pat_def = map (get_def pat_name) cons; - val axs_sel_def = - let - fun def_of_sel sel = ga (sel^"_def") dname; - fun def_of_arg arg = Option.map def_of_sel (sel_of arg); - fun defs_of_con (_, _, args) = map_filter def_of_arg args; - in - maps defs_of_con cons - end; - val ax_copy_def = ga "copy_def" dname; + val ax_take_0 = ga "take_0" dname; + val ax_take_Suc = ga "take_Suc" dname; + val ax_take_strict = ga "take_strict" dname; end; (* local *) +(* ----- define constructors ------------------------------------------------ *) + +val lhsT = fst dom_eqn; + +val rhsT = + let + fun mk_arg_typ (lazy, sel, T) = if lazy then mk_uT T else T; + fun mk_con_typ (bind, args, mx) = + if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); + fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); + in + mk_eq_typ dom_eqn + end; + +val rep_const = Const(dname^"_rep", lhsT ->> rhsT); + +val abs_const = Const(dname^"_abs", rhsT ->> lhsT); + +val iso_info : Domain_Isomorphism.iso_info = + { + absT = lhsT, + repT = rhsT, + abs_const = abs_const, + rep_const = rep_const, + abs_inverse = ax_abs_iso, + rep_inverse = ax_rep_iso + }; + +val (result, thy) = + Domain_Constructors.add_domain_constructors + (Long_Name.base_name dname) (snd dom_eqn) iso_info thy; + +val con_appls = #con_betas result; +val {exhaust, casedist, ...} = result; +val {con_compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result; +val {sel_rews, ...} = result; +val when_rews = #cases result; +val when_strict = hd when_rews; +val dis_rews = #dis_rews result; +val mat_rews = #match_rews result; +val pat_rews = #pat_rews result; + (* ----- theorems concerning the isomorphism -------------------------------- *) -val dc_abs = %%:(dname^"_abs"); -val dc_rep = %%:(dname^"_rep"); +val pg = pg' thy; + val dc_copy = %%:(dname^"_copy"); -val x_name = "x"; -val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso]; val abs_strict = ax_rep_iso RS (allI RS retraction_strict); val rep_strict = ax_abs_iso RS (allI RS retraction_strict); -val abs_defin' = iso_locale RS iso_abs_defin'; -val rep_defin' = iso_locale RS iso_rep_defin'; val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict]; -(* ----- generating beta reduction rules from definitions-------------------- *) - -val _ = trace " Proving beta reduction rules..."; - -local - fun arglist (Const _ $ Abs (s, _, t)) = - let - val (vars,body) = arglist t; - in (s :: vars, body) end - | arglist t = ([], t); - fun bind_fun vars t = Library.foldr mk_All (vars, t); - fun bound_vars 0 = [] - | bound_vars i = Bound (i-1) :: bound_vars (i - 1); -in - fun appl_of_def def = - let - val (_ $ con $ lam) = concl_of def; - val (vars, rhs) = arglist lam; - val lhs = list_ccomb (con, bound_vars (length vars)); - val appl = bind_fun vars (lhs == rhs); - val cs = ContProc.cont_thms lam; - val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs; - in pg (def::betas) appl (K [rtac reflexive_thm 1]) end; -end; - -val _ = trace "Proving when_appl..."; -val when_appl = appl_of_def ax_when_def; -val _ = trace "Proving con_appls..."; -val con_appls = map appl_of_def axs_con_def; - -local - fun arg2typ n arg = - let val t = TVar (("'a", n), pcpoS) - in (n + 1, if is_lazy arg then mk_uT t else t) end; - - fun args2typ n [] = (n, oneT) - | args2typ n [arg] = arg2typ n arg - | args2typ n (arg::args) = - let - val (n1, t1) = arg2typ n arg; - val (n2, t2) = args2typ n1 args - in (n2, mk_sprodT (t1, t2)) end; - - fun cons2typ n [] = (n,oneT) - | cons2typ n [con] = args2typ n (third con) - | cons2typ n (con::cons) = - let - val (n1, t1) = args2typ n (third con); - val (n2, t2) = cons2typ n1 cons - in (n2, mk_ssumT (t1, t2)) end; -in - fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons)); -end; - -local - val iso_swap = iso_locale RS iso_iso_swap; - fun one_con (con, _, args) = - let - val vns = map vname args; - val eqn = %:x_name === con_app2 con %: vns; - val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args)); - in Library.foldr mk_ex (vns, conj) end; - - val conj_assoc = @{thm conj_assoc}; - val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons); - val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start; - val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1; - val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2; - - (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *) - val tacs = [ - rtac disjE 1, - etac (rep_defin' RS disjI1) 2, - etac disjI2 2, - rewrite_goals_tac [mk_meta_eq iso_swap], - rtac thm3 1]; -in - val _ = trace " Proving exhaust..."; - val exhaust = pg con_appls (mk_trp exh) (K tacs); - val _ = trace " Proving casedist..."; - val casedist = - Drule.export_without_context (rewrite_rule exh_casedists (exhaust RS exh_casedist0)); -end; - -local - fun bind_fun t = Library.foldr mk_All (when_funs cons, t); - fun bound_fun i _ = Bound (length cons - i); - val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons); -in - val _ = trace " Proving when_strict..."; - val when_strict = - let - val axs = [when_appl, mk_meta_eq rep_strict]; - val goal = bind_fun (mk_trp (strict when_app)); - val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1]; - in pg axs goal (K tacs) end; - - val _ = trace " Proving when_apps..."; - val when_apps = - let - fun one_when n (con, _, args) = - let - val axs = when_appl :: con_appls; - val goal = bind_fun (lift_defined %: (nonlazy args, - mk_trp (when_app`(con_app con args) === - list_ccomb (bound_fun n 0, map %# args)))); - val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1]; - in pg axs goal (K tacs) end; - in mapn one_when 1 cons end; -end; -val when_rews = when_strict :: when_apps; - -(* ----- theorems concerning the constructors, discriminators and selectors - *) - -local - fun dis_strict (con, _, _) = - let - val goal = mk_trp (strict (%%:(dis_name con))); - in pg axs_dis_def goal (K [rtac when_strict 1]) end; - - fun dis_app c (con, _, args) = - let - val lhs = %%:(dis_name c) ` con_app con args; - val rhs = if con = c then TT else FF; - val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_dis_def goal (K tacs) end; - - val _ = trace " Proving dis_apps..."; - val dis_apps = maps (fn (c,_,_) => map (dis_app c) cons) cons; - - fun dis_defin (con, _, args) = - let - val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name); - val tacs = - [rtac casedist 1, - contr_tac 1, - DETERM_UNTIL_SOLVED (CHANGED - (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))]; - in pg [] goal (K tacs) end; - - val _ = trace " Proving dis_stricts..."; - val dis_stricts = map dis_strict cons; - val _ = trace " Proving dis_defins..."; - val dis_defins = map dis_defin cons; -in - val dis_rews = dis_stricts @ dis_defins @ dis_apps; -end; - -local - fun mat_strict (con, _, _) = - let - val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU); - val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1]; - in pg axs_mat_def goal (K tacs) end; - - val _ = trace " Proving mat_stricts..."; - val mat_stricts = map mat_strict cons; - - fun one_mat c (con, _, args) = - let - val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs"; - val rhs = - if con = c - then list_ccomb (%:"rhs", map %# args) - else mk_fail; - val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_mat_def goal (K tacs) end; - - val _ = trace " Proving mat_apps..."; - val mat_apps = - maps (fn (c,_,_) => map (one_mat c) cons) cons; -in - val mat_rews = mat_stricts @ mat_apps; -end; - -local - fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - - fun pat_lhs (con,_,args) = mk_branch (list_comb (%%:(pat_name con), ps args)); - - fun pat_rhs (con,_,[]) = mk_return ((%:"rhs") ` HOLogic.unit) - | pat_rhs (con,_,args) = - (mk_branch (mk_ctuple_pat (ps args))) - `(%:"rhs")`(mk_ctuple (map %# args)); - - fun pat_strict c = - let - val axs = @{thm branch_def} :: axs_pat_def; - val goal = mk_trp (strict (pat_lhs c ` (%:"rhs"))); - val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1]; - in pg axs goal (K tacs) end; - - fun pat_app c (con, _, args) = - let - val axs = @{thm branch_def} :: axs_pat_def; - val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args); - val rhs = if con = first c then pat_rhs c else mk_fail; - val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs goal (K tacs) end; - - val _ = trace " Proving pat_stricts..."; - val pat_stricts = map pat_strict cons; - val _ = trace " Proving pat_apps..."; - val pat_apps = maps (fn c => map (pat_app c) cons) cons; -in - val pat_rews = pat_stricts @ pat_apps; -end; - -local - fun con_strict (con, _, args) = - let - val rules = abs_strict :: @{thms con_strict_rules}; - fun one_strict vn = - let - fun f arg = if vname arg = vn then UU else %# arg; - val goal = mk_trp (con_app2 con f args === UU); - val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; - in pg con_appls goal (K tacs) end; - in map one_strict (nonlazy args) end; - - fun con_defin (con, _, args) = - let - fun iff_disj (t, []) = HOLogic.mk_not t - | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts; - val lhs = con_app con args === UU; - val rhss = map (fn x => %:x === UU) (nonlazy args); - val goal = mk_trp (iff_disj (lhs, rhss)); - val rule1 = iso_locale RS @{thm iso.abs_defined_iff}; - val rules = rule1 :: @{thms con_defined_iff_rules}; - val tacs = [simp_tac (HOL_ss addsimps rules) 1]; - in pg con_appls goal (K tacs) end; -in - val _ = trace " Proving con_stricts..."; - val con_stricts = maps con_strict cons; - val _ = trace " Proving con_defins..."; - val con_defins = map con_defin cons; - val con_rews = con_stricts @ con_defins; -end; - -local - val rules = - [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE]; - fun con_compact (con, _, args) = - let - val concl = mk_trp (mk_compact (con_app con args)); - val goal = lift (fn x => mk_compact (%#x)) (args, concl); - val tacs = [ - rtac (iso_locale RS iso_compact_abs) 1, - REPEAT (resolve_tac rules 1 ORELSE atac 1)]; - in pg con_appls goal (K tacs) end; -in - val _ = trace " Proving con_compacts..."; - val con_compacts = map con_compact cons; -end; - -local - fun one_sel sel = - pg axs_sel_def (mk_trp (strict (%%:sel))) - (K [simp_tac (HOLCF_ss addsimps when_rews) 1]); - - fun sel_strict (_, _, args) = - map_filter (Option.map one_sel o sel_of) args; -in - val _ = trace " Proving sel_stricts..."; - val sel_stricts = maps sel_strict cons; -end; - -local - fun sel_app_same c n sel (con, args) = - let - val nlas = nonlazy args; - val vns = map vname args; - val vnn = List.nth (vns, n); - val nlas' = filter (fn v => v <> vnn) nlas; - val lhs = (%%:sel)`(con_app con args); - val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn)); - fun tacs1 ctxt = - if vnn mem nlas - then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn] - else []; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; - - fun sel_app_diff c n sel (con, args) = - let - val nlas = nonlazy args; - val goal = mk_trp (%%:sel ` con_app con args === UU); - fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; - - fun sel_app c n sel (con, _, args) = - if con = c - then sel_app_same c n sel (con, args) - else sel_app_diff c n sel (con, args); - - fun one_sel c n sel = map (sel_app c n sel) cons; - fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg); - fun one_con (c, _, args) = - flat (map_filter I (mapn (one_sel' c) 0 args)); -in - val _ = trace " Proving sel_apps..."; - val sel_apps = maps one_con cons; -end; - -local - fun sel_defin sel = - let - val goal = defined (%:x_name) ==> defined (%%:sel`%x_name); - val tacs = [ - rtac casedist 1, - contr_tac 1, - DETERM_UNTIL_SOLVED (CHANGED - (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))]; - in pg [] goal (K tacs) end; -in - val _ = trace " Proving sel_defins..."; - val sel_defins = - if length cons = 1 - then map_filter (fn arg => Option.map sel_defin (sel_of arg)) - (filter_out is_lazy (third (hd cons))) - else []; -end; - -val sel_rews = sel_stricts @ sel_defins @ sel_apps; - -val _ = trace " Proving dist_les..."; -val dist_les = - let - fun dist (con1, args1) (con2, args2) = - let - fun iff_disj (t, []) = HOLogic.mk_not t - | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts; - val lhs = con_app con1 args1 << con_app con2 args2; - val rhss = map (fn x => %:x === UU) (nonlazy args1); - val goal = mk_trp (iff_disj (lhs, rhss)); - val rule1 = iso_locale RS @{thm iso.abs_below}; - val rules = rule1 :: @{thms con_below_iff_rules}; - val tacs = [simp_tac (HOL_ss addsimps rules) 1]; - in pg con_appls goal (K tacs) end; - - fun distinct (con1, _, args1) (con2, _, args2) = - let - val arg1 = (con1, args1); - val arg2 = - (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) - (args2, Name.variant_list (map vname args1) (map vname args2))); - in [dist arg1 arg2, dist arg2 arg1] end; - fun distincts [] = [] - | distincts (c::cs) = maps (distinct c) cs @ distincts cs; - in distincts cons end; - -val _ = trace " Proving dist_eqs..."; -val dist_eqs = - let - fun dist (con1, args1) (con2, args2) = - let - fun iff_disj (t, [], us) = HOLogic.mk_not t - | iff_disj (t, ts, []) = HOLogic.mk_not t - | iff_disj (t, ts, us) = - let - val disj1 = foldr1 HOLogic.mk_disj ts; - val disj2 = foldr1 HOLogic.mk_disj us; - in t === HOLogic.mk_conj (disj1, disj2) end; - val lhs = con_app con1 args1 === con_app con2 args2; - val rhss1 = map (fn x => %:x === UU) (nonlazy args1); - val rhss2 = map (fn x => %:x === UU) (nonlazy args2); - val goal = mk_trp (iff_disj (lhs, rhss1, rhss2)); - val rule1 = iso_locale RS @{thm iso.abs_eq}; - val rules = rule1 :: @{thms con_eq_iff_rules}; - val tacs = [simp_tac (HOL_ss addsimps rules) 1]; - in pg con_appls goal (K tacs) end; - - fun distinct (con1, _, args1) (con2, _, args2) = - let - val arg1 = (con1, args1); - val arg2 = - (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) - (args2, Name.variant_list (map vname args1) (map vname args2))); - in [dist arg1 arg2, dist arg2 arg1] end; - fun distincts [] = [] - | distincts (c::cs) = maps (distinct c) cs @ distincts cs; - in distincts cons end; - -local - fun pgterm rel con args = - let - fun append s = upd_vname (fn v => v^s); - val (largs, rargs) = (args, map (append "'") args); - val concl = - foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs)); - val prem = rel (con_app con largs, con_app con rargs); - val sargs = case largs of [_] => [] | _ => nonlazy args; - val prop = lift_defined %: (sargs, mk_trp (prem === concl)); - in pg con_appls prop end; - val cons' = filter (fn (_, _, args) => args<>[]) cons; -in - val _ = trace " Proving inverts..."; - val inverts = - let - val abs_less = ax_abs_iso RS (allI RS injection_less); - val tacs = - [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1]; - in map (fn (con, _, args) => pgterm (op <<) con args (K tacs)) cons' end; - - val _ = trace " Proving injects..."; - val injects = - let - val abs_eq = ax_abs_iso RS (allI RS injection_eq); - val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1]; - in map (fn (con, _, args) => pgterm (op ===) con args (K tacs)) cons' end; -end; - (* ----- theorems concerning one induction step ----------------------------- *) -val copy_strict = - let - val _ = trace " Proving copy_strict..."; - val goal = mk_trp (strict (dc_copy `% "f")); - val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts}; - val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; - in - SOME (pg [ax_copy_def] goal (K tacs)) - handle - THM (s, _, _) => (trace s; NONE) - | ERROR s => (trace s; NONE) - end; +local + fun dc_take dn = %%:(dn^"_take"); + val dnames = map (fst o fst) eqs; + fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict"); + val axs_take_strict = map get_take_strict dnames; -local - fun copy_app (con, _, args) = + fun one_take_app (con, _, args) = let - val lhs = dc_copy`%"f"`(con_app con args); + fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; fun one_rhs arg = if Datatype_Aux.is_rec_type (dtyp_of arg) then Domain_Axioms.copy_of_dtyp map_tab - (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg) + mk_take (dtyp_of arg) ` (%# arg) else (%# arg); + val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args); val rhs = con_app2 con one_rhs args; fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg); fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); - val args' = filter_out (fn a => is_rec a orelse is_lazy a) args; - val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts}; - fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args'; - val rules = [ax_abs_iso] @ @{thms domain_map_simps}; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; - in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; + val goal = mk_trp (lhs === rhs); + val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}]; + val rules2 = @{thms take_con_rules ID1} @ axs_take_strict; + val tacs = + [simp_tac (HOL_basic_ss addsimps rules) 1, + asm_simp_tac (HOL_basic_ss addsimps rules2) 1]; + in pg con_appls goal (K tacs) end; + val take_apps = map (Drule.export_without_context o one_take_app) cons; in - val _ = trace " Proving copy_apps..."; - val copy_apps = map copy_app cons; + val take_rews = ax_take_0 :: ax_take_strict :: take_apps; end; -local - fun one_strict (con, _, args) = - let - val goal = mk_trp (dc_copy`UU`(con_app con args) === UU); - val rews = the_list copy_strict @ copy_apps @ con_rews; - fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @ - [asm_simp_tac (HOLCF_ss addsimps rews) 1]; - in - SOME (pg [] goal tacs) - handle - THM (s, _, _) => (trace s; NONE) - | ERROR s => (trace s; NONE) - end; - - fun has_nonlazy_rec (_, _, args) = exists is_nonlazy_rec args; -in - val _ = trace " Proving copy_stricts..."; - val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons); -end; - -val copy_rews = the_list copy_strict @ copy_apps @ copy_stricts; - in thy |> Sign.add_path (Long_Name.base_name dname) @@ -674,17 +229,16 @@ ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]), ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]), ((Binding.name "injects" , injects ), [Simplifier.simp_add]), - ((Binding.name "copy_rews" , copy_rews ), [Simplifier.simp_add]), + ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]), ((Binding.name "match_rews", mat_rews ), [Simplifier.simp_add, Fixrec.fixrec_simp_add])] |> Sign.parent_path |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ - pat_rews @ dist_les @ dist_eqs @ copy_rews) + pat_rews @ dist_les @ dist_eqs) end; (* let *) fun comp_theorems (comp_dnam, eqs: eq list) thy = let -val global_ctxt = ProofContext.init thy; val map_tab = Domain_Isomorphism.get_map_tab thy; val dnames = map (fst o fst) eqs; @@ -692,6 +246,81 @@ val comp_dname = Sign.full_bname thy comp_dnam; val _ = message ("Proving induction properties of domain "^comp_dname^" ..."); + +(* ----- define bisimulation predicate -------------------------------------- *) + +local + open HOLCF_Library + val dtypes = map (Type o fst) eqs; + val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes); + val bisim_bind = Binding.name (comp_dnam ^ "_bisim"); + val bisim_type = relprod --> boolT; +in + val (bisim_const, thy) = + Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy; +end; + +local + + fun legacy_infer_term thy t = + singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); + fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); + fun infer_props thy = map (apsnd (legacy_infer_prop thy)); + fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x); + fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; + + val comp_dname = Sign.full_bname thy comp_dnam; + val dnames = map (fst o fst) eqs; + val x_name = idx_name dnames "x"; + + fun one_con (con, _, args) = + let + val nonrec_args = filter_out is_rec args; + val rec_args = filter is_rec args; + val recs_cnt = length rec_args; + val allargs = nonrec_args @ rec_args + @ map (upd_vname (fn s=> s^"'")) rec_args; + val allvns = map vname allargs; + fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; + val vns1 = map (vname_arg "" ) args; + val vns2 = map (vname_arg "'") args; + val allargs_cnt = length nonrec_args + 2*recs_cnt; + val rec_idxs = (recs_cnt-1) downto 0; + val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) + (allargs~~((allargs_cnt-1) downto 0))); + fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ + Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); + val capps = + List.foldr + mk_conj + (mk_conj( + Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), + Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) + (mapn rel_app 1 rec_args); + in + List.foldr + mk_ex + (Library.foldr mk_conj + (map (defined o Bound) nonlazy_idxs,capps)) allvns + end; + fun one_comp n (_,cons) = + mk_all (x_name(n+1), + mk_all (x_name(n+1)^"'", + mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0, + foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) + ::map one_con cons)))); + val bisim_eqn = + %%:(comp_dname^"_bisim") == + mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)); + +in + val ([ax_bisim_def], thy) = + thy + |> Sign.add_path comp_dnam + |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)] + ||> Sign.parent_path; +end; (* local *) + val pg = pg' thy; (* ----- getting the composite axiom and definitions ------------------------ *) @@ -699,11 +328,10 @@ local fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); in - val axs_reach = map (ga "reach" ) dnames; val axs_take_def = map (ga "take_def" ) dnames; + val axs_chain_take = map (ga "chain_take") dnames; + val axs_lub_take = map (ga "lub_take" ) dnames; val axs_finite_def = map (ga "finite_def") dnames; - val ax_copy2_def = ga "copy_def" comp_dnam; - val ax_bisim_def = ga "bisim_def" comp_dnam; end; local @@ -712,7 +340,6 @@ in val cases = map (gt "casedist" ) dnames; val con_rews = maps (gts "con_rews" ) dnames; - val copy_rews = maps (gts "copy_rews") dnames; end; fun dc_take dn = %%:(dn^"_take"); @@ -722,64 +349,20 @@ (* ----- theorems concerning finite approximation and finite induction ------ *) -local - val iterate_Cprod_ss = global_simpset_of @{theory Fix}; - val copy_con_rews = copy_rews @ con_rews; - val copy_take_defs = - (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; - val _ = trace " Proving take_stricts..."; - fun one_take_strict ((dn, args), _) = - let - val goal = mk_trp (strict (dc_take dn $ %:"n")); - val rules = [ - @{thm monofun_fst [THEN monofunE]}, - @{thm monofun_snd [THEN monofunE]}]; - val tacs = [ - rtac @{thm UU_I} 1, - rtac @{thm below_eq_trans} 1, - resolve_tac axs_reach 2, - rtac @{thm monofun_cfun_fun} 1, - REPEAT (resolve_tac rules 1), - rtac @{thm iterate_below_fix} 1]; - in pg axs_take_def goal (K tacs) end; - val take_stricts = map one_take_strict eqs; - fun take_0 n dn = - let - val goal = mk_trp ((dc_take dn $ @{term "0::nat"}) `% x_name n === UU); - in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end; - val take_0s = mapn take_0 1 dnames; - val _ = trace " Proving take_apps..."; - fun one_take_app dn (con, _, args) = - let - fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; - fun one_rhs arg = - if Datatype_Aux.is_rec_type (dtyp_of arg) - then Domain_Axioms.copy_of_dtyp map_tab - mk_take (dtyp_of arg) ` (%# arg) - else (%# arg); - val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); - val rhs = con_app2 con one_rhs args; - fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg); - fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); - fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); - val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps copy_con_rews) 1]; - in pg copy_take_defs goal (K tacs) end; - fun one_take_apps ((dn, _), cons) = map (one_take_app dn) cons; - val take_apps = maps one_take_apps eqs; -in - val take_rews = map Drule.export_without_context - (take_stricts @ take_0s @ take_apps); -end; (* local *) +val take_rews = + maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; local fun one_con p (con, _, args) = let + val P_names = map P_name (1 upto (length dnames)); + val vns = Name.variant_list P_names (map vname args); + val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns)); fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); val t2 = lift ind_hyp (filter is_rec args, t1); - val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2); - in Library.foldr mk_All (map vname args, t3) end; + val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2); + in Library.foldr mk_All (vns, t3) end; fun one_eq ((p, cons), concl) = mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); @@ -787,7 +370,7 @@ fun ind_term concf = Library.foldr one_eq (mapn (fn n => fn x => (P_name n, x)) 1 conss, mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); - val take_ss = HOL_ss addsimps take_rews; + val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); fun quant_tac ctxt i = EVERY (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); @@ -838,6 +421,7 @@ simp_tac (take_ss addsimps prems) 1, TRY (safe_tac HOL_cs)]; fun arg_tac arg = + (* FIXME! case_UU_tac *) case_UU_tac context (prems @ con_rews) 1 (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); fun con_tacs (con, _, args) = @@ -860,31 +444,20 @@ val _ = trace " Proving take_lemmas..."; val take_lemmas = let - fun take_lemma n (dn, ax_reach) = - let - val lhs = dc_take dn $ Bound 0 `%(x_name n); - val rhs = dc_take dn $ Bound 0 `%(x_name n^"'"); - val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); - val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; - val rules = [contlub_fst RS contlubE RS ssubst, - contlub_snd RS contlubE RS ssubst]; - fun tacf {prems, context} = [ - res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1, - res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1, - stac fix_def2 1, - REPEAT (CHANGED - (resolve_tac rules 1 THEN chain_tac 1)), - stac contlub_cfun_fun 1, - stac contlub_cfun_fun 2, - rtac lub_equal 3, - chain_tac 1, - rtac allI 1, - resolve_tac prems 1]; - in pg'' thy axs_take_def goal tacf end; - in mapn take_lemma 1 (dnames ~~ axs_reach) end; + fun take_lemma (ax_chain_take, ax_lub_take) = + @{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]; + in map take_lemma (axs_chain_take ~~ axs_lub_take) end; + + val axs_reach = + let + fun reach (ax_chain_take, ax_lub_take) = + @{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]; + in map reach (axs_chain_take ~~ axs_lub_take) end; (* ----- theorems concerning finiteness and induction ----------------------- *) + val global_ctxt = ProofContext.init thy; + val _ = trace " Proving finites, ind..."; val (finites, ind) = ( @@ -948,6 +521,7 @@ let val goal = mk_trp (%%:(dn^"_finite") $ %:"x"); fun tacs ctxt = [ + (* FIXME! case_UU_tac *) case_UU_tac ctxt take_rews 1 "x", eresolve_tac finite_lemmas1a 1, step_tac HOL_cs 1, @@ -990,22 +564,28 @@ val cont_rules = [cont_id, cont_const, cont2cont_Rep_CFun, cont2cont_fst, cont2cont_snd]; + val subgoal = + let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n)); + in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end; + val subgoal' = legacy_infer_term thy subgoal; fun tacf {prems, context} = - map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ - quant_tac context 1, - rtac (adm_impl_admw RS wfix_ind) 1, - REPEAT_DETERM (rtac adm_all 1), - REPEAT_DETERM ( - TRY (rtac adm_conj 1) THEN - rtac adm_subst 1 THEN - REPEAT (resolve_tac cont_rules 1) THEN - resolve_tac prems 1), - strip_tac 1, - rtac (rewrite_rule axs_take_def finite_ind) 1, - ind_prems_tac prems]; + let + val subtac = + EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems]; + val subthm = Goal.prove context [] [] subgoal' (K subtac); + in + map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ + cut_facts_tac (subthm :: take (length dnames) prems) 1, + REPEAT (rtac @{thm conjI} 1 ORELSE + EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1, + resolve_tac axs_chain_take 1, + asm_simp_tac HOL_basic_ss 1]) + ] + end; val ind = (pg'' thy [] goal tacf handle ERROR _ => - (warning "Cannot prove infinite induction rule"; TrueI)); + (warning "Cannot prove infinite induction rule"; TrueI) + ); in (finites, ind) end ) handle THM _ => @@ -1013,7 +593,6 @@ | ERROR _ => (warning "Cannot prove induction rule"; ([], TrueI)); - end; (* local *) (* ----- theorem concerning coinduction ------------------------------------- *) @@ -1021,7 +600,7 @@ local val xs = mapn (fn n => K (x_name n)) 1 dnames; fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); - val take_ss = HOL_ss addsimps take_rews; + val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); val _ = trace " Proving coind_lemma..."; val coind_lemma = @@ -1075,8 +654,8 @@ in thy |> Sign.add_path comp_dnam |> snd o PureThy.add_thmss [ - ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]), ((Binding.name "take_lemmas", take_lemmas ), []), + ((Binding.name "reach" , axs_reach ), []), ((Binding.name "finites" , finites ), []), ((Binding.name "finite_ind" , [finite_ind]), []), ((Binding.name "ind" , [ind] ), []), diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/Tools/holcf_library.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/holcf_library.ML Tue Mar 02 15:39:15 2010 +0100 @@ -0,0 +1,250 @@ +(* Title: HOLCF/Tools/holcf_library.ML + Author: Brian Huffman + +Functions for constructing HOLCF types and terms. +*) + +structure HOLCF_Library = +struct + +infixr 6 ->>; +infix -->>; + +(*** Operations from Isabelle/HOL ***) + +val boolT = HOLogic.boolT; +val natT = HOLogic.natT; + +val mk_equals = Logic.mk_equals; +val mk_eq = HOLogic.mk_eq; +val mk_trp = HOLogic.mk_Trueprop; +val mk_fst = HOLogic.mk_fst; +val mk_snd = HOLogic.mk_snd; +val mk_not = HOLogic.mk_not; +val mk_conj = HOLogic.mk_conj; +val mk_disj = HOLogic.mk_disj; + +fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t; + + +(*** Basic HOLCF concepts ***) + +fun mk_bottom T = Const (@{const_name UU}, T); + +fun below_const T = Const (@{const_name below}, [T, T] ---> boolT); +fun mk_below (t, u) = below_const (fastype_of t) $ t $ u; + +fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t)); + +fun mk_defined t = mk_not (mk_undef t); + +fun mk_compact t = + Const (@{const_name compact}, fastype_of t --> boolT) $ t; + +fun mk_cont t = + Const (@{const_name cont}, fastype_of t --> boolT) $ t; + +fun mk_chain t = + Const (@{const_name chain}, Term.fastype_of t --> boolT) $ t; + + +(*** Continuous function space ***) + +(* ->> is taken from holcf_logic.ML *) +fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]); + +val (op ->>) = mk_cfunT; +val (op -->>) = Library.foldr mk_cfunT; + +fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) + | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); + +fun capply_const (S, T) = + Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T)); + +fun cabs_const (S, T) = + Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T)); + +fun mk_cabs t = + let val T = fastype_of t + in cabs_const (Term.domain_type T, Term.range_type T) $ t end + +(* builds the expression (% v1 v2 .. vn. rhs) *) +fun lambdas [] rhs = rhs + | lambdas (v::vs) rhs = Term.lambda v (lambdas vs rhs); + +(* builds the expression (LAM v. rhs) *) +fun big_lambda v rhs = + cabs_const (fastype_of v, fastype_of rhs) $ Term.lambda v rhs; + +(* builds the expression (LAM v1 v2 .. vn. rhs) *) +fun big_lambdas [] rhs = rhs + | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); + +fun mk_capply (t, u) = + let val (S, T) = + case fastype_of t of + Type(@{type_name "->"}, [S, T]) => (S, T) + | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); + in capply_const (S, T) $ t $ u end; + +infix 9 ` ; val (op `) = mk_capply; + +val list_ccomb : term * term list -> term = Library.foldl mk_capply; + +fun mk_ID T = Const (@{const_name ID}, T ->> T); + +fun cfcomp_const (T, U, V) = + Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V)); + +fun mk_cfcomp (f, g) = + let + val (U, V) = dest_cfunT (fastype_of f); + val (T, U') = dest_cfunT (fastype_of g); + in + if U = U' + then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g) + else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) + end; + +fun mk_strict t = + let val (T, U) = dest_cfunT (fastype_of t); + in mk_eq (t ` mk_bottom T, mk_bottom U) end; + + +(*** Product type ***) + +val mk_prodT = HOLogic.mk_prodT + +fun mk_tupleT [] = HOLogic.unitT + | mk_tupleT [T] = T + | mk_tupleT (T :: Ts) = mk_prodT (T, mk_tupleT Ts); + +(* builds the expression (v1,v2,..,vn) *) +fun mk_tuple [] = HOLogic.unit + | mk_tuple (t::[]) = t + | mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts); + +(* builds the expression (%(v1,v2,..,vn). rhs) *) +fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs + | lambda_tuple (v::[]) rhs = Term.lambda v rhs + | lambda_tuple (v::vs) rhs = + HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)); + + +(*** Lifted cpo type ***) + +fun mk_upT T = Type(@{type_name "u"}, [T]); + +fun dest_upT (Type(@{type_name "u"}, [T])) = T + | dest_upT T = raise TYPE ("dest_upT", [T], []); + +fun up_const T = Const(@{const_name up}, T ->> mk_upT T); + +fun mk_up t = up_const (fastype_of t) ` t; + +fun fup_const (T, U) = + Const(@{const_name fup}, (T ->> U) ->> mk_upT T ->> U); + +fun from_up T = fup_const (T, T) ` mk_ID T; + + +(*** Strict product type ***) + +val oneT = @{typ "one"}; + +fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]); + +fun dest_sprodT (Type(@{type_name "**"}, [T, U])) = (T, U) + | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []); + +fun spair_const (T, U) = + Const(@{const_name spair}, T ->> U ->> mk_sprodT (T, U)); + +(* builds the expression (:t, u:) *) +fun mk_spair (t, u) = + spair_const (fastype_of t, fastype_of u) ` t ` u; + +(* builds the expression (:t1,t2,..,tn:) *) +fun mk_stuple [] = @{term "ONE"} + | mk_stuple (t::[]) = t + | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts); + +fun sfst_const (T, U) = + Const(@{const_name sfst}, mk_sprodT (T, U) ->> T); + +fun ssnd_const (T, U) = + Const(@{const_name ssnd}, mk_sprodT (T, U) ->> U); + + +(*** Strict sum type ***) + +fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]); + +fun dest_ssumT (Type(@{type_name "++"}, [T, U])) = (T, U) + | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []); + +fun sinl_const (T, U) = Const(@{const_name sinl}, T ->> mk_ssumT (T, U)); +fun sinr_const (T, U) = Const(@{const_name sinr}, U ->> mk_ssumT (T, U)); + +(* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *) +fun mk_sinjects ts = + let + val Ts = map fastype_of ts; + fun combine (t, T) (us, U) = + let + val v = sinl_const (T, U) ` t; + val vs = map (fn u => sinr_const (T, U) ` u) us; + in + (v::vs, mk_ssumT (T, U)) + end + fun inj [] = error "mk_sinjects: empty list" + | inj ((t, T)::[]) = ([t], T) + | inj ((t, T)::ts) = combine (t, T) (inj ts); + in + fst (inj (ts ~~ Ts)) + end; + +fun sscase_const (T, U, V) = + Const(@{const_name sscase}, + (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V); + +fun from_sinl (T, U) = + sscase_const (T, U, T) ` mk_ID T ` mk_bottom (U ->> T); + +fun from_sinr (T, U) = + sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U; + + +(*** pattern match monad type ***) + +fun mk_matchT T = Type (@{type_name "maybe"}, [T]); + +fun dest_matchT (Type(@{type_name "maybe"}, [T])) = T + | dest_matchT T = raise TYPE ("dest_matchT", [T], []); + +fun mk_fail T = Const (@{const_name "Fixrec.fail"}, mk_matchT T); + +fun return_const T = Const (@{const_name "Fixrec.return"}, T ->> mk_matchT T); +fun mk_return t = return_const (fastype_of t) ` t; + + +(*** lifted boolean type ***) + +val trT = @{typ "tr"}; + + +(*** theory of fixed points ***) + +fun mk_fix t = + let val (T, _) = dest_cfunT (fastype_of t) + in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end; + +fun iterate_const T = + Const (@{const_name iterate}, natT --> (T ->> T) ->> (T ->> T)); + +fun mk_iterate (n, f) = + let val (T, _) = dest_cfunT (Term.fastype_of f); + in (iterate_const T $ n) ` f ` mk_bottom T end; + +end; diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/ex/Dnat.thy --- a/src/HOLCF/ex/Dnat.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/ex/Dnat.thy Tue Mar 02 15:39:15 2010 +0100 @@ -62,10 +62,10 @@ apply (rule allI) apply (rule_tac x = y in dnat.casedist) apply (fast intro!: UU_I) - apply (thin_tac "ALL y. d << y --> d = UU | d = y") + apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y") apply simp apply (simp (no_asm_simp)) - apply (drule_tac x="da" in spec) + apply (drule_tac x="dnata" in spec) apply simp done diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/ex/Domain_Proofs.thy --- a/src/HOLCF/ex/Domain_Proofs.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/ex/Domain_Proofs.thy Tue Mar 02 15:39:15 2010 +0100 @@ -196,7 +196,7 @@ by (rule bar_defl_unfold) lemma REP_baz': "REP('a baz) = REP(('a foo convex_pd \ tr)\<^sub>\)" -unfolding REP_foo REP_bar REP_baz REP_simps +unfolding REP_foo REP_bar REP_baz REP_simps REP_convex by (rule baz_defl_unfold) (********************************************************************) diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/ex/Domain_ex.thy --- a/src/HOLCF/ex/Domain_ex.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/ex/Domain_ex.thy Tue Mar 02 15:39:15 2010 +0100 @@ -99,7 +99,7 @@ text {* Trivial datatypes will produce a warning message. *} -domain triv = triv1 triv triv +domain triv = Triv triv triv -- "domain Domain_ex.triv is empty!" lemma "(x::triv) = \" by (induct x, simp_all) @@ -122,7 +122,7 @@ text {* Rules about constructors *} term Leaf term Node -thm tree.Leaf_def tree.Node_def +thm Leaf_def Node_def thm tree.exhaust thm tree.casedist thm tree.compacts @@ -134,7 +134,7 @@ text {* Rules about case combinator *} term tree_when -thm tree.when_def +thm tree.tree_when_def thm tree.when_rews text {* Rules about selectors *} @@ -157,16 +157,17 @@ term match_Node thm tree.match_rews -text {* Rules about copy function *} -term tree_copy -thm tree.copy_def -thm tree.copy_rews - text {* Rules about take function *} term tree_take thm tree.take_def +thm tree.take_0 +thm tree.take_Suc thm tree.take_rews +thm tree.chain_take +thm tree.take_take +thm tree.deflation_take thm tree.take_lemmas +thm tree.reach thm tree.finite_ind text {* Rules about finiteness predicate *} diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/ex/New_Domain.thy --- a/src/HOLCF/ex/New_Domain.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/ex/New_Domain.thy Tue Mar 02 15:39:15 2010 +0100 @@ -51,12 +51,12 @@ thm ltree.reach text {* - The definition of the copy function uses map functions associated with + The definition of the take function uses map functions associated with each type constructor involved in the definition. A map function for the lazy list type has been generated by the new domain package. *} -thm ltree.copy_def +thm ltree.take_rews thm llist_map_def lemma ltree_induct: @@ -67,24 +67,24 @@ assumes Branch: "\f l. \x. P (f\x) \ P (Branch\(llist_map\f\l))" shows "P x" proof - - have "\x. P (fix\ltree_copy\x)" - proof (rule fix_ind) - show "adm (\a. \x. P (a\x))" - by (simp add: adm_subst [OF _ adm]) - next - show "\x. P (\\x)" - by (simp add: bot) - next - fix f :: "'a ltree \ 'a ltree" - assume f: "\x. P (f\x)" - show "\x. P (ltree_copy\f\x)" - apply (rule allI) - apply (case_tac x) - apply (simp add: bot) - apply (simp add: Leaf) - apply (simp add: Branch [OF f]) - done - qed + have "P (\i. ltree_take i\x)" + using adm + proof (rule admD) + fix i + show "P (ltree_take i\x)" + proof (induct i arbitrary: x) + case (0 x) + show "P (ltree_take 0\x)" by (simp add: bot) + next + case (Suc n x) + show "P (ltree_take (Suc n)\x)" + apply (cases x) + apply (simp add: bot) + apply (simp add: Leaf) + apply (simp add: Branch Suc) + done + qed + qed (simp add: ltree.chain_take) thus ?thesis by (simp add: ltree.reach) qed diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/ex/Stream.thy Tue Mar 02 15:39:15 2010 +0100 @@ -143,16 +143,10 @@ lemma stream_reach2: "(LUB i. stream_take i$s) = s" -apply (insert stream.reach [of s], erule subst) back -apply (simp add: fix_def2 stream.take_def) -apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym]) -by simp +by (rule stream.reach) lemma chain_stream_take: "chain (%i. stream_take i$s)" -apply (rule chainI) -apply (rule monofun_cfun_fun) -apply (simp add: stream.take_def del: iterate_Suc) -by (rule chainE, simp) +by (simp add: stream.chain_take) lemma stream_take_prefix [simp]: "stream_take n$s << s" apply (insert stream_reach2 [of s]) @@ -259,10 +253,9 @@ lemma stream_ind2: "[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s) |] ==> P x" apply (insert stream.reach [of x],erule subst) -apply (frule adm_impl_admw, rule wfix_ind, auto) -apply (rule adm_subst [THEN adm_impl_admw],auto) +apply (erule admD, rule chain_stream_take) apply (insert stream_finite_ind2 [of P]) -by (simp add: stream.take_def) +by simp @@ -275,16 +268,9 @@ lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R" apply (simp add: stream.bisim_def,clarsimp) - apply (case_tac "x=UU",clarsimp) - apply (erule_tac x="UU" in allE,simp) - apply (case_tac "x'=UU",simp) - apply (drule stream_exhaust_eq [THEN iffD1],auto)+ - apply (case_tac "x'=UU",auto) - apply (erule_tac x="a && y" in allE) - apply (erule_tac x="UU" in allE)+ - apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp) - apply (erule_tac x="a && y" in allE) - apply (erule_tac x="aa && ya" in allE) back + apply (drule spec, drule spec, drule (1) mp) + apply (case_tac "x", simp) + apply (case_tac "x'", simp) by auto @@ -379,8 +365,8 @@ lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \ | #y < Fin (Suc n))" apply (rule stream.casedist [of x], auto) apply (simp add: zero_inat_def) - apply (case_tac "#s") apply (simp_all add: iSuc_Fin) - apply (case_tac "#s") apply (simp_all add: iSuc_Fin) + apply (case_tac "#stream") apply (simp_all add: iSuc_Fin) + apply (case_tac "#stream") apply (simp_all add: iSuc_Fin) done lemma slen_take_lemma4 [rule_format]: diff -r 118cda173627 -r 5d88ffdb290c src/HOLCF/ex/Strict_Fun.thy --- a/src/HOLCF/ex/Strict_Fun.thy Tue Mar 02 15:39:06 2010 +0100 +++ b/src/HOLCF/ex/Strict_Fun.thy Tue Mar 02 15:39:15 2010 +0100 @@ -232,8 +232,8 @@ setup {* Domain_Isomorphism.add_type_constructor - (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, - @{thm REP_sfun}, @{thm isodefl_sfun}, @{thm sfun_map_ID}) + (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm REP_sfun}, + @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map}) *} end