--- a/src/HOL/Hoare/Hoare_Logic.thy Tue Mar 29 21:11:02 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Tue Mar 29 21:48:01 2011 +0200
@@ -10,7 +10,7 @@
theory Hoare_Logic
imports Main
-uses ("hoare_tac.ML")
+uses ("hoare_syntax.ML") ("hoare_tac.ML")
begin
types
@@ -45,9 +45,6 @@
where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)"
-
-(** parse translations **)
-
syntax
"_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
@@ -58,126 +55,10 @@
"_hoare" :: "['a assn,'a com,'a assn] => bool"
("{_} // _ // {_}" [0,55,0] 50)
-parse_translation {*
- let
- fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
- | mk_abstuple (x :: xs) body =
- Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
-
- fun mk_fbody x e [y] = if Syntax.eq_idt (x, y) then e else y
- | mk_fbody x e (y :: xs) =
- Syntax.const @{const_syntax Pair} $
- (if Syntax.eq_idt (x, y) then e else y) $ mk_fbody x e xs;
-
- fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
-
- (* bexp_tr & assn_tr *)
- (*all meta-variables for bexp except for TRUE are translated as if they
- were boolean expressions*)
-
- fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *)
- | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
-
- fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
-
- (* com_tr *)
-
- fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
- Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
- | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
- | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
- Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
- Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
- Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
- | com_tr t _ = t;
-
- fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
- | vars_tr t = [t];
-
- fun hoare_vars_tr [vars, pre, prg, post] =
- let val xs = vars_tr vars
- in Syntax.const @{const_syntax Valid} $
- assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
- end
- | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
-
- in [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] end
-*}
-
-
-(*****************************************************************************)
-
-(*** print translations ***)
-ML{*
-fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
- subst_bound (Syntax.free v, dest_abstuple body)
- | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
- | dest_abstuple trm = trm;
+use "hoare_syntax.ML"
+parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *}
-fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
- | abs2list (Abs(x,T,t)) = [Free (x, T)]
- | abs2list _ = [];
-
-fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
- | mk_ts (Abs(x,_,t)) = mk_ts t
- | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
- | mk_ts t = [t];
-
-fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
- ((Syntax.free x)::(abs2list t), mk_ts t)
- | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
- | mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
- | find_ch ((v,t)::vts) i xs =
- if t = Bound i then find_ch vts (i-1) xs
- else (true, (v, subst_bounds (xs, t)));
-
-fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
- | is_f (Abs(x,_,t)) = true
- | is_f t = false;
-*}
-
-(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
- | assn_tr' (Const (@{const_syntax inter}, _) $
- (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) =
- Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
- | assn_tr' t = t;
-
-fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
- | bexp_tr' t = t;
-*}
-
-(*com_tr' *)
-ML{*
-fun mk_assign f =
- let val (vs, ts) = mk_vts f;
- val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
- in
- if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
- else Syntax.const @{const_syntax annskip}
- end;
-
-fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
- if is_f f then mk_assign f
- else Syntax.const @{const_syntax Basic} $ f
- | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
- Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
- Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
- Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
- | com_tr' t = t;
-
-fun spec_tr' [p, c, q] =
- Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
-*}
-
-print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp:Valid_def)
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Mar 29 21:11:02 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Mar 29 21:48:01 2011 +0200
@@ -7,7 +7,7 @@
theory Hoare_Logic_Abort
imports Main
-uses ("hoare_tac.ML")
+uses ("hoare_syntax.ML") ("hoare_tac.ML")
begin
types
@@ -47,9 +47,6 @@
"Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
-
-(** parse translations **)
-
syntax
"_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
@@ -60,126 +57,11 @@
"_hoare_abort" :: "['a assn,'a com,'a assn] => bool"
("{_} // _ // {_}" [0,55,0] 50)
-parse_translation {*
- let
- fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
- | mk_abstuple (x :: xs) body =
- Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
-
- fun mk_fbody x e [y] = if Syntax.eq_idt (x, y) then e else y
- | mk_fbody x e (y :: xs) =
- Syntax.const @{const_syntax Pair} $
- (if Syntax.eq_idt (x, y) then e else y) $ mk_fbody x e xs;
-
- fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
-
- (* bexp_tr & assn_tr *)
- (*all meta-variables for bexp except for TRUE are translated as if they
- were boolean expressions*)
-
- fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *)
- | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
-
- fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
-
- (* com_tr *)
-
- fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
- Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
- | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
- | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
- Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
- Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
- Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
- | com_tr t _ = t;
-
- fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
- | vars_tr t = [t];
-
- fun hoare_vars_tr [vars, pre, prg, post] =
- let val xs = vars_tr vars
- in Syntax.const @{const_syntax Valid} $
- assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
- end
- | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
-
- in [(@{syntax_const "_hoare_abort_vars"}, hoare_vars_tr)] end
-*}
-
-
-
-(*****************************************************************************)
-
-(*** print translations ***)
-ML{*
-fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
- subst_bound (Syntax.free v, dest_abstuple body)
- | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
- | dest_abstuple trm = trm;
+use "hoare_syntax.ML"
+parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+print_translation
+ {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *}
-fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
- | abs2list (Abs(x,T,t)) = [Free (x, T)]
- | abs2list _ = [];
-
-fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
- | mk_ts (Abs(x,_,t)) = mk_ts t
- | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
- | mk_ts t = [t];
-
-fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
- ((Syntax.free x)::(abs2list t), mk_ts t)
- | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
- | mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
- | find_ch ((v,t)::vts) i xs =
- if t = Bound i then find_ch vts (i-1) xs
- else (true, (v, subst_bounds (xs,t)));
-
-fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
- | is_f (Abs(x,_,t)) = true
- | is_f t = false;
-*}
-
-(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
- | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $
- (Const (@{const_syntax Collect},_) $ T2)) =
- Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
- | assn_tr' t = t;
-
-fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
- | bexp_tr' t = t;
-*}
-
-(*com_tr' *)
-ML{*
-fun mk_assign f =
- let val (vs, ts) = mk_vts f;
- val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
- in
- if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
- else Syntax.const @{const_syntax annskip}
- end;
-
-fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
- if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f
- | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
- Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
- Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
- Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
- | com_tr' t = t;
-
-fun spec_tr' [p, c, q] =
- Syntax.const @{syntax_const "_hoare_abort"} $ assn_tr' p $ com_tr' c $ assn_tr' q
-*}
-
-print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
(*** The proof rules ***)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/hoare_syntax.ML Tue Mar 29 21:48:01 2011 +0200
@@ -0,0 +1,156 @@
+(* Title: HOL/Hoare/hoare_syntax.ML
+ Author: Leonor Prensa Nieto & Tobias Nipkow
+
+Syntax translations for Hoare logic.
+*)
+
+signature HOARE_SYNTAX =
+sig
+ val hoare_vars_tr: term list -> term
+ val spec_tr': string -> term list -> term
+end;
+
+structure Hoare_Syntax: HOARE_SYNTAX =
+struct
+
+(** parse translation **)
+
+local
+
+fun idt_name (Free (x, _)) = SOME x
+ | idt_name (Const ("_constrain", _) $ t $ _) = idt_name t
+ | idt_name _ = NONE;
+
+fun eq_idt tu =
+ (case pairself idt_name tu of
+ (SOME x, SOME y) => x = y
+ | _ => false);
+
+fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
+ | mk_abstuple (x :: xs) body =
+ Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
+
+fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
+ | mk_fbody x e (y :: xs) =
+ Syntax.const @{const_syntax Pair} $
+ (if eq_idt (x, y) then e else y) $ mk_fbody x e xs;
+
+fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
+
+
+(* bexp_tr & assn_tr *)
+(*all meta-variables for bexp except for TRUE are translated as if they
+ were boolean expressions*)
+
+fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *)
+ | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
+
+fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
+
+
+(* com_tr *)
+
+fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
+ Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
+ | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
+ | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
+ Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
+ | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
+ Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
+ | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
+ Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+ | com_tr t _ = t;
+
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
+ | vars_tr t = [t];
+
+in
+
+fun hoare_vars_tr [vars, pre, prg, post] =
+ let val xs = vars_tr vars
+ in Syntax.const @{const_syntax Valid} $
+ assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
+ end
+ | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
+
+end;
+
+
+
+(** print translation **)
+
+local
+
+fun dest_abstuple
+ (Const (@{const_syntax prod_case}, _) $ Abs (v, _, body)) =
+ subst_bound (Syntax.free v, dest_abstuple body)
+ | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
+ | dest_abstuple tm = tm;
+
+fun abs2list (Const (@{const_syntax prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+ | abs2list (Abs (x, T, t)) = [Free (x, T)]
+ | abs2list _ = [];
+
+fun mk_ts (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = mk_ts t
+ | mk_ts (Abs (x, _, t)) = mk_ts t
+ | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
+ | mk_ts t = [t];
+
+fun mk_vts (Const (@{const_syntax prod_case},_) $ Abs (x, _, t)) =
+ (Syntax.free x :: abs2list t, mk_ts t)
+ | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
+ | mk_vts t = raise Match;
+
+fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) (* FIXME no_ch!? *)
+ | find_ch ((v, t) :: vts) i xs =
+ if t = Bound i then find_ch vts (i - 1) xs
+ else (true, (v, subst_bounds (xs, t)));
+
+fun is_f (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = true
+ | is_f (Abs (x, _, t)) = true
+ | is_f t = false;
+
+
+(* assn_tr' & bexp_tr'*)
+
+fun assn_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
+ | assn_tr' (Const (@{const_syntax inter}, _) $
+ (Const (@{const_syntax Collect}, _) $ T1) $ (Const (@{const_syntax Collect}, _) $ T2)) =
+ Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
+ | assn_tr' t = t;
+
+fun bexp_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
+ | bexp_tr' t = t;
+
+
+(* com_tr' *)
+
+fun mk_assign f =
+ let
+ val (vs, ts) = mk_vts f;
+ val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
+ in
+ if ch
+ then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
+ else Syntax.const @{const_syntax annskip}
+ end;
+
+fun com_tr' (Const (@{const_syntax Basic}, _) $ f) =
+ if is_f f then mk_assign f
+ else Syntax.const @{const_syntax Basic} $ f
+ | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
+ Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
+ | com_tr' (Const (@{const_syntax Cond}, _) $ b $ c1 $ c2) =
+ Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
+ | com_tr' (Const (@{const_syntax While}, _) $ b $ I $ c) =
+ Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
+ | com_tr' t = t;
+
+in
+
+fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q
+
+end;
+
+end;
+
--- a/src/HOL/IsaMakefile Tue Mar 29 21:11:02 2011 +0200
+++ b/src/HOL/IsaMakefile Tue Mar 29 21:48:01 2011 +0200
@@ -650,12 +650,12 @@
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \
- Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy \
- Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \
+ Hoare/Hoare.thy Hoare/hoare_syntax.ML Hoare/hoare_tac.ML \
+ Hoare/Heap.thy Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \
Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \
Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \
- Hoare/SchorrWaite.thy Hoare/Separation.thy \
- Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
+ Hoare/SchorrWaite.thy Hoare/Separation.thy Hoare/SepLogHeap.thy \
+ Hoare/document/root.tex Hoare/document/root.bib
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
--- a/src/Pure/Syntax/syn_trans.ML Tue Mar 29 21:11:02 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Tue Mar 29 21:48:01 2011 +0200
@@ -37,7 +37,6 @@
val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
val constrainAbsC: string
val abs_tr: term list -> term
- val eq_idt: term * term -> bool
val pure_trfuns:
(string * (Ast.ast list -> Ast.ast)) list *
(string * (term list -> term)) list *
@@ -116,18 +115,6 @@
| abs_tr ts = raise TERM ("abs_tr", ts);
-(* equality on idt *)
-
-fun idt_name (Free (x, _)) = SOME x
- | idt_name (Const ("_constrain", _) $ t $ _) = idt_name t
- | idt_name _ = NONE;
-
-fun eq_idt tu =
- (case pairself idt_name tu of
- (SOME x, SOME y) => x = y
- | _ => false);
-
-
(* binder *)
fun mk_binder_tr (syn, name) =