--- a/src/HOL/IsaMakefile Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/IsaMakefile Mon Nov 20 21:23:12 2006 +0100
@@ -499,9 +499,8 @@
HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
-$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/HOHH.ML Prolog/HOHH.thy \
- Prolog/Test.ML Prolog/Test.thy \
- Prolog/Func.ML Prolog/Func.thy Prolog/Type.ML Prolog/Type.thy
+$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML Prolog/HOHH.thy \
+ Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
@$(ISATOOL) usedir $(OUT)/HOL Prolog
--- a/src/HOL/Prolog/Func.ML Mon Nov 20 11:51:10 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title: HOL/Prolog/Func.ML
- ID: $Id$
- Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-*)
-
-val prog_Func = prog_HOHH @ [eval];
-fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
-val p = ptac prog_Func 1;
-
-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";
--- a/src/HOL/Prolog/Func.thy Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/Prolog/Func.thy Mon Nov 20 21:23:12 2006 +0100
@@ -20,8 +20,8 @@
true :: tm
false :: tm
- "and" :: "tm => tm => tm" (infixr 999)
- "eq" :: "tm => tm => tm" (infixr 999)
+ "and" :: "tm => tm => tm" (infixr "and" 999)
+ eq :: "tm => tm => tm" (infixr "eq" 999)
Z :: tm ("Z")
S :: "tm => tm"
@@ -60,6 +60,16 @@
eval ( Z * M) Z..
eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
-ML {* use_legacy_bindings (the_context ()) *}
+
+lemmas prog_Func = eval
+
+lemma "eval ((S (S Z)) + (S Z)) ?X"
+ apply (prolog prog_Func)
+ done
+
+lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
+ (n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"
+ apply (prolog prog_Func)
+ done
end
--- a/src/HOL/Prolog/HOHH.ML Mon Nov 20 11:51:10 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,123 +0,0 @@
-(* Title: HOL/Prolog/HOHH.ML
- ID: $Id$
- Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-*)
-
-exception not_HOHH;
-
-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
- | Const( "==>",_)$l$r => isG l andalso isD r
- | Const("All",_)$Abs(s,_,t) => isD t
- | Const("all",_)$Abs(s,_,t) => isD t
- | Const("op |",_)$_$_ => false
- | Const("Ex" ,_)$_ => false
- | Const("not",_)$_ => false
- | Const("True",_) => false
- | Const("False",_) => false
- | l $ r => isD l
- | Const _ (* rigid atom *) => true
- | Bound _ (* rigid atom *) => true
- | Free _ (* rigid atom *) => true
- | _ (* flexible atom,
- anything else *) => false
-and
- isG t = case t of
- Const("Trueprop",_)$t => isG t
- | Const("op &" ,_)$l$r => isG l andalso isG r
- | Const("op |" ,_)$l$r => isG l andalso isG r
- | Const("op -->",_)$l$r => isD l andalso isG r
- | Const( "==>",_)$l$r => isD l andalso isG r
- | Const("All",_)$Abs(_,_,t) => isG t
- | Const("all",_)$Abs(_,_,t) => isG t
- | Const("Ex" ,_)$Abs(_,_,t) => isG t
- | Const("True",_) => true
- | Const("not",_)$_ => false
- | Const("False",_) => false
- | _ (* 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);
-
-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))
- | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
- | _$(Const("op -->",_)$_$_) => at(thm RS mp)
- | _ => [thm]
-in map zero_var_indexes (at thm) end;
-
-val atomize_ss =
- Simplifier.theory_context (the_context ()) 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)" *)
-
-(*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 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;
-
-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))
-end;
-
-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 Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/Prolog/HOHH.thy Mon Nov 20 21:23:12 2006 +0100
@@ -7,18 +7,27 @@
theory HOHH
imports HOL
+uses "prolog.ML"
begin
+method_setup ptac =
+ {* Method.thms_args (Method.SIMPLE_METHOD' HEADGOAL o Prolog.ptac) *}
+ "Basic Lambda Prolog interpreter"
+
+method_setup prolog =
+ {* Method.thms_args (Method.SIMPLE_METHOD o Prolog.prolog_tac) *}
+ "Lambda Prolog interpreter"
+
consts
(* D-formulas (programs): D ::= !x. D | D .. D | D :- G | A *)
- "Dand" :: "[bool, bool] => bool" (infixr ".." 28)
- ":-" :: "[bool, bool] => bool" (infixl 29)
+ Dand :: "[bool, bool] => bool" (infixr ".." 28)
+ Dif :: "[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)
+(*Dand' :: "[bool, bool] => bool" (infixr "," 35)*)
+ Dimp :: "[bool, bool] => bool" (infixr "=>" 27)
translations
--- a/src/HOL/Prolog/Test.ML Mon Nov 20 11:51:10 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-(* Title: HOL/Prolog/Test.ML
- ID: $Id$
- Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-*)
-
-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;
-
-pgoal "append ?x ?y [a,b,c,d]";
-back();
-back();
-back();
-back();
-
-pgoal "append [a,b] y ?L";
-pgoal "!y. append [a,b] y (?L y)";
-
-pgoal "reverse [] ?L";
-
-pgoal "reverse [23] ?L";
-pgoal "reverse [23,24,?x] ?L";
-pgoal "reverse ?L [23,24,?x]";
-
-pgoal "mappred age ?x [23,24]";
-back();
-
-pgoal "mappred (%x y. ? z. age z y) ?x [23,24]";
-
-pgoal "mappred ?P [bob,sue] [24,23]";
-
-pgoal "mapfun f [bob,bob,sue] [?x,?y,?z]";
-
-pgoal "mapfun (%x. h x 25) [bob,sue] ?L";
-
-pgoal "mapfun ?F [24,25] [h bob 24,h bob 25]";
-
-pgoal "mapfun ?F [24] [h 24 24]";
-back();
-back();
-back();
-
-
-(*
-goal (the_context ()) "f a = ?g a a & ?g = x";
-by (rtac conjI 1);
-by (rtac refl 1);
-back();
-back();
-*)
-
-pgoal "True";
-
-pgoal "age ?x 24 & age ?y 23";
-back();
-
-pgoal "age ?x 24 | age ?x 23";
-back();
-back();
-
-pgoal "? x y. age x y";
-
-pgoal "!x y. append [] x x";
-
-pgoal "age sue 24 .. age bob 23 => age ?x ?y";
-back();
-back();
-back();
-back();
-
-(*set trace_DEPTH_FIRST;*)
-pgoal "age bob 25 :- age bob 24 => age bob 25";
-(*reset trace_DEPTH_FIRST;*)
-
-pgoal "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25";
-back();
-back();
-back();
-
-pgoal "!x. ? y. eq x y";
-
-pgoal "? P. P & eq P ?x";
-(*
-back();
-back();
-back();
-back();
-back();
-back();
-back();
-back();
-*)
-
-pgoal "? P. eq P (True & True) & P";
-
-pgoal "? P. eq P op | & P k True";
-
-pgoal "? P. eq P (Q => True) & P";
-
-(* P flexible: *)
-pgoal "(!P k l. P k l :- eq P Q) => Q a b";
-(*
-loops:
-pgoal "(!P k l. P k l :- eq P (%x y. x | y)) => a | b";
-*)
-
-(* implication and disjunction in atom: *)
-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 (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);
-by (fast_tac HOL_cs 2);
-by (fast_tac HOL_cs 1);
-(*
-hangs:
-goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
-by (fast_tac HOL_cs 1);
-*)
-
-pgoal "!Emp Stk.(\
-\ empty (Emp::'b) .. \
-\ (!(X::nat) S. add X (S::'b) (Stk X S)) .. \
-\ (!(X::nat) S. remove X ((Stk X S)::'b) S))\
-\ => bag_appl 23 24 ?X ?Y";
-
-pgoal "!Qu. ( \
-\ (!L. empty (Qu L L)) .. \
-\ (!(X::nat) L K. add X (Qu L (X#K)) (Qu L K)) ..\
-\ (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))\
-\ => bag_appl 23 24 ?X ?Y";
-
-pgoal "D & (!y. E) :- (!x. True & True) :- True => D";
-
-pgoal "P x .. P y => P ?X";
-back();
-(*
-back();
--> problem with DEPTH_SOLVE:
-Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
-Exception raised at run-time
-*)
--- a/src/HOL/Prolog/Test.thy Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/Prolog/Test.thy Mon Nov 20 21:23:12 2006 +0100
@@ -80,6 +80,202 @@
remove Y S4 S5 &
empty S5)"
-ML {* use_legacy_bindings (the_context ()) *}
+lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
+
+lemma "append ?x ?y [a,b,c,d]"
+ apply (prolog prog_Test)
+ back
+ back
+ back
+ back
+ done
+
+lemma "append [a,b] y ?L"
+ apply (prolog prog_Test)
+ done
+
+lemma "!y. append [a,b] y (?L y)"
+ apply (prolog prog_Test)
+ done
+
+lemma "reverse [] ?L"
+ apply (prolog prog_Test)
+ done
+
+lemma "reverse [23] ?L"
+ apply (prolog prog_Test)
+ done
+
+lemma "reverse [23,24,?x] ?L"
+ apply (prolog prog_Test)
+ done
+
+lemma "reverse ?L [23,24,?x]"
+ apply (prolog prog_Test)
+ done
+
+lemma "mappred age ?x [23,24]"
+ apply (prolog prog_Test)
+ back
+ done
+
+lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
+ apply (prolog prog_Test)
+ done
+
+lemma "mappred ?P [bob,sue] [24,23]"
+ apply (prolog prog_Test)
+ done
+
+lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
+ apply (prolog prog_Test)
+ done
+
+lemma "mapfun (%x. h x 25) [bob,sue] ?L"
+ apply (prolog prog_Test)
+ done
+
+lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
+ apply (prolog prog_Test)
+ done
+
+lemma "mapfun ?F [24] [h 24 24]"
+ apply (prolog prog_Test)
+ back
+ back
+ back
+ done
+
+lemma "True"
+ apply (prolog prog_Test)
+ done
+
+lemma "age ?x 24 & age ?y 23"
+ apply (prolog prog_Test)
+ back
+ done
+
+lemma "age ?x 24 | age ?x 23"
+ apply (prolog prog_Test)
+ back
+ back
+ done
+
+lemma "? x y. age x y"
+ apply (prolog prog_Test)
+ done
+
+lemma "!x y. append [] x x"
+ apply (prolog prog_Test)
+ done
+
+lemma "age sue 24 .. age bob 23 => age ?x ?y"
+ apply (prolog prog_Test)
+ back
+ back
+ back
+ back
+ done
+
+(*set trace_DEPTH_FIRST;*)
+lemma "age bob 25 :- age bob 24 => age bob 25"
+ apply (prolog prog_Test)
+ done
+(*reset trace_DEPTH_FIRST;*)
+
+lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
+ apply (prolog prog_Test)
+ back
+ back
+ back
+ done
+
+lemma "!x. ? y. eq x y"
+ apply (prolog prog_Test)
+ done
+
+lemma "? P. P & eq P ?x"
+ apply (prolog prog_Test)
+(*
+ back
+ back
+ back
+ back
+ back
+ back
+ back
+ back
+*)
+ done
+
+lemma "? P. eq P (True & True) & P"
+ apply (prolog prog_Test)
+ done
+
+lemma "? P. eq P op | & P k True"
+ apply (prolog prog_Test)
+ done
+
+lemma "? P. eq P (Q => True) & P"
+ apply (prolog prog_Test)
+ done
+
+(* P flexible: *)
+lemma "(!P k l. P k l :- eq P Q) => Q a b"
+ apply (prolog prog_Test)
+ done
+(*
+loops:
+lemma "(!P k l. P k l :- eq P (%x y. x | y)) => a | b"
+*)
+
+(* implication and disjunction in atom: *)
+lemma "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)"
+ by fast
+
+(* disjunction in atom: *)
+lemma "(!P. g P :- (P => b | a)) => g(a | b)"
+ apply (tactic "step_tac HOL_cs 1")
+ apply (tactic "step_tac HOL_cs 1")
+ apply (tactic "step_tac HOL_cs 1")
+ prefer 2
+ apply fast
+ apply fast
+ done
+
+(*
+hangs:
+lemma "(!P. g P :- (P => b | a)) => g(a | b)"
+ by fast
+*)
+
+lemma "!Emp Stk.(
+ empty (Emp::'b) ..
+ (!(X::nat) S. add X (S::'b) (Stk X S)) ..
+ (!(X::nat) S. remove X ((Stk X S)::'b) S))
+ => bag_appl 23 24 ?X ?Y"
+ oops
+
+lemma "!Qu. (
+ (!L. empty (Qu L L)) ..
+ (!(X::nat) L K. add X (Qu L (X#K)) (Qu L K)) ..
+ (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
+ => bag_appl 23 24 ?X ?Y"
+ oops
+
+lemma "D & (!y. E) :- (!x. True & True) :- True => D"
+ apply (prolog prog_Test)
+ done
+
+lemma "P x .. P y => P ?X"
+ apply (prolog prog_Test)
+ back
+ done
+(*
+back
+-> problem with DEPTH_SOLVE:
+Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
+Exception raised at run-time
+*)
end
--- a/src/HOL/Prolog/Type.ML Mon Nov 20 11:51:10 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(* Title: HOL/Prolog/Type.ML
- ID: $Id$
- Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-*)
-
-val prog_Type = prog_Func @ [good_typeof,common_typeof];
-fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type));
-val p = ptac prog_Type 1;
-
-pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T";
-
-pgoal "typeof (fix (%x. x)) ?T";
-
-pgoal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T";
-
-pgoal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
- \(n * (app fact (n - (S Z))))))) ?T";
-
-pgoal "typeof (abs(%v. Z)) ?T"; (*correct only solution (?A1 -> nat) *)
-Goal "typeof (abs(%v. Z)) ?T";
-by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*)
-back(); (* 2nd result (?A1 -> ?A1) wrong *)
-
-(*pgoal "typeof (abs(%v. abs(%v. app v v))) ?T"; correctly fails*)
-Goal "typeof (abs(%v. abs(%v. app v v))) ?T";
-by (prolog_tac [bad2_typeof,common_typeof]);
- (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
--- a/src/HOL/Prolog/Type.thy Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/Prolog/Type.thy Mon Nov 20 21:23:12 2006 +0100
@@ -14,7 +14,7 @@
consts
bool :: ty
nat :: ty
- "->" :: "ty => ty => ty" (infixr 20)
+ arrow :: "ty => ty => ty" (infixr "->" 20)
typeof :: "[tm, ty] => bool"
anyterm :: tm
@@ -45,6 +45,45 @@
axioms bad2_typeof: "
typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
-ML {* use_legacy_bindings (the_context ()) *}
+
+lemmas prog_Type = prog_Func good_typeof common_typeof
+
+lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
+ apply (prolog prog_Type)
+ done
+
+lemma "typeof (fix (%x. x)) ?T"
+ apply (prolog prog_Type)
+ done
+
+lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
+ apply (prolog prog_Type)
+ done
+
+lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
+ (n * (app fact (n - (S Z))))))) ?T"
+ apply (prolog prog_Type)
+ done
+
+lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
+ apply (prolog prog_Type)
+ done
+
+lemma "typeof (abs(%v. Z)) ?T"
+ apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
+ done
+
+lemma "typeof (abs(%v. Z)) ?T"
+ apply (prolog bad1_typeof common_typeof)
+ back (* 2nd result (?A1 -> ?A1) wrong *)
+ done
+
+lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
+ apply (prolog prog_Type)? (*correctly fails*)
+ oops
+
+lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
+ apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
+ done
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/prolog.ML Mon Nov 20 21:23:12 2006 +0100
@@ -0,0 +1,130 @@
+(* Title: HOL/Prolog/prolog.ML
+ ID: $Id$
+ Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+*)
+
+set Proof.show_main_goal;
+
+structure Prolog =
+struct
+
+exception not_HOHH;
+
+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
+ | Const( "==>",_)$l$r => isG l andalso isD r
+ | Const("All",_)$Abs(s,_,t) => isD t
+ | Const("all",_)$Abs(s,_,t) => isD t
+ | Const("op |",_)$_$_ => false
+ | Const("Ex" ,_)$_ => false
+ | Const("not",_)$_ => false
+ | Const("True",_) => false
+ | Const("False",_) => false
+ | l $ r => isD l
+ | Const _ (* rigid atom *) => true
+ | Bound _ (* rigid atom *) => true
+ | Free _ (* rigid atom *) => true
+ | _ (* flexible atom,
+ anything else *) => false
+and
+ isG t = case t of
+ Const("Trueprop",_)$t => isG t
+ | Const("op &" ,_)$l$r => isG l andalso isG r
+ | Const("op |" ,_)$l$r => isG l andalso isG r
+ | Const("op -->",_)$l$r => isD l andalso isG r
+ | Const( "==>",_)$l$r => isD l andalso isG r
+ | Const("All",_)$Abs(_,_,t) => isG t
+ | Const("all",_)$Abs(_,_,t) => isG t
+ | Const("Ex" ,_)$Abs(_,_,t) => isG t
+ | Const("True",_) => true
+ | Const("not",_)$_ => false
+ | Const("False",_) => false
+ | _ (* 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);
+
+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))
+ | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ | _$(Const("op -->",_)$_$_) => at(thm RS mp)
+ | _ => [thm]
+in map zero_var_indexes (at thm) end;
+
+val atomize_ss =
+ Simplifier.theory_context (the_context ()) 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)" *)
+
+(*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 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;
+
+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))
+end;
+
+fun prolog_tac prog = check_HOHH_tac1 THEN
+ DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
+
+val prog_HOHH = [];
+
+end;