converted to Isar theory format;
authorwenzelm
Wed Sep 07 21:07:09 2005 +0200 (2005-09-07)
changeset 173115b1d47d920ce
parent 17310 1322ed8e0ee4
child 17312 159783c74f75
converted to Isar theory format;
src/HOL/Prolog/Func.ML
src/HOL/Prolog/Func.thy
src/HOL/Prolog/HOHH.ML
src/HOL/Prolog/HOHH.thy
src/HOL/Prolog/Test.ML
src/HOL/Prolog/Test.thy
src/HOL/Prolog/Type.thy
     1.1 --- a/src/HOL/Prolog/Func.ML	Wed Sep 07 21:00:30 2005 +0200
     1.2 +++ b/src/HOL/Prolog/Func.ML	Wed Sep 07 21:07:09 2005 +0200
     1.3 @@ -3,8 +3,6 @@
     1.4      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     1.5  *)
     1.6  
     1.7 -open Func;
     1.8 -
     1.9  val prog_Func = prog_HOHH @ [eval];
    1.10  fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
    1.11  val p = ptac prog_Func 1;
    1.12 @@ -12,6 +10,4 @@
    1.13  pgoal "eval ((S (S Z)) + (S Z)) ?X";
    1.14  
    1.15  pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
    1.16 -			\(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
    1.17 -
    1.18 -
    1.19 +                        \(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
     2.1 --- a/src/HOL/Prolog/Func.thy	Wed Sep 07 21:00:30 2005 +0200
     2.2 +++ b/src/HOL/Prolog/Func.thy	Wed Sep 07 21:07:09 2005 +0200
     2.3 @@ -1,40 +1,41 @@
     2.4  (*  Title:    HOL/Prolog/Func.thy
     2.5      ID:       $Id$
     2.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     2.7 -
     2.8 -untyped functional language, with call by value semantics 
     2.9  *)
    2.10  
    2.11 -Func = HOHH +
    2.12 +header {* Untyped functional language, with call by value semantics *}
    2.13  
    2.14 -types tm
    2.15 -
    2.16 -arities tm :: type
    2.17 +theory Func
    2.18 +imports HOHH
    2.19 +begin
    2.20  
    2.21 -consts	abs	:: (tm => tm) => tm
    2.22 -	app	:: tm => tm => tm
    2.23 +typedecl tm
    2.24  
    2.25 -	cond	:: tm => tm => tm => tm
    2.26 -	fix	:: (tm => tm) => tm
    2.27 +consts
    2.28 +  abs     :: "(tm => tm) => tm"
    2.29 +  app     :: "tm => tm => tm"
    2.30 +
    2.31 +  cond    :: "tm => tm => tm => tm"
    2.32 +  "fix"   :: "(tm => tm) => tm"
    2.33  
    2.34 -	true,
    2.35 -	false	:: tm
    2.36 -	"and"	:: tm => tm => tm	(infixr 999)
    2.37 -	"eq"	:: tm => tm => tm	(infixr 999)
    2.38 +  true    :: tm
    2.39 +  false   :: tm
    2.40 +  "and"   :: "tm => tm => tm"       (infixr 999)
    2.41 +  "eq"    :: "tm => tm => tm"       (infixr 999)
    2.42  
    2.43 -	"0"	:: tm			("Z")
    2.44 -	S	:: tm => tm
    2.45 +  "0"     :: tm                   ("Z")
    2.46 +  S       :: "tm => tm"
    2.47  (*
    2.48 -	"++", "--",
    2.49 -	"**"	:: tm => tm => tm	(infixr 999)
    2.50 +        "++", "--",
    2.51 +        "**"    :: tm => tm => tm       (infixr 999)
    2.52  *)
    2.53 -	eval	:: [tm, tm] => bool
    2.54 +        eval    :: "[tm, tm] => bool"
    2.55  
    2.56 -arities tm :: plus
    2.57 -arities tm :: minus
    2.58 -arities tm :: times
    2.59 +instance tm :: plus ..
    2.60 +instance tm :: minus ..
    2.61 +instance tm :: times ..
    2.62  
    2.63 -rules	eval "
    2.64 +axioms   eval: "
    2.65  
    2.66  eval (abs RR) (abs RR)..
    2.67  eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V..
    2.68 @@ -47,7 +48,7 @@
    2.69  eval false false..
    2.70  eval (P and Q) true  :- eval P true  & eval Q true ..
    2.71  eval (P and Q) false :- eval P false | eval Q false..
    2.72 -eval (A1 eq B1) true  :- eval A1 C1 & eval B1 C1.. 
    2.73 +eval (A1 eq B1) true  :- eval A1 C1 & eval B1 C1..
    2.74  eval (A2 eq B2) false :- True..
    2.75  
    2.76  eval Z Z..
    2.77 @@ -59,4 +60,6 @@
    2.78  eval ( Z    * M) Z..
    2.79  eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
    2.80  
    2.81 +ML {* use_legacy_bindings (the_context ()) *}
    2.82 +
    2.83  end
     3.1 --- a/src/HOL/Prolog/HOHH.ML	Wed Sep 07 21:00:30 2005 +0200
     3.2 +++ b/src/HOL/Prolog/HOHH.ML	Wed Sep 07 21:07:09 2005 +0200
     3.3 @@ -3,11 +3,9 @@
     3.4      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     3.5  *)
     3.6  
     3.7 -open HOHH;
     3.8 -
     3.9  exception not_HOHH;
    3.10  
    3.11 -fun isD t = case t of 
    3.12 +fun isD t = case t of
    3.13      Const("Trueprop",_)$t     => isD t
    3.14    | Const("op &"  ,_)$l$r     => isD l andalso isD r
    3.15    | Const("op -->",_)$l$r     => isG l andalso isD r
    3.16 @@ -24,7 +22,7 @@
    3.17    | Bound _ (* rigid atom *)  => true
    3.18    | Free  _ (* rigid atom *)  => true
    3.19    | _    (* flexible atom,
    3.20 -	    anything else *)  => false
    3.21 +            anything else *)  => false
    3.22  and
    3.23      isG t = case t of
    3.24      Const("Trueprop",_)$t     => isG t
    3.25 @@ -38,85 +36,85 @@
    3.26    | Const("True",_)           => true
    3.27    | Const("not",_)$_          => false
    3.28    | Const("False",_)          => false
    3.29 -  | _ (* atom *)	      => true;
    3.30 +  | _ (* atom *)              => true;
    3.31  
    3.32 -val check_HOHH_tac1 = PRIMITIVE (fn thm => 
    3.33 -	if isG (concl_of thm) then thm else raise not_HOHH);
    3.34 -val check_HOHH_tac2 = PRIMITIVE (fn thm => 
    3.35 -	if forall isG (prems_of thm) then thm else raise not_HOHH);
    3.36 -fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm) 
    3.37 -			then thm else raise not_HOHH);
    3.38 +val check_HOHH_tac1 = PRIMITIVE (fn thm =>
    3.39 +        if isG (concl_of thm) then thm else raise not_HOHH);
    3.40 +val check_HOHH_tac2 = PRIMITIVE (fn thm =>
    3.41 +        if forall isG (prems_of thm) then thm else raise not_HOHH);
    3.42 +fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
    3.43 +                        then thm else raise not_HOHH);
    3.44  
    3.45 -fun atomizeD thm = let 
    3.46 +fun atomizeD thm = let
    3.47      fun at  thm = case concl_of thm of
    3.48        _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
    3.49 -					"?"^(if s="P" then "PP" else s))] spec))
    3.50 +                                        "?"^(if s="P" then "PP" else s))] spec))
    3.51      | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    3.52      | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
    3.53 -    | _				    => [thm]
    3.54 +    | _                             => [thm]
    3.55  in map zero_var_indexes (at thm) end;
    3.56  
    3.57  val atomize_ss = empty_ss setmksimps (mksimps mksimps_pairs) addsimps [
    3.58 -	all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    3.59 -	imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    3.60 -	imp_conjR,	  (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    3.61 -	imp_all];	  (* "((!x. D) :- G) = (!x. D :- G)" *)
    3.62 +        all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    3.63 +        imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    3.64 +        imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    3.65 +        imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
    3.66  
    3.67 -(*val hyp_resolve_tac = METAHYPS (fn prems => 
    3.68 -				  resolve_tac (List.concat (map atomizeD prems)) 1);
    3.69 +(*val hyp_resolve_tac = METAHYPS (fn prems =>
    3.70 +                                  resolve_tac (List.concat (map atomizeD prems)) 1);
    3.71    -- is nice, but cannot instantiate unknowns in the assumptions *)
    3.72  fun hyp_resolve_tac i st = let
    3.73 -	fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    3.74 -	|   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    3.75 -	|   ap t			  = 			    (0,false,t);
    3.76 +        fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    3.77 +        |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    3.78 +        |   ap t                          =                         (0,false,t);
    3.79  (*
    3.80 -	fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
    3.81 -	|   rep_goal (Const ("==>",_)$s$t)	   = 
    3.82 -			(case rep_goal t of (l,t) => (s::l,t))
    3.83 -	|   rep_goal t				   = ([]  ,t);
    3.84 -	val (prems, Const("Trueprop", _)$concl) = rep_goal 
    3.85 -						(#3(dest_state (st,i)));
    3.86 +        fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
    3.87 +        |   rep_goal (Const ("==>",_)$s$t)         =
    3.88 +                        (case rep_goal t of (l,t) => (s::l,t))
    3.89 +        |   rep_goal t                             = ([]  ,t);
    3.90 +        val (prems, Const("Trueprop", _)$concl) = rep_goal
    3.91 +                                                (#3(dest_state (st,i)));
    3.92  *)
    3.93 -	val subgoal = #3(dest_state (st,i));
    3.94 -	val prems = Logic.strip_assums_hyp subgoal;
    3.95 -	val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
    3.96 -	fun drot_tac k i = DETERM (rotate_tac k i);
    3.97 -	fun spec_tac 0 i = all_tac
    3.98 -	|   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
    3.99 -	fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
   3.100 -		      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
   3.101 -	fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
   3.102 -	|   same_head k (s$_)         (t$_)	    = same_head k s t
   3.103 -	|   same_head k (Bound i)     (Bound j)	    = i = j + k
   3.104 -	|   same_head _ _             _             = true;
   3.105 -	fun mapn f n []      = []
   3.106 -	|   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
   3.107 -	fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
   3.108 -		if same_head k t concl
   3.109 -		then dup_spec_tac k i THEN 
   3.110 -		     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
   3.111 -		else no_tac);
   3.112 -	val ptacs = mapn (fn n => fn t => 
   3.113 -			  pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
   3.114 -	in Library.foldl (op APPEND) (no_tac, ptacs) st end;
   3.115 +        val subgoal = #3(dest_state (st,i));
   3.116 +        val prems = Logic.strip_assums_hyp subgoal;
   3.117 +        val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
   3.118 +        fun drot_tac k i = DETERM (rotate_tac k i);
   3.119 +        fun spec_tac 0 i = all_tac
   3.120 +        |   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
   3.121 +        fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
   3.122 +                      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
   3.123 +        fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
   3.124 +        |   same_head k (s$_)         (t$_)         = same_head k s t
   3.125 +        |   same_head k (Bound i)     (Bound j)     = i = j + k
   3.126 +        |   same_head _ _             _             = true;
   3.127 +        fun mapn f n []      = []
   3.128 +        |   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
   3.129 +        fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
   3.130 +                if same_head k t concl
   3.131 +                then dup_spec_tac k i THEN
   3.132 +                     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
   3.133 +                else no_tac);
   3.134 +        val ptacs = mapn (fn n => fn t =>
   3.135 +                          pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
   3.136 +        in Library.foldl (op APPEND) (no_tac, ptacs) st end;
   3.137  
   3.138  fun ptac prog = let
   3.139 -  val proga = List.concat (map atomizeD prog)			(* atomize the prog *)
   3.140 -  in	(REPEAT_DETERM1 o FIRST' [
   3.141 -		rtac TrueI,			(* "True" *)
   3.142 -		rtac conjI,			(* "[| P; Q |] ==> P & Q" *)
   3.143 -		rtac allI,			(* "(!!x. P x) ==> ! x. P x" *)
   3.144 -		rtac exI,			(* "P x ==> ? x. P x" *)
   3.145 -		rtac impI THEN'			(* "(P ==> Q) ==> P --> Q" *)
   3.146 -		  asm_full_simp_tac atomize_ss THEN'	(* atomize the asms *)
   3.147 -		  (REPEAT_DETERM o (etac conjE))	(* split the asms *)
   3.148 -		]) 
   3.149 -	ORELSE' resolve_tac [disjI1,disjI2]	(* "P ==> P | Q","Q ==> P | Q"*)
   3.150 -	ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
   3.151 -		 THEN' (fn _ => check_HOHH_tac2))
   3.152 +  val proga = List.concat (map atomizeD prog)                   (* atomize the prog *)
   3.153 +  in    (REPEAT_DETERM1 o FIRST' [
   3.154 +                rtac TrueI,                     (* "True" *)
   3.155 +                rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
   3.156 +                rtac allI,                      (* "(!!x. P x) ==> ! x. P x" *)
   3.157 +                rtac exI,                       (* "P x ==> ? x. P x" *)
   3.158 +                rtac impI THEN'                 (* "(P ==> Q) ==> P --> Q" *)
   3.159 +                  asm_full_simp_tac atomize_ss THEN'    (* atomize the asms *)
   3.160 +                  (REPEAT_DETERM o (etac conjE))        (* split the asms *)
   3.161 +                ])
   3.162 +        ORELSE' resolve_tac [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
   3.163 +        ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
   3.164 +                 THEN' (fn _ => check_HOHH_tac2))
   3.165  end;
   3.166  
   3.167 -fun prolog_tac prog = check_HOHH_tac1 THEN 
   3.168 -		      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
   3.169 +fun prolog_tac prog = check_HOHH_tac1 THEN
   3.170 +                      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
   3.171  
   3.172  val prog_HOHH = [];
     4.1 --- a/src/HOL/Prolog/HOHH.thy	Wed Sep 07 21:00:30 2005 +0200
     4.2 +++ b/src/HOL/Prolog/HOHH.thy	Wed Sep 07 21:07:09 2005 +0200
     4.3 @@ -1,29 +1,30 @@
     4.4  (*  Title:    HOL/Prolog/HOHH.thy
     4.5      ID:       $Id$
     4.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     4.7 -
     4.8 -higher-order hereditary Harrop formulas 
     4.9  *)
    4.10  
    4.11 -HOHH = HOL +
    4.12 +header {* Higher-order hereditary Harrop formulas *}
    4.13 +
    4.14 +theory HOHH
    4.15 +imports HOL
    4.16 +begin
    4.17  
    4.18  consts
    4.19  
    4.20 -(* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A		*)
    4.21 -  "Dand"	:: [bool, bool] => bool		(infixr ".." 28)
    4.22 -  ":-"		:: [bool, bool] => bool		(infixl 29)
    4.23 +(* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A            *)
    4.24 +  "Dand"        :: "[bool, bool] => bool"         (infixr ".." 28)
    4.25 +  ":-"          :: "[bool, bool] => bool"         (infixl 29)
    4.26  
    4.27 -(* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G 
    4.28 -			       | True | !x. G | D => G			*)
    4.29 -(*","           :: [bool, bool] => bool		(infixr 35)*)
    4.30 -  "=>"		:: [bool, bool] => bool		(infixr 27)
    4.31 +(* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G
    4.32 +                               | True | !x. G | D => G                  *)
    4.33 +(*","           :: "[bool, bool] => bool"         (infixr 35)*)
    4.34 +  "=>"          :: "[bool, bool] => bool"         (infixr 27)
    4.35  
    4.36  translations
    4.37  
    4.38 -  "D :- G"	=>	"G --> D"
    4.39 -  "D1 .. D2"	=>	"D1 & D2"
    4.40 -(*"G1 , G2"	=>	"G1 & G2"*)
    4.41 -  "D => G"	=>	"D --> G"
    4.42 +  "D :- G"      =>      "G --> D"
    4.43 +  "D1 .. D2"    =>      "D1 & D2"
    4.44 +(*"G1 , G2"     =>      "G1 & G2"*)
    4.45 +  "D => G"      =>      "D --> G"
    4.46  
    4.47  end
    4.48 -
     5.1 --- a/src/HOL/Prolog/Test.ML	Wed Sep 07 21:00:30 2005 +0200
     5.2 +++ b/src/HOL/Prolog/Test.ML	Wed Sep 07 21:07:09 2005 +0200
     5.3 @@ -3,8 +3,6 @@
     5.4      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     5.5  *)
     5.6  
     5.7 -open Test;
     5.8 -
     5.9  val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
    5.10  fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test));
    5.11  val p = ptac prog_Test 1;
    5.12 @@ -44,7 +42,7 @@
    5.13  
    5.14  
    5.15  (*
    5.16 -goal thy "f a = ?g a a & ?g = x"; 
    5.17 +goal (the_context ()) "f a = ?g a a & ?g = x";
    5.18  by (rtac conjI 1);
    5.19  by (rtac refl 1);
    5.20  back();
    5.21 @@ -107,11 +105,11 @@
    5.22  *)
    5.23  
    5.24  (* implication and disjunction in atom: *)
    5.25 -goal thy "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
    5.26 +goal (the_context ()) "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
    5.27  by (fast_tac HOL_cs 1);
    5.28  
    5.29  (* disjunction in atom: *)
    5.30 -goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
    5.31 +goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
    5.32  by (step_tac HOL_cs 1);
    5.33  by (step_tac HOL_cs 1);
    5.34  by (step_tac HOL_cs 1);
    5.35 @@ -119,7 +117,7 @@
    5.36  by (fast_tac HOL_cs 1);
    5.37  (*
    5.38  hangs:
    5.39 -goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
    5.40 +goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
    5.41  by (fast_tac HOL_cs 1);
    5.42  *)
    5.43  
    5.44 @@ -144,4 +142,4 @@
    5.45  -> problem with DEPTH_SOLVE:
    5.46  Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
    5.47  Exception raised at run-time
    5.48 -*)
    5.49 \ No newline at end of file
    5.50 +*)
     6.1 --- a/src/HOL/Prolog/Test.thy	Wed Sep 07 21:00:30 2005 +0200
     6.2 +++ b/src/HOL/Prolog/Test.thy	Wed Sep 07 21:07:09 2005 +0200
     6.3 @@ -1,81 +1,85 @@
     6.4  (*  Title:    HOL/Prolog/Test.thy
     6.5      ID:       $Id$
     6.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     6.7 -
     6.8 -basic examples 
     6.9  *)
    6.10  
    6.11 -Test = HOHH +
    6.12 +header {* Basic examples *}
    6.13  
    6.14 -types nat
    6.15 -arities nat :: type
    6.16 +theory Test
    6.17 +imports HOHH
    6.18 +begin
    6.19  
    6.20 -types 'a list
    6.21 -arities list :: (type) type
    6.22 +typedecl nat
    6.23 +
    6.24 +typedecl 'a list
    6.25  
    6.26 -consts Nil   :: 'a list		 	 		 ("[]")
    6.27 -       Cons  :: 'a => 'a list => 'a list		 (infixr "#"  65)
    6.28 +consts
    6.29 +  Nil   :: "'a list"                                  ("[]")
    6.30 +  Cons  :: "'a => 'a list => 'a list"                 (infixr "#"  65)
    6.31  
    6.32  syntax
    6.33    (* list Enumeration *)
    6.34 -  "@list"     :: args => 'a list                          ("[(_)]")
    6.35 +  "@list"     :: "args => 'a list"                          ("[(_)]")
    6.36  
    6.37  translations
    6.38    "[x, xs]"     == "x#[xs]"
    6.39    "[x]"         == "x#[]"
    6.40  
    6.41 -types   person
    6.42 -arities person  :: type
    6.43 +typedecl person
    6.44  
    6.45 -consts  
    6.46 -	append  :: ['a list, 'a list, 'a list]		  => bool
    6.47 -	reverse :: ['a list, 'a list]			  => bool
    6.48 +consts
    6.49 +  append  :: "['a list, 'a list, 'a list]            => bool"
    6.50 +  reverse :: "['a list, 'a list]                     => bool"
    6.51  
    6.52 -	mappred	:: [('a => 'b => bool), 'a list, 'b list] => bool
    6.53 -	mapfun	:: [('a => 'b), 'a list, 'b list]	  => bool
    6.54 +  mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool"
    6.55 +  mapfun  :: "[('a => 'b), 'a list, 'b list]         => bool"
    6.56  
    6.57 -	bob	:: person
    6.58 -	sue	:: person
    6.59 -	ned	:: person
    6.60 +  bob     :: person
    6.61 +  sue     :: person
    6.62 +  ned     :: person
    6.63  
    6.64 -	"23"	:: nat		("23")
    6.65 -	"24"	:: nat		("24")
    6.66 -	"25"	:: nat		("25")
    6.67 +  "23"    :: nat          ("23")
    6.68 +  "24"    :: nat          ("24")
    6.69 +  "25"    :: nat          ("25")
    6.70  
    6.71 -	age	:: [person, nat]			  => bool
    6.72 +  age     :: "[person, nat]                          => bool"
    6.73  
    6.74 -	eq	:: ['a, 'a]				  => bool
    6.75 +  eq      :: "['a, 'a]                               => bool"
    6.76  
    6.77 -	empty	:: ['b]					  => bool
    6.78 -	add	:: ['a, 'b, 'b]				  => bool
    6.79 -	remove	:: ['a, 'b, 'b]				  => bool
    6.80 -	bag_appl:: ['a, 'a, 'a, 'a]			  => bool
    6.81 +  empty   :: "['b]                                   => bool"
    6.82 +  add     :: "['a, 'b, 'b]                           => bool"
    6.83 +  remove  :: "['a, 'b, 'b]                           => bool"
    6.84 +  bag_appl:: "['a, 'a, 'a, 'a]                       => bool"
    6.85  
    6.86 -rules   append	"append  []    xs  xs    ..
    6.87 -		 append (x#xs) ys (x#zs) :- append xs ys zs"
    6.88 -	reverse "reverse L1 L2 :- (!rev_aux. 
    6.89 -		  (!L.          rev_aux  []    L  L )..
    6.90 -		  (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
    6.91 -		  => rev_aux L1 L2 [])"
    6.92 +axioms
    6.93 +        append:  "append  []    xs  xs    ..
    6.94 +                  append (x#xs) ys (x#zs) :- append xs ys zs"
    6.95 +        reverse: "reverse L1 L2 :- (!rev_aux.
    6.96 +                  (!L.          rev_aux  []    L  L )..
    6.97 +                  (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
    6.98 +                  => rev_aux L1 L2 [])"
    6.99  
   6.100 -	mappred "mappred P  []     []    ..
   6.101 -		 mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
   6.102 -	mapfun  "mapfun f  []     []      ..
   6.103 -		 mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
   6.104 +        mappred: "mappred P  []     []    ..
   6.105 +                  mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
   6.106 +        mapfun:  "mapfun f  []     []      ..
   6.107 +                  mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
   6.108  
   6.109 -	age     "age bob 24 ..
   6.110 -		 age sue 23 ..
   6.111 -		 age ned 23"
   6.112 +        age:     "age bob 24 ..
   6.113 +                  age sue 23 ..
   6.114 +                  age ned 23"
   6.115  
   6.116 -	eq	"eq x x"
   6.117 +        eq:      "eq x x"
   6.118  
   6.119  (* actual definitions of empty and add is hidden -> yields abstract data type *)
   6.120  
   6.121 -	bag_appl"bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
   6.122 -				empty    S1    &
   6.123 -				add A    S1 S2 &
   6.124 -				add B    S2 S3 &
   6.125 -				remove X S3 S4 &
   6.126 -				remove Y S4 S5 &
   6.127 -				empty    S5)"
   6.128 +        bag_appl: "bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
   6.129 +                                empty    S1    &
   6.130 +                                add A    S1 S2 &
   6.131 +                                add B    S2 S3 &
   6.132 +                                remove X S3 S4 &
   6.133 +                                remove Y S4 S5 &
   6.134 +                                empty    S5)"
   6.135 +
   6.136 +ML {* use_legacy_bindings (the_context ()) *}
   6.137 +
   6.138  end
     7.1 --- a/src/HOL/Prolog/Type.thy	Wed Sep 07 21:00:30 2005 +0200
     7.2 +++ b/src/HOL/Prolog/Type.thy	Wed Sep 07 21:07:09 2005 +0200
     7.3 @@ -1,23 +1,24 @@
     7.4  (*  Title:    HOL/Prolog/Type.thy
     7.5      ID:       $Id$
     7.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     7.7 -
     7.8 -type inference 
     7.9  *)
    7.10  
    7.11 -Type = Func +
    7.12 +header {* Type inference *}
    7.13  
    7.14 -types ty
    7.15 +theory Type
    7.16 +imports Func
    7.17 +begin
    7.18  
    7.19 -arities ty :: type
    7.20 +typedecl ty
    7.21  
    7.22 -consts  bool	:: ty
    7.23 -	nat	:: ty
    7.24 -	"->"	:: ty => ty => ty	(infixr 20)
    7.25 -	typeof	:: [tm, ty] => bool
    7.26 -        anyterm :: tm
    7.27 +consts
    7.28 +  bool    :: ty
    7.29 +  nat     :: ty
    7.30 +  "->"    :: "ty => ty => ty"       (infixr 20)
    7.31 +  typeof  :: "[tm, ty] => bool"
    7.32 +  anyterm :: tm
    7.33  
    7.34 -rules	common_typeof	"
    7.35 +axioms  common_typeof:   "
    7.36  typeof (app M N) B       :- typeof M (A -> B) & typeof N A..
    7.37  
    7.38  typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
    7.39 @@ -35,13 +36,15 @@
    7.40  typeof (M - N) nat :- typeof M nat & typeof N nat..
    7.41  typeof (M * N) nat :- typeof M nat & typeof N nat"
    7.42  
    7.43 -rules	good_typeof	"
    7.44 +axioms good_typeof:     "
    7.45  typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
    7.46  
    7.47 -rules	bad1_typeof	"
    7.48 +axioms bad1_typeof:     "
    7.49  typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
    7.50  
    7.51 -rules	bad2_typeof	"
    7.52 +axioms bad2_typeof:     "
    7.53  typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
    7.54  
    7.55 +ML {* use_legacy_bindings (the_context ()) *}
    7.56 +
    7.57  end