--- a/src/HOL/Prolog/Func.ML Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Func.ML Wed Sep 07 21:07:09 2005 +0200
@@ -3,8 +3,6 @@
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
-open Func;
-
val prog_Func = prog_HOHH @ [eval];
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
val p = ptac prog_Func 1;
@@ -12,6 +10,4 @@
pgoal "eval ((S (S Z)) + (S Z)) ?X";
pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
- \(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
-
-
+ \(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
--- a/src/HOL/Prolog/Func.thy Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Func.thy Wed Sep 07 21:07:09 2005 +0200
@@ -1,40 +1,41 @@
(* Title: HOL/Prolog/Func.thy
ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-
-untyped functional language, with call by value semantics
*)
-Func = HOHH +
+header {* Untyped functional language, with call by value semantics *}
-types tm
-
-arities tm :: type
+theory Func
+imports HOHH
+begin
-consts abs :: (tm => tm) => tm
- app :: tm => tm => tm
+typedecl tm
- cond :: tm => tm => tm => tm
- fix :: (tm => tm) => tm
+consts
+ abs :: "(tm => tm) => tm"
+ app :: "tm => tm => tm"
+
+ cond :: "tm => tm => tm => tm"
+ "fix" :: "(tm => tm) => tm"
- true,
- false :: tm
- "and" :: tm => tm => tm (infixr 999)
- "eq" :: tm => tm => tm (infixr 999)
+ true :: tm
+ false :: tm
+ "and" :: "tm => tm => tm" (infixr 999)
+ "eq" :: "tm => tm => tm" (infixr 999)
- "0" :: tm ("Z")
- S :: tm => tm
+ "0" :: tm ("Z")
+ S :: "tm => tm"
(*
- "++", "--",
- "**" :: tm => tm => tm (infixr 999)
+ "++", "--",
+ "**" :: tm => tm => tm (infixr 999)
*)
- eval :: [tm, tm] => bool
+ eval :: "[tm, tm] => bool"
-arities tm :: plus
-arities tm :: minus
-arities tm :: times
+instance tm :: plus ..
+instance tm :: minus ..
+instance tm :: times ..
-rules eval "
+axioms eval: "
eval (abs RR) (abs RR)..
eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V..
@@ -47,7 +48,7 @@
eval false false..
eval (P and Q) true :- eval P true & eval Q true ..
eval (P and Q) false :- eval P false | eval Q false..
-eval (A1 eq B1) true :- eval A1 C1 & eval B1 C1..
+eval (A1 eq B1) true :- eval A1 C1 & eval B1 C1..
eval (A2 eq B2) false :- True..
eval Z Z..
@@ -59,4 +60,6 @@
eval ( Z * M) Z..
eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/Prolog/HOHH.ML Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/HOHH.ML Wed Sep 07 21:07:09 2005 +0200
@@ -3,11 +3,9 @@
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
-open HOHH;
-
exception not_HOHH;
-fun isD t = case t of
+fun isD t = case t of
Const("Trueprop",_)$t => isD t
| Const("op &" ,_)$l$r => isD l andalso isD r
| Const("op -->",_)$l$r => isG l andalso isD r
@@ -24,7 +22,7 @@
| Bound _ (* rigid atom *) => true
| Free _ (* rigid atom *) => true
| _ (* flexible atom,
- anything else *) => false
+ anything else *) => false
and
isG t = case t of
Const("Trueprop",_)$t => isG t
@@ -38,85 +36,85 @@
| Const("True",_) => true
| Const("not",_)$_ => false
| Const("False",_) => false
- | _ (* atom *) => true;
+ | _ (* atom *) => true;
-val check_HOHH_tac1 = PRIMITIVE (fn thm =>
- if isG (concl_of thm) then thm else raise not_HOHH);
-val check_HOHH_tac2 = PRIMITIVE (fn thm =>
- if forall isG (prems_of thm) then thm else raise not_HOHH);
-fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm)
- then thm else raise not_HOHH);
+val check_HOHH_tac1 = PRIMITIVE (fn thm =>
+ if isG (concl_of thm) then thm else raise not_HOHH);
+val check_HOHH_tac2 = PRIMITIVE (fn thm =>
+ if forall isG (prems_of thm) then thm else raise not_HOHH);
+fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm)
+ then thm else raise not_HOHH);
-fun atomizeD thm = let
+fun atomizeD thm = let
fun at thm = case concl_of thm of
_$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
- "?"^(if s="P" then "PP" else s))] spec))
+ "?"^(if s="P" then "PP" else s))] spec))
| _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const("op -->",_)$_$_) => at(thm RS mp)
- | _ => [thm]
+ | _ => [thm]
in map zero_var_indexes (at thm) end;
val atomize_ss = empty_ss setmksimps (mksimps mksimps_pairs) addsimps [
- all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
- imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
- imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
- imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *)
+ all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
+ imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
+ imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
+ imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *)
-(*val hyp_resolve_tac = METAHYPS (fn prems =>
- resolve_tac (List.concat (map atomizeD prems)) 1);
+(*val hyp_resolve_tac = METAHYPS (fn prems =>
+ resolve_tac (List.concat (map atomizeD prems)) 1);
-- is nice, but cannot instantiate unknowns in the assumptions *)
fun hyp_resolve_tac i st = let
- fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
- | ap (Const("op -->",_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
- | ap t = (0,false,t);
+ fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
+ | ap (Const("op -->",_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
+ | ap t = (0,false,t);
(*
- fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
- | rep_goal (Const ("==>",_)$s$t) =
- (case rep_goal t of (l,t) => (s::l,t))
- | rep_goal t = ([] ,t);
- val (prems, Const("Trueprop", _)$concl) = rep_goal
- (#3(dest_state (st,i)));
+ fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
+ | rep_goal (Const ("==>",_)$s$t) =
+ (case rep_goal t of (l,t) => (s::l,t))
+ | rep_goal t = ([] ,t);
+ val (prems, Const("Trueprop", _)$concl) = rep_goal
+ (#3(dest_state (st,i)));
*)
- val subgoal = #3(dest_state (st,i));
- val prems = Logic.strip_assums_hyp subgoal;
- val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
- fun drot_tac k i = DETERM (rotate_tac k i);
- fun spec_tac 0 i = all_tac
- | spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
- fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
- [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
- fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
- | same_head k (s$_) (t$_) = same_head k s t
- | same_head k (Bound i) (Bound j) = i = j + k
- | same_head _ _ _ = true;
- fun mapn f n [] = []
- | mapn f n (x::xs) = f n x::mapn f (n+1) xs;
- fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
- if same_head k t concl
- then dup_spec_tac k i THEN
- (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
- else no_tac);
- val ptacs = mapn (fn n => fn t =>
- pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
- in Library.foldl (op APPEND) (no_tac, ptacs) st end;
+ val subgoal = #3(dest_state (st,i));
+ val prems = Logic.strip_assums_hyp subgoal;
+ val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
+ fun drot_tac k i = DETERM (rotate_tac k i);
+ fun spec_tac 0 i = all_tac
+ | spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
+ fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
+ [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
+ fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
+ | same_head k (s$_) (t$_) = same_head k s t
+ | same_head k (Bound i) (Bound j) = i = j + k
+ | same_head _ _ _ = true;
+ fun mapn f n [] = []
+ | mapn f n (x::xs) = f n x::mapn f (n+1) xs;
+ fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
+ if same_head k t concl
+ then dup_spec_tac k i THEN
+ (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
+ else no_tac);
+ val ptacs = mapn (fn n => fn t =>
+ pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
+ in Library.foldl (op APPEND) (no_tac, ptacs) st end;
fun ptac prog = let
- val proga = List.concat (map atomizeD prog) (* atomize the prog *)
- in (REPEAT_DETERM1 o FIRST' [
- rtac TrueI, (* "True" *)
- rtac conjI, (* "[| P; Q |] ==> P & Q" *)
- rtac allI, (* "(!!x. P x) ==> ! x. P x" *)
- rtac exI, (* "P x ==> ? x. P x" *)
- rtac impI THEN' (* "(P ==> Q) ==> P --> Q" *)
- asm_full_simp_tac atomize_ss THEN' (* atomize the asms *)
- (REPEAT_DETERM o (etac conjE)) (* split the asms *)
- ])
- ORELSE' resolve_tac [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*)
- ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
- THEN' (fn _ => check_HOHH_tac2))
+ val proga = List.concat (map atomizeD prog) (* atomize the prog *)
+ in (REPEAT_DETERM1 o FIRST' [
+ rtac TrueI, (* "True" *)
+ rtac conjI, (* "[| P; Q |] ==> P & Q" *)
+ rtac allI, (* "(!!x. P x) ==> ! x. P x" *)
+ rtac exI, (* "P x ==> ? x. P x" *)
+ rtac impI THEN' (* "(P ==> Q) ==> P --> Q" *)
+ asm_full_simp_tac atomize_ss THEN' (* atomize the asms *)
+ (REPEAT_DETERM o (etac conjE)) (* split the asms *)
+ ])
+ ORELSE' resolve_tac [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*)
+ ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
+ THEN' (fn _ => check_HOHH_tac2))
end;
-fun prolog_tac prog = check_HOHH_tac1 THEN
- DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
+fun prolog_tac prog = check_HOHH_tac1 THEN
+ DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
val prog_HOHH = [];
--- a/src/HOL/Prolog/HOHH.thy Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/HOHH.thy Wed Sep 07 21:07:09 2005 +0200
@@ -1,29 +1,30 @@
(* Title: HOL/Prolog/HOHH.thy
ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-
-higher-order hereditary Harrop formulas
*)
-HOHH = HOL +
+header {* Higher-order hereditary Harrop formulas *}
+
+theory HOHH
+imports HOL
+begin
consts
-(* D-formulas (programs): D ::= !x. D | D .. D | D :- G | A *)
- "Dand" :: [bool, bool] => bool (infixr ".." 28)
- ":-" :: [bool, bool] => bool (infixl 29)
+(* D-formulas (programs): D ::= !x. D | D .. D | D :- G | A *)
+ "Dand" :: "[bool, bool] => bool" (infixr ".." 28)
+ ":-" :: "[bool, bool] => bool" (infixl 29)
-(* G-formulas (goals): G ::= A | G & G | G | G | ? x. G
- | True | !x. G | D => G *)
-(*"," :: [bool, bool] => bool (infixr 35)*)
- "=>" :: [bool, bool] => bool (infixr 27)
+(* G-formulas (goals): G ::= A | G & G | G | G | ? x. G
+ | True | !x. G | D => G *)
+(*"," :: "[bool, bool] => bool" (infixr 35)*)
+ "=>" :: "[bool, bool] => bool" (infixr 27)
translations
- "D :- G" => "G --> D"
- "D1 .. D2" => "D1 & D2"
-(*"G1 , G2" => "G1 & G2"*)
- "D => G" => "D --> G"
+ "D :- G" => "G --> D"
+ "D1 .. D2" => "D1 & D2"
+(*"G1 , G2" => "G1 & G2"*)
+ "D => G" => "D --> G"
end
-
--- a/src/HOL/Prolog/Test.ML Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Test.ML Wed Sep 07 21:07:09 2005 +0200
@@ -3,8 +3,6 @@
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
-open Test;
-
val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test));
val p = ptac prog_Test 1;
@@ -44,7 +42,7 @@
(*
-goal thy "f a = ?g a a & ?g = x";
+goal (the_context ()) "f a = ?g a a & ?g = x";
by (rtac conjI 1);
by (rtac refl 1);
back();
@@ -107,11 +105,11 @@
*)
(* implication and disjunction in atom: *)
-goal thy "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
+goal (the_context ()) "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
by (fast_tac HOL_cs 1);
(* disjunction in atom: *)
-goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
+goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
by (step_tac HOL_cs 1);
by (step_tac HOL_cs 1);
by (step_tac HOL_cs 1);
@@ -119,7 +117,7 @@
by (fast_tac HOL_cs 1);
(*
hangs:
-goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
+goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
by (fast_tac HOL_cs 1);
*)
@@ -144,4 +142,4 @@
-> problem with DEPTH_SOLVE:
Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
Exception raised at run-time
-*)
\ No newline at end of file
+*)
--- a/src/HOL/Prolog/Test.thy Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Test.thy Wed Sep 07 21:07:09 2005 +0200
@@ -1,81 +1,85 @@
(* Title: HOL/Prolog/Test.thy
ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-
-basic examples
*)
-Test = HOHH +
+header {* Basic examples *}
-types nat
-arities nat :: type
+theory Test
+imports HOHH
+begin
-types 'a list
-arities list :: (type) type
+typedecl nat
+
+typedecl 'a list
-consts Nil :: 'a list ("[]")
- Cons :: 'a => 'a list => 'a list (infixr "#" 65)
+consts
+ Nil :: "'a list" ("[]")
+ Cons :: "'a => 'a list => 'a list" (infixr "#" 65)
syntax
(* list Enumeration *)
- "@list" :: args => 'a list ("[(_)]")
+ "@list" :: "args => 'a list" ("[(_)]")
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
-types person
-arities person :: type
+typedecl person
-consts
- append :: ['a list, 'a list, 'a list] => bool
- reverse :: ['a list, 'a list] => bool
+consts
+ append :: "['a list, 'a list, 'a list] => bool"
+ reverse :: "['a list, 'a list] => bool"
- mappred :: [('a => 'b => bool), 'a list, 'b list] => bool
- mapfun :: [('a => 'b), 'a list, 'b list] => bool
+ mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool"
+ mapfun :: "[('a => 'b), 'a list, 'b list] => bool"
- bob :: person
- sue :: person
- ned :: person
+ bob :: person
+ sue :: person
+ ned :: person
- "23" :: nat ("23")
- "24" :: nat ("24")
- "25" :: nat ("25")
+ "23" :: nat ("23")
+ "24" :: nat ("24")
+ "25" :: nat ("25")
- age :: [person, nat] => bool
+ age :: "[person, nat] => bool"
- eq :: ['a, 'a] => bool
+ eq :: "['a, 'a] => bool"
- empty :: ['b] => bool
- add :: ['a, 'b, 'b] => bool
- remove :: ['a, 'b, 'b] => bool
- bag_appl:: ['a, 'a, 'a, 'a] => bool
+ empty :: "['b] => bool"
+ add :: "['a, 'b, 'b] => bool"
+ remove :: "['a, 'b, 'b] => bool"
+ bag_appl:: "['a, 'a, 'a, 'a] => bool"
-rules append "append [] xs xs ..
- append (x#xs) ys (x#zs) :- append xs ys zs"
- reverse "reverse L1 L2 :- (!rev_aux.
- (!L. rev_aux [] L L )..
- (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
- => rev_aux L1 L2 [])"
+axioms
+ append: "append [] xs xs ..
+ append (x#xs) ys (x#zs) :- append xs ys zs"
+ reverse: "reverse L1 L2 :- (!rev_aux.
+ (!L. rev_aux [] L L )..
+ (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
+ => rev_aux L1 L2 [])"
- mappred "mappred P [] [] ..
- mappred P (x#xs) (y#ys) :- P x y & mappred P xs ys"
- mapfun "mapfun f [] [] ..
- mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
+ mappred: "mappred P [] [] ..
+ mappred P (x#xs) (y#ys) :- P x y & mappred P xs ys"
+ mapfun: "mapfun f [] [] ..
+ mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
- age "age bob 24 ..
- age sue 23 ..
- age ned 23"
+ age: "age bob 24 ..
+ age sue 23 ..
+ age ned 23"
- eq "eq x x"
+ eq: "eq x x"
(* actual definitions of empty and add is hidden -> yields abstract data type *)
- bag_appl"bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
- empty S1 &
- add A S1 S2 &
- add B S2 S3 &
- remove X S3 S4 &
- remove Y S4 S5 &
- empty S5)"
+ bag_appl: "bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
+ empty S1 &
+ add A S1 S2 &
+ add B S2 S3 &
+ remove X S3 S4 &
+ remove Y S4 S5 &
+ empty S5)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/Prolog/Type.thy Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Type.thy Wed Sep 07 21:07:09 2005 +0200
@@ -1,23 +1,24 @@
(* Title: HOL/Prolog/Type.thy
ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-
-type inference
*)
-Type = Func +
+header {* Type inference *}
-types ty
+theory Type
+imports Func
+begin
-arities ty :: type
+typedecl ty
-consts bool :: ty
- nat :: ty
- "->" :: ty => ty => ty (infixr 20)
- typeof :: [tm, ty] => bool
- anyterm :: tm
+consts
+ bool :: ty
+ nat :: ty
+ "->" :: "ty => ty => ty" (infixr 20)
+ typeof :: "[tm, ty] => bool"
+ anyterm :: tm
-rules common_typeof "
+axioms common_typeof: "
typeof (app M N) B :- typeof M (A -> B) & typeof N A..
typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
@@ -35,13 +36,15 @@
typeof (M - N) nat :- typeof M nat & typeof N nat..
typeof (M * N) nat :- typeof M nat & typeof N nat"
-rules good_typeof "
+axioms good_typeof: "
typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
-rules bad1_typeof "
+axioms bad1_typeof: "
typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
-rules bad2_typeof "
+axioms bad2_typeof: "
typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
+ML {* use_legacy_bindings (the_context ()) *}
+
end