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