228 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t; |
228 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t; |
229 val thmId = thmid ^ UnparseC.term_in_thy thy arg; |
229 val thmId = thmid ^ UnparseC.term_in_thy thy arg; |
230 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end |
230 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end |
231 | eval_var _ _ _ _ = NONE; |
231 | eval_var _ _ _ _ = NONE; |
232 |
232 |
|
233 (* refer to Thm.lhs_of *) |
233 fun lhs (Const ("HOL.eq",_) $ l $ _) = l |
234 fun lhs (Const ("HOL.eq",_) $ l $ _) = l |
234 | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")"); |
235 | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")"); |
235 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*) |
236 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*) |
236 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ = |
237 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ = |
237 SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l), |
238 SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l), |