1(* Title: HOL/Prolog/prolog.ML 2 Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) 3*) 4 5Options.default_put_bool \<^system_option>\<open>show_main_goal\<close> true; 6 7structure Prolog = 8struct 9 10exception not_HOHH; 11 12fun isD t = case t of 13 Const(\<^const_name>\<open>Trueprop\<close>,_)$t => isD t 14 | Const(\<^const_name>\<open>HOL.conj\<close> ,_)$l$r => isD l andalso isD r 15 | Const(\<^const_name>\<open>HOL.implies\<close>,_)$l$r => isG l andalso isD r 16 | Const(\<^const_name>\<open>Pure.imp\<close>,_)$l$r => isG l andalso isD r 17 | Const(\<^const_name>\<open>All\<close>,_)$Abs(s,_,t) => isD t 18 | Const(\<^const_name>\<open>Pure.all\<close>,_)$Abs(s,_,t) => isD t 19 | Const(\<^const_name>\<open>HOL.disj\<close>,_)$_$_ => false 20 | Const(\<^const_name>\<open>Ex\<close> ,_)$_ => false 21 | Const(\<^const_name>\<open>Not\<close>,_)$_ => false 22 | Const(\<^const_name>\<open>True\<close>,_) => false 23 | Const(\<^const_name>\<open>False\<close>,_) => false 24 | l $ r => isD l 25 | Const _ (* rigid atom *) => true 26 | Bound _ (* rigid atom *) => true 27 | Free _ (* rigid atom *) => true 28 | _ (* flexible atom, 29 anything else *) => false 30and 31 isG t = case t of 32 Const(\<^const_name>\<open>Trueprop\<close>,_)$t => isG t 33 | Const(\<^const_name>\<open>HOL.conj\<close> ,_)$l$r => isG l andalso isG r 34 | Const(\<^const_name>\<open>HOL.disj\<close> ,_)$l$r => isG l andalso isG r 35 | Const(\<^const_name>\<open>HOL.implies\<close>,_)$l$r => isD l andalso isG r 36 | Const(\<^const_name>\<open>Pure.imp\<close>,_)$l$r => isD l andalso isG r 37 | Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,t) => isG t 38 | Const(\<^const_name>\<open>Pure.all\<close>,_)$Abs(_,_,t) => isG t 39 | Const(\<^const_name>\<open>Ex\<close> ,_)$Abs(_,_,t) => isG t 40 | Const(\<^const_name>\<open>True\<close>,_) => true 41 | Const(\<^const_name>\<open>Not\<close>,_)$_ => false 42 | Const(\<^const_name>\<open>False\<close>,_) => false 43 | _ (* atom *) => true; 44 45val check_HOHH_tac1 = PRIMITIVE (fn thm => 46 if isG (Thm.concl_of thm) then thm else raise not_HOHH); 47val check_HOHH_tac2 = PRIMITIVE (fn thm => 48 if forall isG (Thm.prems_of thm) then thm else raise not_HOHH); 49fun check_HOHH thm = (if isD (Thm.concl_of thm) andalso forall isG (Thm.prems_of thm) 50 then thm else raise not_HOHH); 51 52fun atomizeD ctxt thm = 53 let 54 fun at thm = case Thm.concl_of thm of 55 _$(Const(\<^const_name>\<open>All\<close> ,_)$Abs(s,_,_))=> 56 let val s' = if s="P" then "PP" else s in 57 at(thm RS (Rule_Insts.read_instantiate ctxt [((("x", 0), Position.none), s')] [s'] spec)) 58 end 59 | _$(Const(\<^const_name>\<open>HOL.conj\<close>,_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) 60 | _$(Const(\<^const_name>\<open>HOL.implies\<close>,_)$_$_) => at(thm RS mp) 61 | _ => [thm] 62 in map zero_var_indexes (at thm) end; 63 64val atomize_ss = 65 (empty_simpset \<^context> |> Simplifier.set_mksimps (mksimps mksimps_pairs)) 66 addsimps [ 67 @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) 68 @{thm imp_conjL} RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *) 69 @{thm imp_conjR}, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *) 70 @{thm imp_all}] (* "((!x. D) :- G) = (!x. D :- G)" *) 71 |> simpset_of; 72 73 74(*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} => 75 resolve_tac (maps atomizeD prems) 1); 76 -- is nice, but cannot instantiate unknowns in the assumptions *) 77fun hyp_resolve_tac ctxt = SUBGOAL (fn (subgoal, i) => 78 let 79 fun ap (Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t)) 80 | ap (Const(\<^const_name>\<open>HOL.implies\<close>,_)$_$t) =(case ap t of (k,_,t) => (k,true ,t)) 81 | ap t = (0,false,t); 82(* 83 fun rep_goal (Const (@{const_name Pure.all},_)$Abs (_,_,t)) = rep_goal t 84 | rep_goal (Const (@{const_name Pure.imp},_)$s$t) = 85 (case rep_goal t of (l,t) => (s::l,t)) 86 | rep_goal t = ([] ,t); 87 val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal 88 (#3(dest_state (st,i))); 89*) 90 val prems = Logic.strip_assums_hyp subgoal; 91 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal); 92 fun drot_tac k i = DETERM (rotate_tac k i); 93 fun spec_tac 0 i = all_tac 94 | spec_tac k i = EVERY' [dresolve_tac ctxt [spec], drot_tac ~1, spec_tac (k-1)] i; 95 fun dup_spec_tac k i = if k = 0 then all_tac else EVERY' 96 [DETERM o (eresolve_tac ctxt [all_dupE]), drot_tac ~2, spec_tac (k-1)] i; 97 fun same_head _ (Const (x,_)) (Const (y,_)) = x = y 98 | same_head k (s$_) (t$_) = same_head k s t 99 | same_head k (Bound i) (Bound j) = i = j + k 100 | same_head _ _ _ = true; 101 fun mapn f n [] = [] 102 | mapn f n (x::xs) = f n x::mapn f (n+1) xs; 103 fun pres_tac (k,arrow,t) n i = drot_tac n i THEN ( 104 if same_head k t concl 105 then dup_spec_tac k i THEN 106 (if arrow then eresolve_tac ctxt [mp] i THEN drot_tac (~n) i else assume_tac ctxt i) 107 else no_tac); 108 val ptacs = mapn (fn n => fn t => 109 pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems; 110 in Library.foldl (op APPEND) (no_tac, ptacs) end); 111 112fun ptac ctxt prog = let 113 val proga = maps (atomizeD ctxt) prog (* atomize the prog *) 114 in (REPEAT_DETERM1 o FIRST' [ 115 resolve_tac ctxt [TrueI], (* "True" *) 116 resolve_tac ctxt [conjI], (* "[| P; Q |] ==> P & Q" *) 117 resolve_tac ctxt [allI], (* "(!!x. P x) ==> ! x. P x" *) 118 resolve_tac ctxt [exI], (* "P x ==> ? x. P x" *) 119 resolve_tac ctxt [impI] THEN' (* "(P ==> Q) ==> P --> Q" *) 120 asm_full_simp_tac (put_simpset atomize_ss ctxt) THEN' (* atomize the asms *) 121 (REPEAT_DETERM o (eresolve_tac ctxt [conjE])) (* split the asms *) 122 ]) 123 ORELSE' resolve_tac ctxt [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*) 124 ORELSE' ((resolve_tac ctxt proga APPEND' hyp_resolve_tac ctxt) 125 THEN' (fn _ => check_HOHH_tac2)) 126end; 127 128fun prolog_tac ctxt prog = 129 check_HOHH_tac1 THEN 130 DEPTH_SOLVE (ptac ctxt (map check_HOHH prog) 1); 131 132val prog_HOHH = []; 133 134end; 135