src/HOL/Prolog/HOHH.ML
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 15570 8d8c70b41bab
child 17311 5b1d47d920ce
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:    HOL/Prolog/HOHH.ML
     2     ID:       $Id$
     3     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     4 *)
     5 
     6 open HOHH;
     7 
     8 exception not_HOHH;
     9 
    10 fun isD t = case t of 
    11     Const("Trueprop",_)$t     => isD t
    12   | Const("op &"  ,_)$l$r     => isD l andalso isD r
    13   | Const("op -->",_)$l$r     => isG l andalso isD r
    14   | Const(   "==>",_)$l$r     => isG l andalso isD r
    15   | Const("All",_)$Abs(s,_,t) => isD t
    16   | Const("all",_)$Abs(s,_,t) => isD t
    17   | Const("op |",_)$_$_       => false
    18   | Const("Ex" ,_)$_          => false
    19   | Const("not",_)$_          => false
    20   | Const("True",_)           => false
    21   | Const("False",_)          => false
    22   | l $ r                     => isD l
    23   | Const _ (* rigid atom *)  => true
    24   | Bound _ (* rigid atom *)  => true
    25   | Free  _ (* rigid atom *)  => true
    26   | _    (* flexible atom,
    27 	    anything else *)  => false
    28 and
    29     isG t = case t of
    30     Const("Trueprop",_)$t     => isG t
    31   | Const("op &"  ,_)$l$r     => isG l andalso isG r
    32   | Const("op |"  ,_)$l$r     => isG l andalso isG r
    33   | Const("op -->",_)$l$r     => isD l andalso isG r
    34   | Const(   "==>",_)$l$r     => isD l andalso isG r
    35   | Const("All",_)$Abs(_,_,t) => isG t
    36   | Const("all",_)$Abs(_,_,t) => isG t
    37   | Const("Ex" ,_)$Abs(_,_,t) => isG t
    38   | Const("True",_)           => true
    39   | Const("not",_)$_          => false
    40   | Const("False",_)          => false
    41   | _ (* atom *)	      => true;
    42 
    43 val check_HOHH_tac1 = PRIMITIVE (fn thm => 
    44 	if isG (concl_of thm) then thm else raise not_HOHH);
    45 val check_HOHH_tac2 = PRIMITIVE (fn thm => 
    46 	if forall isG (prems_of thm) then thm else raise not_HOHH);
    47 fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm) 
    48 			then thm else raise not_HOHH);
    49 
    50 fun atomizeD thm = let 
    51     fun at  thm = case concl_of thm of
    52       _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
    53 					"?"^(if s="P" then "PP" else s))] spec))
    54     | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    55     | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
    56     | _				    => [thm]
    57 in map zero_var_indexes (at thm) end;
    58 
    59 val atomize_ss = empty_ss setmksimps (mksimps mksimps_pairs) addsimps [
    60 	all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    61 	imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    62 	imp_conjR,	  (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    63 	imp_all];	  (* "((!x. D) :- G) = (!x. D :- G)" *)
    64 
    65 (*val hyp_resolve_tac = METAHYPS (fn prems => 
    66 				  resolve_tac (List.concat (map atomizeD prems)) 1);
    67   -- is nice, but cannot instantiate unknowns in the assumptions *)
    68 fun hyp_resolve_tac i st = let
    69 	fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    70 	|   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    71 	|   ap t			  = 			    (0,false,t);
    72 (*
    73 	fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
    74 	|   rep_goal (Const ("==>",_)$s$t)	   = 
    75 			(case rep_goal t of (l,t) => (s::l,t))
    76 	|   rep_goal t				   = ([]  ,t);
    77 	val (prems, Const("Trueprop", _)$concl) = rep_goal 
    78 						(#3(dest_state (st,i)));
    79 *)
    80 	val subgoal = #3(dest_state (st,i));
    81 	val prems = Logic.strip_assums_hyp subgoal;
    82 	val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
    83 	fun drot_tac k i = DETERM (rotate_tac k i);
    84 	fun spec_tac 0 i = all_tac
    85 	|   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
    86 	fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
    87 		      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
    88 	fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
    89 	|   same_head k (s$_)         (t$_)	    = same_head k s t
    90 	|   same_head k (Bound i)     (Bound j)	    = i = j + k
    91 	|   same_head _ _             _             = true;
    92 	fun mapn f n []      = []
    93 	|   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
    94 	fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
    95 		if same_head k t concl
    96 		then dup_spec_tac k i THEN 
    97 		     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
    98 		else no_tac);
    99 	val ptacs = mapn (fn n => fn t => 
   100 			  pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
   101 	in Library.foldl (op APPEND) (no_tac, ptacs) st end;
   102 
   103 fun ptac prog = let
   104   val proga = List.concat (map atomizeD prog)			(* atomize the prog *)
   105   in	(REPEAT_DETERM1 o FIRST' [
   106 		rtac TrueI,			(* "True" *)
   107 		rtac conjI,			(* "[| P; Q |] ==> P & Q" *)
   108 		rtac allI,			(* "(!!x. P x) ==> ! x. P x" *)
   109 		rtac exI,			(* "P x ==> ? x. P x" *)
   110 		rtac impI THEN'			(* "(P ==> Q) ==> P --> Q" *)
   111 		  asm_full_simp_tac atomize_ss THEN'	(* atomize the asms *)
   112 		  (REPEAT_DETERM o (etac conjE))	(* split the asms *)
   113 		]) 
   114 	ORELSE' resolve_tac [disjI1,disjI2]	(* "P ==> P | Q","Q ==> P | Q"*)
   115 	ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
   116 		 THEN' (fn _ => check_HOHH_tac2))
   117 end;
   118 
   119 fun prolog_tac prog = check_HOHH_tac1 THEN 
   120 		      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
   121 
   122 val prog_HOHH = [];