Hello Bill,
On 07/04/2013 05:22, Bill Richter wrote: > I wonder if you could translate part of > Examples/inverse_bug_puzzle_tac.ml > from the latest subversion (159) into you IsabelleLight framework. > I tried a couple of the proofs: reachableNSymmetry and FourStepMoveABBAreach. I have included some extra code that needs to be included because I implemented it recently and haven't gotten around to sending it to John yet. I tried as much as possible not to change the proofs (I haven't read what they mean anyway), and simply used Isabelle Light's tools to perform the same steps. Isabelle Light tactics can be used at the same level as normal HOL Light tactics, so it is up to you to decide what you find more elegant in each case. For example, (rule impI) is equivalent to DISCH_TAC and (fun x -> rule_tac [`a`,x] exI) is equivalent to MATCH_EXISTS_TAC. Also, you lose some of the labelling functionality that you have from the recently added tactics (HYP, INTRO_TAC etc). It would take a bit of work to build this into Isabelle Light which I'm hoping to find some time to do. Hope this helps get a better idea about the library. As a side note, I suggest you rename your "cases" tactic because you are overriding the "cases" function of HOL Light (http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/cases.html). Regards, Petros needs "IsabelleLight/make.ml";; needs "Examples/inverse_bug_puzzle_tac.ml";; (* Some extra code that normally belongs to Isabelle Light: *) let try_type tp tm = try inst (type_match (type_of tm) tp []) tm with Failure _ -> tm;; let (X_MATCH_GEN_TAC: term -> tactic), (X_MATCH_CHOOSE_TAC: term -> thm_tactic), (MATCH_EXISTS_TAC: term -> tactic) = let tactic_type_compatibility_check pfx e g = let et = type_of e in let g' = try_type et g in let gt = type_of g' in if et = gt then g' else failwith(pfx ^ ": expected type :"^string_of_type et^" but got :"^ string_of_type gt) in let X_MATCH_GEN_TAC x' = if not(is_var x') then failwith "X_GEN_TAC: not a variable" else fun (asl,w) -> let x,bod = try dest_forall w with Failure _ -> failwith "X_GEN_TAC: Not universally quantified" in let x'' = tactic_type_compatibility_check "X_GEN_TAC" x x' in let avoids = itlist (union o thm_frees o snd) asl (frees w) in if mem x'' avoids then failwith "X_GEN_TAC: invalid variable" else let afn = CONV_RULE(GEN_ALPHA_CONV x) in null_meta,[asl,vsubst[x'',x] bod], fun i [th] -> afn (GEN x'' th) and X_MATCH_CHOOSE_TAC x' xth = let xtm = concl xth in let x,bod = try dest_exists xtm with Failure _ -> failwith "X_CHOOSE_TAC: not existential" in let x'' = tactic_type_compatibility_check "X_CHOOSE_TAC" x x' in let pat = vsubst[x'',x] bod in let xth' = ASSUME pat in fun (asl,w) -> let avoids = itlist (union o frees o concl o snd) asl (union (frees w) (thm_frees xth)) in if mem x'' avoids then failwith "X_CHOOSE_TAC: invalid variable" else null_meta,[("",xth')::asl,w], fun i [th] -> CHOOSE(x'',INSTANTIATE_ALL i xth) th and MATCH_EXISTS_TAC t (asl,w) = let v,bod = try dest_exists w with Failure _ -> failwith "EXISTS_TAC: Goal not existentially quantified" in let t' = tactic_type_compatibility_check "EXISTS_TAC" v t in null_meta,[asl,vsubst[t',v] bod], fun i [th] -> EXISTS (instantiate i w,instantiate i t') th in X_MATCH_GEN_TAC,X_MATCH_CHOOSE_TAC,MATCH_EXISTS_TAC;; (* reachableNSymmetry using Isabelle Light tactics: *) let reachableNSymmetry = prove (`! n. ! A B C A' B' C'. reachableN (A,B,C) (A',B',C') n ==> reachableN (B,C,A) (B',C',A') n /\ reachableN (C,A,B) (C',A',B') n /\ reachableN (A,C,B) (A',C',B') n /\ reachableN (B,A,C) (B',A',C') n /\ reachableN (C,B,A) (C',B',A') n`, MATCH_MP_TAC num_INDUCTION THEN simp[reachableN_CLAUSES;PAIR_EQ] THEN allI THEN rule impI THEN REPEAT allI THEN simp[LEFT_IMP_EXISTS_THM; FORALL_PAIR_THM] THEN MAP_EVERY X_MATCH_GEN_TAC [`X`; `Y`; `Z`] THEN rule impI THEN simp[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM] THEN MAP_EVERY (fun x -> rule_tac [`a`,x] exI) [`(Y,Z,X)`; `(Z,X,Y)`; `(X,Z,Y)`; `(Y,X,Z)`; `(Z,Y,X)`] THEN simp[moveSymmetry]);; (* Broken down version: *) g (`! n. ! A B C A' B' C'. reachableN (A,B,C) (A',B',C') n ==> reachableN (B,C,A) (B',C',A') n /\ reachableN (C,A,B) (C',A',B') n /\ reachableN (A,C,B) (A',C',B') n /\ reachableN (B,A,C) (B',A',C') n /\ reachableN (C,B,A) (C',B',A') n`);; e (MATCH_MP_TAC num_INDUCTION THEN simp[reachableN_CLAUSES;PAIR_EQ]);; e allI;; e (rule impI);; e (REPEAT allI);; e (simp[LEFT_IMP_EXISTS_THM; FORALL_PAIR_THM]);; e (MAP_EVERY X_MATCH_GEN_TAC [`X`; `Y`; `Z`]);; e (rule impI);; e (simp[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM]);; e (MAP_EVERY (fun x -> rule_tac [`a`,x] exI) [`(Y,Z,X)`; `(Z,X,Y)`; `(X,Z,Y)`; `(Y,X,Z)`; `(Z,Y,X)`]);; e (simp[moveSymmetry]);; (* FourStepMoveABBAreach using Isabelle Light tactics: *) let FourStepMoveABBAreach = prove (`!A B C A' B'. ~collinear {A,B,C} /\ move2Cond A B A' B' ==> ? Y. reachableN (A,B,C) (A',B',Y) 4`, REPEAT allI THEN rule impI THEN erule conjE THEN drule ((MIMP_RULE o fst o EQ_IMP_RULE o SPEC_ALL) move2Cond) THEN erule disjE THENL [ meson[FourStepMoveAB; reachableN_Four] ; subgoal_tac `~collinear {B,(A:real^2),C}` ] THENL [ meson[collinearSymmetry] ; drule_tac [(`A`,`B`);(`A'`,`B'`);(`B'`,`A'`)] ((MIMP_RULE o SPEC_ALL) FourStepMoveAB) ] THENL [ assumption ; meson[moveSymmetry; reachableN_Four]]);; (* Broken down version: *) g (`!A B C A' B'. ~collinear {A,B,C} /\ move2Cond A B A' B' ==> ? Y. reachableN (A,B,C) (A',B',Y) 4`);; e (REPEAT allI);; e (rule impI);; e (erule conjE);; e (drule ((MIMP_RULE o fst o EQ_IMP_RULE o SPEC_ALL) move2Cond));; e (erule disjE);; e (meson[FourStepMoveAB; reachableN_Four]);; e (subgoal_tac `~collinear {B,(A:real^2),C}`);; e (meson[collinearSymmetry]);; e (drule_tac [(`A`,`B`);(`A'`,`B'`);(`B'`,`A'`)] ((MIMP_RULE o SPEC_ALL) FourStepMoveAB));; e (assumption);; e (meson[moveSymmetry; reachableN_Four]);; -- Petros Papapanagiotou CISA, School of Informatics The University of Edinburgh Email: p.papapanagio...@sms.ed.ac.uk --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
