Theory Prolog
section ‹First-Order Logic: PROLOG examples›
theory Prolog
imports FOL
begin
typedecl 'a list
instance list :: (‹term›) ‹term› ..
axiomatization
Nil :: ‹'a list› and
Cons :: ‹['a, 'a list]=> 'a list› (infixr ‹:› 60) and
app :: ‹['a list, 'a list, 'a list] => o› and
rev :: ‹['a list, 'a list] => o›
where
appNil: ‹app(Nil,ys,ys)› and
appCons: ‹app(xs,ys,zs) ==> app(x:xs, ys, x:zs)› and
revNil: ‹rev(Nil,Nil)› and
revCons: ‹[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)›
schematic_goal ‹app(a:b:c:Nil, d:e:Nil, ?x)›
apply (rule appNil appCons)
apply (rule appNil appCons)
apply (rule appNil appCons)
apply (rule appNil appCons)
done
schematic_goal ‹app(?x, c:d:Nil, a:b:c:d:Nil)›
apply (rule appNil appCons)+
done
schematic_goal ‹app(?x, ?y, a:b:c:d:Nil)›
apply (rule appNil appCons)+
back
back
back
back
done
lemmas rules = appNil appCons revNil revCons
schematic_goal ‹rev(a:b:c:d:Nil, ?x)›
apply (rule rules)+
done
schematic_goal ‹rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)›
apply (rule rules)+
done
schematic_goal ‹rev(?x, a:b:c:Nil)›
apply (rule rules)+
back
back
done
ML ‹
fun prolog_tac ctxt =
DEPTH_FIRST (has_fewer_prems 1) (resolve_tac ctxt @{thms rules} 1)
›
schematic_goal ‹rev(?x, a:b:c:Nil)›
apply (tactic ‹prolog_tac \<^context>›)
done
schematic_goal ‹rev(a:?x:c:?y:Nil, d:?z:b:?u)›
apply (tactic ‹prolog_tac \<^context>›)
done
schematic_goal ‹rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)›
apply (tactic ‹
DEPTH_SOLVE (resolve_tac \<^context> ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)›)
done
schematic_goal ‹a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x ∧ app(?x,?x,?y) ∧ rev(?y,?w)›
apply (tactic ‹
DEPTH_SOLVE (resolve_tac \<^context> ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)›)
done
end