# HG changeset patch # User wenzelm # Date 1126120029 -7200 # Node ID 5b1d47d920ce02d4bba3387518ae2ac2135c8f78 # Parent 1322ed8e0ee4d79c45fb0d399fc5cc6d92e358f8 converted to Isar theory format; diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/Func.ML --- 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"; diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/Func.thy --- 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 diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/HOHH.ML --- 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 = []; diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/HOHH.thy --- 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 - diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/Test.ML --- 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 +*) diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/Test.thy --- 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 diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/Type.thy --- 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